%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT001-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:11:11 PM UTC 2026
% Result : Unsatisfiable 88.32s 18.10s
% Output : Proof 88.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 18
% Syntax : Number of formulae : 206 ( 178 unt; 0 def)
% Number of atoms : 366 ( 146 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 326 ( 166 ~; 160 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-4 aty)
% Number of variables : 535 ( 38 sgn 88 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f3,hypothesis,
( greater(J,I)
| ~ greater(H,G)
| ~ greater(F,E)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1_FOL_4) ).
fof(f3_nnf,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( greater(J,I)
| ~ greater(H,G)
| ~ greater(F,E)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( greater(J,I)
| ~ greater(H,G)
| ~ greater(F,E)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( greater(X9,X8)
| ~ greater(X7,X6)
| ~ greater(X5,X4)
| ~ survival_chance(X2,X9,X3)
| ~ survival_chance(X0,X8,X1)
| ~ accountability(X2,X7,X3)
| ~ accountability(X0,X6,X1)
| ~ reliability(X2,X5,X3)
| ~ reliability(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t18,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reliability(X1,X5,X2),true,ifeq(reliability(X3,X6,X4),true,ifeq(accountability(X1,X7,X2),true,ifeq(accountability(X3,X8,X4),true,ifeq(survival_chance(X1,X9,X2),true,ifeq(survival_chance(X3,X10,X4),true,ifeq(greater(X6,X5),true,ifeq(greater(X8,X7),true,greater(X10,X9),true),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t235,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reliability(X1,X5,X2),true,ifeq(reliability(X3,X6,X4),true,ifeq(accountability(X1,X7,X2),true,ifeq(accountability(X3,X8,X4),true,ifeq(survival_chance(X1,X9,X2),true,ifeq(survival_chance(X3,X10,X4),true,ifeq(greater(X6,X5),true,ifeq(greater(X8,X7),true,greater(X10,X9),true),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(f1,axiom,
( accountability(A,sk2(B,A),B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_2) ).
fof(f1_nnf,plain,
! [A,B] :
( accountability(A,sk2(B,A),B)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( accountability(A,sk2(B,A),B)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( accountability(X0,sk2(X1,X0),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t10,plain,
ifeq(organization(X1,X2),true,accountability(X1,sk2(X2,X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t29,plain,
ifeq(organization(X1,X2),true,accountability(X1,sk2(X2,X1),X2),true) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(f9,negated_conjecture,
organization(sk4,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_10) ).
fof(f9_nnf,plain,
organization(sk4,sk6),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
organization(sk4,sk6),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t1,plain,
organization(sk4,sk6) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t20,plain,
organization(sk4,sk6) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
true = ifeq(true,true,accountability(sk4,sk2(sk6,sk4),sk6),true),
inference(cp,[status(thm)],[t29,t20]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t28,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t5342,plain,
true = accountability(sk4,sk2(sk6,sk4),sk6),
inference(step,[status(thm)],[t30,t28]) ).
cnf(t32,plain,
accountability(sk4,sk2(sk6,sk4),sk6) = true,
inference(orient,[status(thm)],[t5342]) ).
cnf(t247,plain,
true = ifeq(organization(sk4,sk6),true,ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(survival_chance(sk4,X6,sk6),true,ifeq(survival_chance(X1,X7,X2),true,ifeq(greater(X4,X3),true,ifeq(greater(X5,sk2(sk6,sk4)),true,greater(X7,X6),true),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t235,t32]) ).
cnf(t6964,plain,
true = ifeq(true,true,ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(survival_chance(sk4,X6,sk6),true,ifeq(survival_chance(X1,X7,X2),true,ifeq(greater(X4,X3),true,ifeq(greater(X5,sk2(sk6,sk4)),true,greater(X7,X6),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t247,t20]) ).
cnf(t6965,plain,
true = ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(survival_chance(sk4,X6,sk6),true,ifeq(survival_chance(X1,X7,X2),true,ifeq(greater(X4,X3),true,ifeq(greater(X5,sk2(sk6,sk4)),true,greater(X7,X6),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t6964,t28]) ).
cnf(t6966,plain,
true = ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(accountability(X1,X5,X2),true,ifeq(survival_chance(sk4,X6,sk6),true,ifeq(survival_chance(X1,X7,X2),true,ifeq(greater(X4,X3),true,ifeq(greater(X5,sk2(sk6,sk4)),true,greater(X7,X6),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t6965,t28]) ).
cnf(t4175,plain,
ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(accountability(X1,X5,X2),true,ifeq(survival_chance(sk4,X6,sk6),true,ifeq(survival_chance(X1,X7,X2),true,ifeq(greater(X4,X3),true,ifeq(greater(X5,sk2(sk6,sk4)),true,greater(X7,X6),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t6966]) ).
cnf(f10,negated_conjecture,
organization(sk5,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_11) ).
fof(f10_nnf,plain,
organization(sk5,sk7),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
organization(sk5,sk7),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t2,plain,
organization(sk5,sk7) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t21,plain,
organization(sk5,sk7) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t31,plain,
true = ifeq(true,true,accountability(sk5,sk2(sk7,sk5),sk7),true),
inference(cp,[status(thm)],[t29,t21]) ).
cnf(t5343,plain,
true = accountability(sk5,sk2(sk7,sk5),sk7),
inference(step,[status(thm)],[t31,t28]) ).
cnf(t33,plain,
accountability(sk5,sk2(sk7,sk5),sk7) = true,
inference(orient,[status(thm)],[t5343]) ).
cnf(t4177,plain,
true = ifeq(organization(sk5,sk7),true,ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(true,true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,ifeq(greater(sk2(sk7,sk5),sk2(sk6,sk4)),true,greater(X4,X3),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t4175,t33]) ).
cnf(t7208,plain,
true = ifeq(true,true,ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(true,true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,ifeq(greater(sk2(sk7,sk5),sk2(sk6,sk4)),true,greater(X4,X3),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t4177,t21]) ).
cnf(t7209,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(true,true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,ifeq(greater(sk2(sk7,sk5),sk2(sk6,sk4)),true,greater(X4,X3),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t7208,t28]) ).
cnf(t7210,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,ifeq(greater(sk2(sk7,sk5),sk2(sk6,sk4)),true,greater(X4,X3),true),true),true),true),true),true),
inference(step,[status(thm)],[t7209,t28]) ).
cnf(f5,hypothesis,
( greater(H,G)
| ~ greater(J,I)
| ~ reproducibility(C,J,D)
| ~ reproducibility(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2_FOL_6) ).
fof(f5_nnf,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( greater(H,G)
| ~ greater(J,I)
| ~ reproducibility(C,J,D)
| ~ reproducibility(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( greater(H,G)
| ~ greater(J,I)
| ~ reproducibility(C,J,D)
| ~ reproducibility(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( greater(X7,X6)
| ~ greater(X9,X8)
| ~ reproducibility(X2,X9,X3)
| ~ reproducibility(X0,X8,X1)
| ~ accountability(X2,X7,X3)
| ~ accountability(X0,X6,X1)
| ~ reliability(X2,X5,X3)
| ~ reliability(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t14,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reliability(X1,X5,X2),true,ifeq(reliability(X3,X6,X4),true,ifeq(accountability(X1,X7,X2),true,ifeq(accountability(X3,X8,X4),true,ifeq(reproducibility(X1,X9,X2),true,ifeq(reproducibility(X3,X10,X4),true,ifeq(greater(X10,X9),true,greater(X8,X7),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t76,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reliability(X1,X5,X2),true,ifeq(reliability(X3,X6,X4),true,ifeq(accountability(X1,X7,X2),true,ifeq(accountability(X3,X8,X4),true,ifeq(reproducibility(X1,X9,X2),true,ifeq(reproducibility(X3,X10,X4),true,ifeq(greater(X10,X9),true,greater(X8,X7),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t14]) ).
cnf(t83,plain,
true = ifeq(organization(sk4,sk6),true,ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X5,sk2(sk6,sk4)),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t76,t32]) ).
cnf(t5840,plain,
true = ifeq(true,true,ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X5,sk2(sk6,sk4)),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t83,t20]) ).
cnf(t5841,plain,
true = ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X5,sk2(sk6,sk4)),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t5840,t28]) ).
cnf(t5842,plain,
true = ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X5,sk2(sk6,sk4)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t5841,t28]) ).
cnf(t1041,plain,
ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X5,sk2(sk6,sk4)),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t5842]) ).
cnf(f0,axiom,
( reliability(A,sk1(B,A),B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_1) ).
fof(f0_nnf,plain,
! [A,B] :
( reliability(A,sk1(B,A),B)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( reliability(A,sk1(B,A),B)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( reliability(X0,sk1(X1,X0),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t11,plain,
ifeq(organization(X1,X2),true,reliability(X1,sk1(X2,X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t34,plain,
ifeq(organization(X1,X2),true,reliability(X1,sk1(X2,X1),X2),true) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t36,plain,
true = ifeq(true,true,reliability(sk5,sk1(sk7,sk5),sk7),true),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t5345,plain,
true = reliability(sk5,sk1(sk7,sk5),sk7),
inference(step,[status(thm)],[t36,t28]) ).
cnf(t38,plain,
reliability(sk5,sk1(sk7,sk5),sk7) = true,
inference(orient,[status(thm)],[t5345]) ).
cnf(t1046,plain,
true = ifeq(organization(sk5,sk7),true,ifeq(reliability(sk4,X1,sk6),true,ifeq(true,true,ifeq(accountability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,sk2(sk6,sk4)),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t1041,t38]) ).
cnf(t5875,plain,
true = ifeq(true,true,ifeq(reliability(sk4,X1,sk6),true,ifeq(true,true,ifeq(accountability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,sk2(sk6,sk4)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1046,t21]) ).
cnf(t5876,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(true,true,ifeq(accountability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,sk2(sk6,sk4)),true),true),true),true),true),true),
inference(step,[status(thm)],[t5875,t28]) ).
cnf(t5877,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(accountability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,sk2(sk6,sk4)),true),true),true),true),true),
inference(step,[status(thm)],[t5876,t28]) ).
cnf(t1134,plain,
ifeq(reliability(sk4,X1,sk6),true,ifeq(accountability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,sk2(sk6,sk4)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t5877]) ).
cnf(t35,plain,
true = ifeq(true,true,reliability(sk4,sk1(sk6,sk4),sk6),true),
inference(cp,[status(thm)],[t34,t20]) ).
cnf(t5344,plain,
true = reliability(sk4,sk1(sk6,sk4),sk6),
inference(step,[status(thm)],[t35,t28]) ).
cnf(t37,plain,
reliability(sk4,sk1(sk6,sk4),sk6) = true,
inference(orient,[status(thm)],[t5344]) ).
cnf(t1137,plain,
true = ifeq(true,true,ifeq(accountability(sk5,X1,sk7),true,ifeq(reproducibility(sk4,X2,sk6),true,ifeq(reproducibility(sk5,X3,sk7),true,ifeq(greater(X3,X2),true,greater(X1,sk2(sk6,sk4)),true),true),true),true),true),
inference(cp,[status(thm)],[t1134,t37]) ).
cnf(t5878,plain,
true = ifeq(accountability(sk5,X1,sk7),true,ifeq(reproducibility(sk4,X2,sk6),true,ifeq(reproducibility(sk5,X3,sk7),true,ifeq(greater(X3,X2),true,greater(X1,sk2(sk6,sk4)),true),true),true),true),
inference(step,[status(thm)],[t1137,t28]) ).
cnf(t1140,plain,
ifeq(accountability(sk5,X1,sk7),true,ifeq(reproducibility(sk4,X2,sk6),true,ifeq(reproducibility(sk5,X3,sk7),true,ifeq(greater(X3,X2),true,greater(X1,sk2(sk6,sk4)),true),true),true),true) = true,
inference(orient,[status(thm)],[t5878]) ).
cnf(t1143,plain,
true = ifeq(true,true,ifeq(reproducibility(sk4,X1,sk6),true,ifeq(reproducibility(sk5,X2,sk7),true,ifeq(greater(X2,X1),true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),true),true),
inference(cp,[status(thm)],[t1140,t33]) ).
cnf(t5884,plain,
true = ifeq(reproducibility(sk4,X1,sk6),true,ifeq(reproducibility(sk5,X2,sk7),true,ifeq(greater(X2,X1),true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),true),
inference(step,[status(thm)],[t1143,t28]) ).
cnf(t1156,plain,
ifeq(reproducibility(sk4,X1,sk6),true,ifeq(reproducibility(sk5,X2,sk7),true,ifeq(greater(X2,X1),true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),true) = true,
inference(orient,[status(thm)],[t5884]) ).
cnf(f8,hypothesis,
( greater(F,E)
| ~ greater(H,G)
| ~ inertia(C,H,D)
| ~ inertia(A,G,B)
| ~ reproducibility(C,F,D)
| ~ reproducibility(A,E,B)
| ~ reorganization_free(C,D,D)
| ~ reorganization_free(A,B,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3_FOL_9) ).
fof(f8_nnf,plain,
! [A,B,C,D,E,F,G,H] :
( greater(F,E)
| ~ greater(H,G)
| ~ inertia(C,H,D)
| ~ inertia(A,G,B)
| ~ reproducibility(C,F,D)
| ~ reproducibility(A,E,B)
| ~ reorganization_free(C,D,D)
| ~ reorganization_free(A,B,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B,C,D,E,F,G,H] :
( greater(F,E)
| ~ greater(H,G)
| ~ inertia(C,H,D)
| ~ inertia(A,G,B)
| ~ reproducibility(C,F,D)
| ~ reproducibility(A,E,B)
| ~ reorganization_free(C,D,D)
| ~ reorganization_free(A,B,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( greater(X5,X4)
| ~ greater(X7,X6)
| ~ inertia(X2,X7,X3)
| ~ inertia(X0,X6,X1)
| ~ reproducibility(X2,X5,X3)
| ~ reproducibility(X0,X4,X1)
| ~ reorganization_free(X2,X3,X3)
| ~ reorganization_free(X0,X1,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t16,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reorganization_free(X3,X4,X4),true,ifeq(reproducibility(X1,X5,X2),true,ifeq(reproducibility(X3,X6,X4),true,ifeq(inertia(X1,X7,X2),true,ifeq(inertia(X3,X8,X4),true,ifeq(greater(X8,X7),true,greater(X6,X5),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t158,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reorganization_free(X3,X4,X4),true,ifeq(reproducibility(X1,X5,X2),true,ifeq(reproducibility(X3,X6,X4),true,ifeq(inertia(X1,X7,X2),true,ifeq(inertia(X3,X8,X4),true,ifeq(greater(X8,X7),true,greater(X6,X5),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(f17,negated_conjecture,
greater(sk9,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_18) ).
fof(f17_nnf,plain,
greater(sk9,sk8),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
greater(sk9,sk8),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(t0,plain,
greater(sk9,sk8) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t19,plain,
greater(sk9,sk8) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t159,plain,
true = ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reorganization_free(X3,X4,X4),true,ifeq(reproducibility(X1,X5,X2),true,ifeq(reproducibility(X3,X6,X4),true,ifeq(inertia(X1,sk8,X2),true,ifeq(inertia(X3,sk9,X4),true,ifeq(true,true,greater(X6,X5),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t158,t19]) ).
cnf(t6272,plain,
true = ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reorganization_free(X3,X4,X4),true,ifeq(reproducibility(X1,X5,X2),true,ifeq(reproducibility(X3,X6,X4),true,ifeq(inertia(X1,sk8,X2),true,ifeq(inertia(X3,sk9,X4),true,greater(X6,X5),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t159,t28]) ).
cnf(t1906,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reorganization_free(X3,X4,X4),true,ifeq(reproducibility(X1,X5,X2),true,ifeq(reproducibility(X3,X6,X4),true,ifeq(inertia(X1,sk8,X2),true,ifeq(inertia(X3,sk9,X4),true,greater(X6,X5),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t6272]) ).
cnf(f2,axiom,
( reproducibility(A,sk3(B,A),B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3_3) ).
fof(f2_nnf,plain,
! [A,B] :
( reproducibility(A,sk3(B,A),B)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] :
( reproducibility(A,sk3(B,A),B)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( reproducibility(X0,sk3(X1,X0),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t12,plain,
ifeq(organization(X1,X2),true,reproducibility(X1,sk3(X2,X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t39,plain,
ifeq(organization(X1,X2),true,reproducibility(X1,sk3(X2,X1),X2),true) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t40,plain,
true = ifeq(true,true,reproducibility(sk4,sk3(sk6,sk4),sk6),true),
inference(cp,[status(thm)],[t39,t20]) ).
cnf(t5346,plain,
true = reproducibility(sk4,sk3(sk6,sk4),sk6),
inference(step,[status(thm)],[t40,t28]) ).
cnf(t42,plain,
reproducibility(sk4,sk3(sk6,sk4),sk6) = true,
inference(orient,[status(thm)],[t5346]) ).
cnf(t1911,plain,
true = ifeq(organization(sk4,sk6),true,ifeq(organization(X1,X2),true,ifeq(reorganization_free(sk4,sk6,sk6),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(true,true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(sk4,sk8,sk6),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t1906,t42]) ).
cnf(t6274,plain,
true = ifeq(true,true,ifeq(organization(X1,X2),true,ifeq(reorganization_free(sk4,sk6,sk6),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(true,true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(sk4,sk8,sk6),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1911,t20]) ).
cnf(t6275,plain,
true = ifeq(organization(X1,X2),true,ifeq(reorganization_free(sk4,sk6,sk6),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(true,true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(sk4,sk8,sk6),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t6274,t28]) ).
cnf(f11,negated_conjecture,
reorganization_free(sk4,sk6,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_12) ).
fof(f11_nnf,plain,
reorganization_free(sk4,sk6,sk6),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
reorganization_free(sk4,sk6,sk6),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t5,plain,
reorganization_free(sk4,sk6,sk6) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t24,plain,
reorganization_free(sk4,sk6,sk6) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t6276,plain,
true = ifeq(organization(X1,X2),true,ifeq(true,true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(true,true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(sk4,sk8,sk6),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t6275,t24]) ).
cnf(t6277,plain,
true = ifeq(organization(X1,X2),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(true,true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(sk4,sk8,sk6),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),true),
inference(step,[status(thm)],[t6276,t28]) ).
cnf(t6278,plain,
true = ifeq(organization(X1,X2),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(sk4,sk8,sk6),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),
inference(step,[status(thm)],[t6277,t28]) ).
cnf(f13,negated_conjecture,
inertia(sk4,sk8,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_14) ).
fof(f13_nnf,plain,
inertia(sk4,sk8,sk6),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
inertia(sk4,sk8,sk6),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t3,plain,
inertia(sk4,sk8,sk6) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t22,plain,
inertia(sk4,sk8,sk6) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t6279,plain,
true = ifeq(organization(X1,X2),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reproducibility(X1,X3,X2),true,ifeq(true,true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),true),
inference(step,[status(thm)],[t6278,t22]) ).
cnf(t6280,plain,
true = ifeq(organization(X1,X2),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true),
inference(step,[status(thm)],[t6279,t28]) ).
cnf(t1916,plain,
ifeq(organization(X1,X2),true,ifeq(reorganization_free(X1,X2,X2),true,ifeq(reproducibility(X1,X3,X2),true,ifeq(inertia(X1,sk9,X2),true,greater(X3,sk3(sk6,sk4)),true),true),true),true) = true,
inference(orient,[status(thm)],[t6280]) ).
cnf(t41,plain,
true = ifeq(true,true,reproducibility(sk5,sk3(sk7,sk5),sk7),true),
inference(cp,[status(thm)],[t39,t21]) ).
cnf(t5347,plain,
true = reproducibility(sk5,sk3(sk7,sk5),sk7),
inference(step,[status(thm)],[t41,t28]) ).
cnf(t43,plain,
reproducibility(sk5,sk3(sk7,sk5),sk7) = true,
inference(orient,[status(thm)],[t5347]) ).
cnf(t1920,plain,
true = ifeq(organization(sk5,sk7),true,ifeq(reorganization_free(sk5,sk7,sk7),true,ifeq(true,true,ifeq(inertia(sk5,sk9,sk7),true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),true),true),true),
inference(cp,[status(thm)],[t1916,t43]) ).
cnf(t6281,plain,
true = ifeq(true,true,ifeq(reorganization_free(sk5,sk7,sk7),true,ifeq(true,true,ifeq(inertia(sk5,sk9,sk7),true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),true),true),true),
inference(step,[status(thm)],[t1920,t21]) ).
cnf(t6282,plain,
true = ifeq(reorganization_free(sk5,sk7,sk7),true,ifeq(true,true,ifeq(inertia(sk5,sk9,sk7),true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),true),true),
inference(step,[status(thm)],[t6281,t28]) ).
cnf(f12,negated_conjecture,
reorganization_free(sk5,sk7,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_13) ).
fof(f12_nnf,plain,
reorganization_free(sk5,sk7,sk7),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
reorganization_free(sk5,sk7,sk7),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t6,plain,
reorganization_free(sk5,sk7,sk7) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t25,plain,
reorganization_free(sk5,sk7,sk7) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t6283,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(inertia(sk5,sk9,sk7),true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),true),true),
inference(step,[status(thm)],[t6282,t25]) ).
cnf(t6284,plain,
true = ifeq(true,true,ifeq(inertia(sk5,sk9,sk7),true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),true),
inference(step,[status(thm)],[t6283,t28]) ).
cnf(t6285,plain,
true = ifeq(inertia(sk5,sk9,sk7),true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),
inference(step,[status(thm)],[t6284,t28]) ).
cnf(f14,negated_conjecture,
inertia(sk5,sk9,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_15) ).
fof(f14_nnf,plain,
inertia(sk5,sk9,sk7),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
inertia(sk5,sk9,sk7),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t4,plain,
inertia(sk5,sk9,sk7) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t23,plain,
inertia(sk5,sk9,sk7) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t6286,plain,
true = ifeq(true,true,greater(sk3(sk7,sk5),sk3(sk6,sk4)),true),
inference(step,[status(thm)],[t6285,t23]) ).
cnf(t6287,plain,
true = greater(sk3(sk7,sk5),sk3(sk6,sk4)),
inference(step,[status(thm)],[t6286,t28]) ).
cnf(t1921,plain,
greater(sk3(sk7,sk5),sk3(sk6,sk4)) = true,
inference(orient,[status(thm)],[t6287]) ).
cnf(t2071,plain,
true = ifeq(reproducibility(sk4,sk3(sk6,sk4),sk6),true,ifeq(reproducibility(sk5,sk3(sk7,sk5),sk7),true,ifeq(true,true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),true),
inference(cp,[status(thm)],[t1156,t1921]) ).
cnf(t6293,plain,
true = ifeq(true,true,ifeq(reproducibility(sk5,sk3(sk7,sk5),sk7),true,ifeq(true,true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),true),
inference(step,[status(thm)],[t2071,t42]) ).
cnf(t6294,plain,
true = ifeq(reproducibility(sk5,sk3(sk7,sk5),sk7),true,ifeq(true,true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),
inference(step,[status(thm)],[t6293,t28]) ).
cnf(t6295,plain,
true = ifeq(true,true,ifeq(true,true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),true),
inference(step,[status(thm)],[t6294,t43]) ).
cnf(t6296,plain,
true = ifeq(true,true,greater(sk2(sk7,sk5),sk2(sk6,sk4)),true),
inference(step,[status(thm)],[t6295,t28]) ).
cnf(t6297,plain,
true = greater(sk2(sk7,sk5),sk2(sk6,sk4)),
inference(step,[status(thm)],[t6296,t28]) ).
cnf(t2388,plain,
greater(sk2(sk7,sk5),sk2(sk6,sk4)) = true,
inference(orient,[status(thm)],[t6297]) ).
cnf(t7211,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,ifeq(true,true,greater(X4,X3),true),true),true),true),true),true),
inference(step,[status(thm)],[t7210,t2388]) ).
cnf(t7212,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,greater(X4,X3),true),true),true),true),true),
inference(step,[status(thm)],[t7211,t28]) ).
cnf(t4904,plain,
ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(survival_chance(sk4,X3,sk6),true,ifeq(survival_chance(sk5,X4,sk7),true,ifeq(greater(X2,X1),true,greater(X4,X3),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t7212]) ).
cnf(f4,hypothesis,
( greater(F,E)
| ~ greater(J,I)
| ~ reproducibility(C,J,D)
| ~ reproducibility(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2_FOL_5) ).
fof(f4_nnf,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( greater(F,E)
| ~ greater(J,I)
| ~ reproducibility(C,J,D)
| ~ reproducibility(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( greater(F,E)
| ~ greater(J,I)
| ~ reproducibility(C,J,D)
| ~ reproducibility(A,I,B)
| ~ accountability(C,H,D)
| ~ accountability(A,G,B)
| ~ reliability(C,F,D)
| ~ reliability(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( greater(X5,X4)
| ~ greater(X9,X8)
| ~ reproducibility(X2,X9,X3)
| ~ reproducibility(X0,X8,X1)
| ~ accountability(X2,X7,X3)
| ~ accountability(X0,X6,X1)
| ~ reliability(X2,X5,X3)
| ~ reliability(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t13,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reliability(X1,X5,X2),true,ifeq(reliability(X3,X6,X4),true,ifeq(accountability(X1,X7,X2),true,ifeq(accountability(X3,X8,X4),true,ifeq(reproducibility(X1,X9,X2),true,ifeq(reproducibility(X3,X10,X4),true,ifeq(greater(X10,X9),true,greater(X6,X5),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t44,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(reliability(X1,X5,X2),true,ifeq(reliability(X3,X6,X4),true,ifeq(accountability(X1,X7,X2),true,ifeq(accountability(X3,X8,X4),true,ifeq(reproducibility(X1,X9,X2),true,ifeq(reproducibility(X3,X10,X4),true,ifeq(greater(X10,X9),true,greater(X6,X5),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t51,plain,
true = ifeq(organization(sk4,sk6),true,ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X4,X3),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t44,t32]) ).
cnf(t5348,plain,
true = ifeq(true,true,ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X4,X3),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t51,t20]) ).
cnf(t5349,plain,
true = ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(true,true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X4,X3),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t5348,t28]) ).
cnf(t5350,plain,
true = ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X4,X3),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t5349,t28]) ).
cnf(t63,plain,
ifeq(organization(X1,X2),true,ifeq(reliability(sk4,X3,sk6),true,ifeq(reliability(X1,X4,X2),true,ifeq(accountability(X1,X5,X2),true,ifeq(reproducibility(sk4,X6,sk6),true,ifeq(reproducibility(X1,X7,X2),true,ifeq(greater(X7,X6),true,greater(X4,X3),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t5350]) ).
cnf(t69,plain,
true = ifeq(organization(sk5,sk7),true,ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(true,true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,X1),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t63,t33]) ).
cnf(t5396,plain,
true = ifeq(true,true,ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(true,true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,X1),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t69,t21]) ).
cnf(t5397,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(true,true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,X1),true),true),true),true),true),true),
inference(step,[status(thm)],[t5396,t28]) ).
cnf(t5398,plain,
true = ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,X1),true),true),true),true),true),
inference(step,[status(thm)],[t5397,t28]) ).
cnf(t215,plain,
ifeq(reliability(sk4,X1,sk6),true,ifeq(reliability(sk5,X2,sk7),true,ifeq(reproducibility(sk4,X3,sk6),true,ifeq(reproducibility(sk5,X4,sk7),true,ifeq(greater(X4,X3),true,greater(X2,X1),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t5398]) ).
cnf(t218,plain,
true = ifeq(true,true,ifeq(reliability(sk5,X1,sk7),true,ifeq(reproducibility(sk4,X2,sk6),true,ifeq(reproducibility(sk5,X3,sk7),true,ifeq(greater(X3,X2),true,greater(X1,sk1(sk6,sk4)),true),true),true),true),true),
inference(cp,[status(thm)],[t215,t37]) ).
cnf(t5403,plain,
true = ifeq(reliability(sk5,X1,sk7),true,ifeq(reproducibility(sk4,X2,sk6),true,ifeq(reproducibility(sk5,X3,sk7),true,ifeq(greater(X3,X2),true,greater(X1,sk1(sk6,sk4)),true),true),true),true),
inference(step,[status(thm)],[t218,t28]) ).
cnf(t231,plain,
ifeq(reliability(sk5,X1,sk7),true,ifeq(reproducibility(sk4,X2,sk6),true,ifeq(reproducibility(sk5,X3,sk7),true,ifeq(greater(X3,X2),true,greater(X1,sk1(sk6,sk4)),true),true),true),true) = true,
inference(orient,[status(thm)],[t5403]) ).
cnf(t232,plain,
true = ifeq(true,true,ifeq(reproducibility(sk4,X1,sk6),true,ifeq(reproducibility(sk5,X2,sk7),true,ifeq(greater(X2,X1),true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),true),true),
inference(cp,[status(thm)],[t231,t38]) ).
cnf(t5404,plain,
true = ifeq(reproducibility(sk4,X1,sk6),true,ifeq(reproducibility(sk5,X2,sk7),true,ifeq(greater(X2,X1),true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),true),
inference(step,[status(thm)],[t232,t28]) ).
cnf(t256,plain,
ifeq(reproducibility(sk4,X1,sk6),true,ifeq(reproducibility(sk5,X2,sk7),true,ifeq(greater(X2,X1),true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),true) = true,
inference(orient,[status(thm)],[t5404]) ).
cnf(t1970,plain,
true = ifeq(reproducibility(sk4,sk3(sk6,sk4),sk6),true,ifeq(reproducibility(sk5,sk3(sk7,sk5),sk7),true,ifeq(true,true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),true),
inference(cp,[status(thm)],[t256,t1921]) ).
cnf(t6288,plain,
true = ifeq(true,true,ifeq(reproducibility(sk5,sk3(sk7,sk5),sk7),true,ifeq(true,true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),true),
inference(step,[status(thm)],[t1970,t42]) ).
cnf(t6289,plain,
true = ifeq(reproducibility(sk5,sk3(sk7,sk5),sk7),true,ifeq(true,true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),
inference(step,[status(thm)],[t6288,t28]) ).
cnf(t6290,plain,
true = ifeq(true,true,ifeq(true,true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),true),
inference(step,[status(thm)],[t6289,t43]) ).
cnf(t6291,plain,
true = ifeq(true,true,greater(sk1(sk7,sk5),sk1(sk6,sk4)),true),
inference(step,[status(thm)],[t6290,t28]) ).
cnf(t6292,plain,
true = greater(sk1(sk7,sk5),sk1(sk6,sk4)),
inference(step,[status(thm)],[t6291,t28]) ).
cnf(t2159,plain,
greater(sk1(sk7,sk5),sk1(sk6,sk4)) = true,
inference(orient,[status(thm)],[t6292]) ).
cnf(t4922,plain,
true = ifeq(reliability(sk4,sk1(sk6,sk4),sk6),true,ifeq(reliability(sk5,sk1(sk7,sk5),sk7),true,ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,ifeq(true,true,greater(X2,X1),true),true),true),true),true),
inference(cp,[status(thm)],[t4904,t2159]) ).
cnf(t7213,plain,
true = ifeq(true,true,ifeq(reliability(sk5,sk1(sk7,sk5),sk7),true,ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,ifeq(true,true,greater(X2,X1),true),true),true),true),true),
inference(step,[status(thm)],[t4922,t37]) ).
cnf(t7214,plain,
true = ifeq(reliability(sk5,sk1(sk7,sk5),sk7),true,ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,ifeq(true,true,greater(X2,X1),true),true),true),true),
inference(step,[status(thm)],[t7213,t28]) ).
cnf(t7215,plain,
true = ifeq(true,true,ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,ifeq(true,true,greater(X2,X1),true),true),true),true),
inference(step,[status(thm)],[t7214,t38]) ).
cnf(t7216,plain,
true = ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,ifeq(true,true,greater(X2,X1),true),true),true),
inference(step,[status(thm)],[t7215,t28]) ).
cnf(t7217,plain,
true = ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,greater(X2,X1),true),true),
inference(step,[status(thm)],[t7216,t28]) ).
cnf(t4929,plain,
ifeq(survival_chance(sk4,X1,sk6),true,ifeq(survival_chance(sk5,X2,sk7),true,greater(X2,X1),true),true) = true,
inference(orient,[status(thm)],[t7217]) ).
cnf(f15,negated_conjecture,
survival_chance(sk4,sk10,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_16) ).
fof(f15_nnf,plain,
survival_chance(sk4,sk10,sk6),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
survival_chance(sk4,sk10,sk6),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(t7,plain,
survival_chance(sk4,sk10,sk6) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t26,plain,
survival_chance(sk4,sk10,sk6) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t4931,plain,
true = ifeq(true,true,ifeq(survival_chance(sk5,X1,sk7),true,greater(X1,sk10),true),true),
inference(cp,[status(thm)],[t4929,t26]) ).
cnf(t7218,plain,
true = ifeq(survival_chance(sk5,X1,sk7),true,greater(X1,sk10),true),
inference(step,[status(thm)],[t4931,t28]) ).
cnf(t4936,plain,
ifeq(survival_chance(sk5,X1,sk7),true,greater(X1,sk10),true) = true,
inference(orient,[status(thm)],[t7218]) ).
cnf(f16,negated_conjecture,
survival_chance(sk5,sk11,sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_17) ).
fof(f16_nnf,plain,
survival_chance(sk5,sk11,sk7),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
survival_chance(sk5,sk11,sk7),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t8,plain,
survival_chance(sk5,sk11,sk7) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t27,plain,
survival_chance(sk5,sk11,sk7) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t4937,plain,
true = ifeq(true,true,greater(sk11,sk10),true),
inference(cp,[status(thm)],[t4936,t27]) ).
cnf(t7219,plain,
true = greater(sk11,sk10),
inference(step,[status(thm)],[t4937,t28]) ).
cnf(t4938,plain,
greater(sk11,sk10) = true,
inference(orient,[status(thm)],[t7219]) ).
cnf(f18,negated_conjecture,
~ greater(sk11,sk10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_FOL_19) ).
fof(f18_nnf,plain,
~ greater(sk11,sk10),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
~ greater(sk11,sk10),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
~ greater(sk11,sk10),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(goal_0,negated_conjecture,
greater(sk11,sk10) != true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4938]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT001-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n017.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 00:50:53 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 88.32/18.10 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 88.32/18.10 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------