%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : SWV438+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 01:07:01 PM UTC 2026
% Result : Theorem 1.10s 0.44s
% Output : Proof 1.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV438+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.17 % Computer : n009.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 11:07:59 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.10/0.44 Command-line arguments: --no-flatten-goal
% 1.10/0.44
% 1.10/0.44 % SZS status Theorem
% 1.10/0.44
% 1.90/0.49 % SZS output start Proof
% 1.90/0.49 Axiom 1 (ax61): state_file_is_not_working_paper(not_secretfile) = true.
% 1.90/0.49 Axiom 2 (ax65): state_file_has_owner(not_secretfile, owner_not_secretfile) = true.
% 1.90/0.49 Axiom 3 (ax62): system_file_needs_compartments(system, not_secretfile, nil) = true.
% 1.90/0.49 Axiom 4 (ax63): system_file_needs_level(system, not_secretfile, unclassified) = true.
% 1.90/0.49 Axiom 5 (ax64): system_file_needs_citizenship(system, not_secretfile, anycountry) = true.
% 1.90/0.49 Axiom 6 (ax24): admin_indi_has_level(admin, X, unclassified) = true.
% 1.90/0.49 Axiom 7 (ax26): admin_indi_has_compartments(admin, X, nil) = true.
% 1.90/0.49 Axiom 8 (ax85): owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile) = true.
% 1.90/0.49 Axiom 9 (ax22): admin_indi_has_citizenship(admin, X, anycountry) = true.
% 1.90/0.49 Axiom 10 (ax9): admin_file_has_compartments_h(admin, X, Y, nil) = true.
% 1.90/0.49 Axiom 11 (ax12): admin_file_has_level_h(admin, X, Y, nil) = true.
% 1.90/0.49 Axiom 12 (ax15): admin_file_has_citizenship_h(admin, X, Y, nil) = true.
% 1.90/0.49 Axiom 13 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 1.90/0.49 Axiom 14 (ax36): ifeq(owner_indi_has_need_to_know(X, Y, Z), true, ifeq(state_file_has_owner(Z, X), true, admin_indi_has_need_to_know_for_file(admin, Y, Z), true), true) = true.
% 1.90/0.49 Axiom 15 (ax35): ifeq(admin_indi_has_level(admin, X, Y), true, ifeq(admin_file_has_level(admin, Z, Y), true, admin_indi_has_level_for_file(admin, X, Z), true), true) = true.
% 1.90/0.49 Axiom 16 (ax34): ifeq(admin_indi_has_compartments(admin, X, Y), true, ifeq(admin_file_has_compartments(admin, Z, Y), true, admin_indi_has_compartments_for_file(admin, X, Z), true), true) = true.
% 1.90/0.49 Axiom 17 (ax37): ifeq(admin_indi_has_citizenship(admin, X, Y), true, ifeq(admin_file_has_citizenship(admin, Z, Y), true, admin_indi_has_citizenship_for_file(admin, X, Z), true), true) = true.
% 1.90/0.49 Axiom 18 (ax8): ifeq(admin_file_has_compartments_h(admin, X, Y, Y), true, ifeq(system_file_needs_compartments(system, X, Y), true, admin_file_has_compartments(admin, X, Y), true), true) = true.
% 1.90/0.49 Axiom 19 (ax11): ifeq(admin_file_has_level_h(admin, X, Y, Z), true, ifeq(system_file_needs_level(system, X, Y), true, ifeq(admin_file_has_compartments(admin, X, Z), true, admin_file_has_level(admin, X, Y), true), true), true) = true.
% 1.90/0.49 Axiom 20 (ax14): ifeq(admin_file_has_citizenship_h(admin, X, Y, Z), true, ifeq(system_file_needs_citizenship(system, X, Y), true, ifeq(admin_file_has_compartments(admin, X, Z), true, admin_file_has_citizenship(admin, X, Y), true), true), true) = true.
% 1.90/0.49 Axiom 21 (ax39): ifeq(state_file_is_not_working_paper(X), true, ifeq(admin_indi_has_citizenship_for_file(admin, Y, X), true, ifeq(admin_indi_has_need_to_know_for_file(admin, Y, X), true, ifeq(admin_indi_has_level_for_file(admin, Y, X), true, ifeq(admin_indi_has_compartments_for_file(admin, Y, X), true, admin_indi_may_file(admin, Y, X, read), true), true), true), true), true) = true.
% 1.90/0.50
% 1.90/0.50 Goal 1 (babureadnotsecret): admin_indi_may_file(admin, babu, not_secretfile, read) = true.
% 1.90/0.50 Proof:
% 1.90/0.50 admin_indi_may_file(admin, babu, not_secretfile, read)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(true, true, admin_indi_may_file(admin, babu, not_secretfile, read), true)
% 1.90/0.50 = { by axiom 14 (ax36) R->L }
% 1.90/0.50 ifeq(ifeq(owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile), true, ifeq(state_file_has_owner(not_secretfile, owner_not_secretfile), true, admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true)
% 1.90/0.50 = { by axiom 8 (ax85) }
% 1.90/0.50 ifeq(ifeq(true, true, ifeq(state_file_has_owner(not_secretfile, owner_not_secretfile), true, admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(ifeq(state_file_has_owner(not_secretfile, owner_not_secretfile), true, admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true)
% 1.90/0.50 = { by axiom 2 (ax65) }
% 1.90/0.50 ifeq(ifeq(true, true, admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(true, true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 16 (ax34) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_compartments(admin, babu, nil), true, ifeq(admin_file_has_compartments(admin, not_secretfile, nil), true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_compartments(admin, babu, nil), true, ifeq(ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_compartments(admin, babu, nil), true, ifeq(ifeq(true, true, ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 10 (ax9) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_compartments(admin, babu, nil), true, ifeq(ifeq(admin_file_has_compartments_h(admin, not_secretfile, nil, nil), true, ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 3 (ax62) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_compartments(admin, babu, nil), true, ifeq(ifeq(admin_file_has_compartments_h(admin, not_secretfile, nil, nil), true, ifeq(system_file_needs_compartments(system, not_secretfile, nil), true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 18 (ax8) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_compartments(admin, babu, nil), true, ifeq(true, true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 7 (ax26) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(true, true, ifeq(true, true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(true, true, admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(true, true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 15 (ax35) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(admin_file_has_level(admin, not_secretfile, unclassified), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(true, true, admin_file_has_level(admin, not_secretfile, unclassified), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 4 (ax63) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, admin_file_has_level(admin, not_secretfile, unclassified), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(true, true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(true, true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(true, true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 11 (ax12) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(admin_file_has_level_h(admin, not_secretfile, unclassified, nil), true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(true, true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 18 (ax8) R->L }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(admin_file_has_level_h(admin, not_secretfile, unclassified, nil), true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(ifeq(admin_file_has_compartments_h(admin, not_secretfile, nil, nil), true, ifeq(system_file_needs_compartments(system, not_secretfile, nil), true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 3 (ax62) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(admin_file_has_level_h(admin, not_secretfile, unclassified, nil), true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(ifeq(admin_file_has_compartments_h(admin, not_secretfile, nil, nil), true, ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 10 (ax9) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(admin_file_has_level_h(admin, not_secretfile, unclassified, nil), true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(ifeq(true, true, ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(admin_file_has_level_h(admin, not_secretfile, unclassified, nil), true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(ifeq(admin_file_has_level_h(admin, not_secretfile, unclassified, nil), true, ifeq(system_file_needs_level(system, not_secretfile, unclassified), true, ifeq(admin_file_has_compartments(admin, not_secretfile, nil), true, admin_file_has_level(admin, not_secretfile, unclassified), true), true), true), true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 19 (ax11) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(admin_indi_has_level(admin, babu, unclassified), true, ifeq(true, true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 6 (ax24) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(true, true, ifeq(true, true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.50 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(ifeq(true, true, admin_indi_has_level_for_file(admin, babu, not_secretfile), true), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.50 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.51 ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.51 ifeq(true, true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.51 ifeq(true, true, ifeq(true, true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 1 (ax61) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(true, true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 17 (ax37) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(admin_file_has_citizenship(admin, not_secretfile, anycountry), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(true, true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 5 (ax64) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(true, true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(true, true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(true, true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 12 (ax15) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil), true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(true, true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 18 (ax8) R->L }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil), true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(ifeq(admin_file_has_compartments_h(admin, not_secretfile, nil, nil), true, ifeq(system_file_needs_compartments(system, not_secretfile, nil), true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 3 (ax62) }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil), true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(ifeq(admin_file_has_compartments_h(admin, not_secretfile, nil, nil), true, ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 10 (ax9) }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil), true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(ifeq(true, true, ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true), true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil), true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(ifeq(true, true, admin_file_has_compartments(admin, not_secretfile, nil), true), true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.51 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.51 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(ifeq(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil), true, ifeq(system_file_needs_citizenship(system, not_secretfile, anycountry), true, ifeq(admin_file_has_compartments(admin, not_secretfile, nil), true, admin_file_has_citizenship(admin, not_secretfile, anycountry), true), true), true), true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.52 = { by axiom 20 (ax14) }
% 1.90/0.52 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(admin_indi_has_citizenship(admin, babu, anycountry), true, ifeq(true, true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.52 = { by axiom 9 (ax22) }
% 1.90/0.52 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(true, true, ifeq(true, true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.52 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.52 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(ifeq(true, true, admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.52 = { by axiom 13 (ifeq_axiom) }
% 1.90/0.52 ifeq(state_file_is_not_working_paper(not_secretfile), true, ifeq(admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_level_for_file(admin, babu, not_secretfile), true, ifeq(admin_indi_has_compartments_for_file(admin, babu, not_secretfile), true, admin_indi_may_file(admin, babu, not_secretfile, read), true), true), true), true), true)
% 1.90/0.52 = { by axiom 21 (ax39) }
% 1.90/0.52 true
% 1.90/0.52 % SZS output end Proof
% 1.90/0.52
% 1.90/0.52 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------