%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : MGT001-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 : Tue Sep 29 12:01:41 PM UTC 2026
% Result : Unsatisfiable 81.72s 10.85s
% Output : Proof 84.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT001-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.40 % Computer : n003.cluster.edu
% 0.09/0.40 % Model : x86_64 x86_64
% 0.09/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.40 % Memory : 8046.5625MB
% 0.09/0.40 % OS : Linux 6.8.0-71-generic
% 0.09/0.40 % CPULimit : 300
% 0.09/0.40 % WCLimit : 300
% 0.09/0.40 % DateTime : Sun Sep 27 17:17:11 UTC 2026
% 0.09/0.41 % CPUTime :
% 0.09/0.41 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 81.72/10.85 Command-line arguments: --lhs-weight 1 --flip-ordering --normalise-queue-percent 10 --cp-renormalise-threshold 10 --complete-subsets --ground-joining-incomplete-limit 15 --flatten-every 2
% 81.72/10.85
% 81.72/10.85 % SZS status Unsatisfiable
% 81.72/10.85
% 82.52/11.05 % SZS output start Proof
% 82.52/11.05 Axiom 1 (t1_FOL_10): organization(sk4, sk6) = true.
% 82.52/11.05 Axiom 2 (t1_FOL_11): organization(sk5, sk7) = true.
% 82.52/11.05 Axiom 3 (t1_FOL_18): greater(sk9, sk8) = true.
% 82.52/11.05 Axiom 4 (t1_FOL_12): reorganization_free(sk4, sk6, sk6) = true.
% 82.52/11.05 Axiom 5 (t1_FOL_13): reorganization_free(sk5, sk7, sk7) = true.
% 82.52/11.05 Axiom 6 (t1_FOL_14): inertia(sk4, sk8, sk6) = true.
% 82.52/11.05 Axiom 7 (t1_FOL_15): inertia(sk5, sk9, sk7) = true.
% 82.52/11.05 Axiom 8 (t1_FOL_16): survival_chance(sk4, sk10, sk6) = true.
% 82.52/11.05 Axiom 9 (t1_FOL_17): survival_chance(sk5, sk11, sk7) = true.
% 82.52/11.05 Axiom 10 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 82.52/11.05 Axiom 11 (mp3_3): ifeq(organization(X, Y), true, reproducibility(X, sk3(Y, X), Y), true) = true.
% 82.52/11.05 Axiom 12 (mp1_1): ifeq(organization(X, Y), true, reliability(X, sk1(Y, X), Y), true) = true.
% 82.52/11.05 Axiom 13 (mp2_2): ifeq(organization(X, Y), true, accountability(X, sk2(Y, X), Y), true) = true.
% 82.52/11.05 Axiom 14 (a2_FOL_6): ifeq(greater(X, Y), true, ifeq(reproducibility(Z, X, W), true, ifeq(reproducibility(V, Y, U), true, ifeq(accountability(Z, T, W), true, ifeq(accountability(V, S, U), true, ifeq(reliability(Z, X2, W), true, ifeq(reliability(V, Y2, U), true, ifeq(organization(Z, W), true, ifeq(organization(V, U), true, greater(T, S), true), true), true), true), true), true), true), true), true) = true.
% 82.52/11.05 Axiom 15 (a2_FOL_5): ifeq(greater(X, Y), true, ifeq(reproducibility(Z, X, W), true, ifeq(reproducibility(V, Y, U), true, ifeq(accountability(Z, T, W), true, ifeq(accountability(V, S, U), true, ifeq(reliability(Z, X2, W), true, ifeq(reliability(V, Y2, U), true, ifeq(organization(Z, W), true, ifeq(organization(V, U), true, greater(X2, Y2), true), true), true), true), true), true), true), true), true) = true.
% 82.52/11.05 Axiom 16 (a3_FOL_9): ifeq(inertia(X, Y, Z), true, ifeq(inertia(W, V, U), true, ifeq(reorganization_free(X, Z, Z), true, ifeq(reorganization_free(W, U, U), true, ifeq(greater(Y, V), true, ifeq(reproducibility(X, T, Z), true, ifeq(reproducibility(W, S, U), true, ifeq(organization(X, Z), true, ifeq(organization(W, U), true, greater(T, S), true), true), true), true), true), true), true), true), true) = true.
% 82.52/11.06 Axiom 17 (a1_FOL_4): ifeq(greater(X, Y), true, ifeq(greater(Z, W), true, ifeq(survival_chance(V, U, T), true, ifeq(survival_chance(S, X2, Y2), true, ifeq(accountability(V, X, T), true, ifeq(accountability(S, Y, Y2), true, ifeq(reliability(V, Z, T), true, ifeq(reliability(S, W, Y2), true, ifeq(organization(V, T), true, ifeq(organization(S, Y2), true, greater(U, X2), true), true), true), true), true), true), true), true), true), true) = true.
% 82.52/11.06
% 82.52/11.06 Goal 1 (t1_FOL_19): greater(sk11, sk10) = true.
% 82.52/11.06 Proof:
% 82.52/11.06 greater(sk11, sk10)
% 82.52/11.06 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.06 ifeq(true, true, greater(sk11, sk10), true)
% 82.52/11.06 = { by axiom 12 (mp1_1) R->L }
% 82.52/11.06 ifeq(ifeq(organization(sk4, sk6), true, reliability(sk4, sk1(sk6, sk4), sk6), true), true, greater(sk11, sk10), true)
% 82.52/11.06 = { by axiom 1 (t1_FOL_10) }
% 82.52/11.06 ifeq(ifeq(true, true, reliability(sk4, sk1(sk6, sk4), sk6), true), true, greater(sk11, sk10), true)
% 82.52/11.06 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.06 ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true)
% 82.52/11.06 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.06 ifeq(true, true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true)
% 82.52/11.06 = { by axiom 12 (mp1_1) R->L }
% 82.52/11.06 ifeq(ifeq(organization(sk5, sk7), true, reliability(sk5, sk1(sk7, sk5), sk7), true), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true)
% 82.52/11.06 = { by axiom 2 (t1_FOL_11) }
% 82.52/11.06 ifeq(ifeq(true, true, reliability(sk5, sk1(sk7, sk5), sk7), true), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true)
% 82.52/11.06 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.06 ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true)
% 82.52/11.06 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.06 ifeq(true, true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.06 = { by axiom 15 (a2_FOL_5) R->L }
% 82.52/11.06 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.06 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.06 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(ifeq(true, true, accountability(sk4, sk2(sk6, sk4), sk6), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.06 = { by axiom 1 (t1_FOL_10) R->L }
% 82.52/11.06 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(ifeq(organization(sk4, sk6), true, accountability(sk4, sk2(sk6, sk4), sk6), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.06 = { by axiom 13 (mp2_2) }
% 82.52/11.06 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(true, true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.07 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.07 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.07 = { by axiom 1 (t1_FOL_10) }
% 82.52/11.07 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(true, true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.07 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.07 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.07 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.07 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(ifeq(true, true, accountability(sk5, sk2(sk7, sk5), sk7), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.07 = { by axiom 2 (t1_FOL_11) R->L }
% 82.52/11.07 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(ifeq(organization(sk5, sk7), true, accountability(sk5, sk2(sk7, sk5), sk7), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 13 (mp2_2) }
% 82.52/11.08 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(true, true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.08 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 2 (t1_FOL_11) }
% 82.52/11.08 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(true, true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.08 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 11 (mp3_3) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(ifeq(organization(sk5, sk7), true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 2 (t1_FOL_11) }
% 82.52/11.08 ifeq(ifeq(ifeq(ifeq(true, true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 11 (mp3_3) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(ifeq(organization(sk4, sk6), true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 1 (t1_FOL_10) }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(ifeq(true, true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 2 (t1_FOL_11) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(true, true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 3 (t1_FOL_18) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(true, true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.08 = { by axiom 5 (t1_FOL_13) R->L }
% 82.52/11.08 ifeq(ifeq(ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(true, true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 7 (t1_FOL_15) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 1 (t1_FOL_10) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(true, true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 4 (t1_FOL_12) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(reorganization_free(sk4, sk6, sk6), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(true, true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(reorganization_free(sk4, sk6, sk6), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 6 (t1_FOL_14) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(inertia(sk4, sk8, sk6), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(reorganization_free(sk4, sk6, sk6), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 16 (a3_FOL_9) }
% 82.52/11.09 ifeq(ifeq(true, true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.09 ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(true, true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 2 (t1_FOL_11) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(organization(sk5, sk7), true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 11 (mp3_3) }
% 82.52/11.09 ifeq(ifeq(true, true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.09 ifeq(ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(true, true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 1 (t1_FOL_10) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(organization(sk4, sk6), true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 11 (mp3_3) }
% 82.52/11.09 ifeq(ifeq(true, true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.09 ifeq(ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(ifeq(true, true, reliability(sk4, sk1(sk6, sk4), sk6), true), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 1 (t1_FOL_10) R->L }
% 82.52/11.09 ifeq(ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(ifeq(organization(sk4, sk6), true, reliability(sk4, sk1(sk6, sk4), sk6), true), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 12 (mp1_1) }
% 82.52/11.09 ifeq(ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(true, true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.09 ifeq(ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(true, true, reliability(sk5, sk1(sk7, sk5), sk7), true), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 2 (t1_FOL_11) R->L }
% 82.52/11.09 ifeq(ifeq(ifeq(organization(sk5, sk7), true, reliability(sk5, sk1(sk7, sk5), sk7), true), true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 12 (mp1_1) }
% 82.52/11.09 ifeq(ifeq(true, true, greater(sk1(sk7, sk5), sk1(sk6, sk4)), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.09 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true)
% 82.52/11.09 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.09 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(true, true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true)
% 82.52/11.10 = { by axiom 13 (mp2_2) R->L }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(ifeq(organization(sk4, sk6), true, accountability(sk4, sk2(sk6, sk4), sk6), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true)
% 82.52/11.10 = { by axiom 1 (t1_FOL_10) }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(ifeq(true, true, accountability(sk4, sk2(sk6, sk4), sk6), true), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(true, true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true)
% 82.52/11.10 = { by axiom 13 (mp2_2) R->L }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(ifeq(organization(sk5, sk7), true, accountability(sk5, sk2(sk7, sk5), sk7), true), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true)
% 82.52/11.10 = { by axiom 2 (t1_FOL_11) }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(ifeq(true, true, accountability(sk5, sk2(sk7, sk5), sk7), true), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.10 ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.10 ifeq(true, true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 14 (a2_FOL_6) R->L }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(ifeq(true, true, reliability(sk4, sk1(sk6, sk4), sk6), true), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 1 (t1_FOL_10) R->L }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(ifeq(organization(sk4, sk6), true, reliability(sk4, sk1(sk6, sk4), sk6), true), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 12 (mp1_1) }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(true, true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 1 (t1_FOL_10) }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(organization(sk5, sk7), true, ifeq(true, true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(organization(sk5, sk7), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(ifeq(true, true, reliability(sk5, sk1(sk7, sk5), sk7), true), true, ifeq(organization(sk5, sk7), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.10 = { by axiom 2 (t1_FOL_11) R->L }
% 82.52/11.10 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(ifeq(organization(sk5, sk7), true, reliability(sk5, sk1(sk7, sk5), sk7), true), true, ifeq(organization(sk5, sk7), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 12 (mp1_1) }
% 82.52/11.11 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(true, true, ifeq(organization(sk5, sk7), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.11 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 2 (t1_FOL_11) }
% 82.52/11.11 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(true, true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.11 ifeq(ifeq(greater(sk3(sk7, sk5), sk3(sk6, sk4)), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 11 (mp3_3) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(ifeq(organization(sk5, sk7), true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 2 (t1_FOL_11) }
% 82.52/11.11 ifeq(ifeq(ifeq(ifeq(true, true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 11 (mp3_3) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(ifeq(organization(sk4, sk6), true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 1 (t1_FOL_10) }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(ifeq(true, true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 2 (t1_FOL_11) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(true, true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 3 (t1_FOL_18) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 10 (ifeq_axiom) R->L }
% 82.52/11.11 ifeq(ifeq(ifeq(true, true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.11 = { by axiom 5 (t1_FOL_13) R->L }
% 82.52/11.12 ifeq(ifeq(ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 82.52/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(true, true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 7 (t1_FOL_15) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(true, true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 1 (t1_FOL_10) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(true, true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 4 (t1_FOL_12) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(reorganization_free(sk4, sk6, sk6), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(true, true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(reorganization_free(sk4, sk6, sk6), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 6 (t1_FOL_14) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(inertia(sk5, sk9, sk7), true, ifeq(inertia(sk4, sk8, sk6), true, ifeq(reorganization_free(sk5, sk7, sk7), true, ifeq(reorganization_free(sk4, sk6, sk6), true, ifeq(greater(sk9, sk8), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk3(sk7, sk5), sk3(sk6, sk4)), true), true), true), true), true), true), true), true), true), true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 16 (a3_FOL_9) }
% 84.06/11.12 ifeq(ifeq(true, true, ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) }
% 84.06/11.12 ifeq(ifeq(reproducibility(sk5, sk3(sk7, sk5), sk7), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(true, true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 2 (t1_FOL_11) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(organization(sk5, sk7), true, reproducibility(sk5, sk3(sk7, sk5), sk7), true), true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 11 (mp3_3) }
% 84.06/11.12 ifeq(ifeq(true, true, ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) }
% 84.06/11.12 ifeq(ifeq(reproducibility(sk4, sk3(sk6, sk4), sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(true, true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 1 (t1_FOL_10) R->L }
% 84.06/11.12 ifeq(ifeq(ifeq(organization(sk4, sk6), true, reproducibility(sk4, sk3(sk6, sk4), sk6), true), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 11 (mp3_3) }
% 84.06/11.12 ifeq(ifeq(true, true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) }
% 84.06/11.12 ifeq(ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.12 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.12 ifeq(ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(ifeq(true, true, accountability(sk4, sk2(sk6, sk4), sk6), true), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 1 (t1_FOL_10) R->L }
% 84.06/11.13 ifeq(ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(ifeq(organization(sk4, sk6), true, accountability(sk4, sk2(sk6, sk4), sk6), true), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 13 (mp2_2) }
% 84.06/11.13 ifeq(ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(true, true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) }
% 84.06/11.13 ifeq(ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.13 ifeq(ifeq(ifeq(true, true, accountability(sk5, sk2(sk7, sk5), sk7), true), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 2 (t1_FOL_11) R->L }
% 84.06/11.13 ifeq(ifeq(ifeq(organization(sk5, sk7), true, accountability(sk5, sk2(sk7, sk5), sk7), true), true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 13 (mp2_2) }
% 84.06/11.13 ifeq(ifeq(true, true, greater(sk2(sk7, sk5), sk2(sk6, sk4)), true), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, greater(sk11, sk10), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(true, true, greater(sk11, sk10), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 2 (t1_FOL_11) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk11, sk10), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(true, true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk11, sk10), true), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 9 (t1_FOL_17) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(survival_chance(sk5, sk11, sk7), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, greater(sk11, sk10), true), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(survival_chance(sk5, sk11, sk7), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(true, true, greater(sk11, sk10), true), true), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 1 (t1_FOL_10) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(survival_chance(sk5, sk11, sk7), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk11, sk10), true), true), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 10 (ifeq_axiom) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(survival_chance(sk5, sk11, sk7), true, ifeq(true, true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk11, sk10), true), true), true), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 8 (t1_FOL_16) R->L }
% 84.06/11.13 ifeq(greater(sk2(sk7, sk5), sk2(sk6, sk4)), true, ifeq(greater(sk1(sk7, sk5), sk1(sk6, sk4)), true, ifeq(survival_chance(sk5, sk11, sk7), true, ifeq(survival_chance(sk4, sk10, sk6), true, ifeq(accountability(sk5, sk2(sk7, sk5), sk7), true, ifeq(accountability(sk4, sk2(sk6, sk4), sk6), true, ifeq(reliability(sk5, sk1(sk7, sk5), sk7), true, ifeq(reliability(sk4, sk1(sk6, sk4), sk6), true, ifeq(organization(sk5, sk7), true, ifeq(organization(sk4, sk6), true, greater(sk11, sk10), true), true), true), true), true), true), true), true), true), true)
% 84.06/11.13 = { by axiom 17 (a1_FOL_4) }
% 84.06/11.13 true
% 84.06/11.13 % SZS output end Proof
% 84.06/11.13
% 84.06/11.13 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------