%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 19:51:04 EDT 2022
% Result : Theorem 0.37s 1.41s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0.
% 0.00/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n016.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 15 14:27:47 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.37/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/1.42
% 0.37/1.42 %-----------------------------------------------------
% 0.37/1.42 fof(babureadnotsecret, conjecture, admin_indi_may_file(admin, babu, not_secretfile, read), file('/export/starexec/sandbox/benchmark/theBenchmark.p', babureadnotsecret)).
% 0.37/1.42 fof(ax61, hypothesis, state_file_is_not_working_paper(not_secretfile), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax61)).
% 0.37/1.42 fof(ax62, hypothesis, system_file_needs_compartments(system, not_secretfile, nil), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax62)).
% 0.37/1.42 fof(ax63, hypothesis, system_file_needs_level(system, not_secretfile, unclassified), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax63)).
% 0.37/1.42 fof(ax64, hypothesis, system_file_needs_citizenship(system, not_secretfile, anycountry), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax64)).
% 0.37/1.42 fof(ax65, hypothesis, state_file_has_owner(not_secretfile, owner_not_secretfile), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax65)).
% 0.37/1.42 fof(ax85, hypothesis, owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax85)).
% 0.37/1.42 fof(ax8, axiom, ! [_76704, _76707] : (system_file_needs_compartments(system, _76704, _76707) => admin_file_has_compartments_h(admin, _76704, _76707, _76707) => admin_file_has_compartments(admin, _76704, _76707)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax8)).
% 0.37/1.42 fof(ax9, axiom, ! [_76906, _76909] : admin_file_has_compartments_h(admin, _76906, _76909, nil), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax9)).
% 0.37/1.42 fof(ax11, axiom, ! [_77039, _77042, _77045] : (system_file_needs_level(system, _77039, _77042) => admin_file_has_compartments(admin, _77039, _77045) => admin_file_has_level_h(admin, _77039, _77042, _77045) => admin_file_has_level(admin, _77039, _77042)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax11)).
% 0.37/1.42 fof(ax12, axiom, ! [_77287, _77290] : admin_file_has_level_h(admin, _77287, _77290, nil), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax12)).
% 0.37/1.42 fof(ax14, axiom, ! [_77420, _77423, _77426] : (system_file_needs_citizenship(system, _77420, _77423) => admin_file_has_compartments(admin, _77420, _77426) => admin_file_has_citizenship_h(admin, _77420, _77423, _77426) => admin_file_has_citizenship(admin, _77420, _77423)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax14)).
% 0.37/1.42 fof(ax15, axiom, ! [_77668, _77671] : admin_file_has_citizenship_h(admin, _77668, _77671, nil), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax15)).
% 0.37/1.42 fof(ax22, axiom, ! [_77806] : admin_indi_has_citizenship(admin, _77806, anycountry), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax22)).
% 0.37/1.42 fof(ax24, axiom, ! [_77921] : admin_indi_has_level(admin, _77921, unclassified), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax24)).
% 0.37/1.42 fof(ax26, axiom, ! [_78036] : admin_indi_has_compartments(admin, _78036, nil), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax26)).
% 0.37/1.42 fof(ax34, axiom, ! [_78157, _78160, _78163] : (admin_file_has_compartments(admin, _78160, _78163) => admin_indi_has_compartments(admin, _78157, _78163) => admin_indi_has_compartments_for_file(admin, _78157, _78160)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax34)).
% 0.37/1.42 fof(ax35, axiom, ! [_78363, _78366, _78369] : (admin_file_has_level(admin, _78366, _78369) => admin_indi_has_level(admin, _78363, _78369) => admin_indi_has_level_for_file(admin, _78363, _78366)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax35)).
% 0.37/1.42 fof(ax36, axiom, ! [_78569, _78572, _78575] : (state_file_has_owner(_78572, _78575) => owner_indi_has_need_to_know(_78575, _78569, _78572) => admin_indi_has_need_to_know_for_file(admin, _78569, _78572)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax36)).
% 0.37/1.42 fof(ax37, axiom, ! [_78768, _78771, _78774] : (admin_file_has_citizenship(admin, _78771, _78774) => admin_indi_has_citizenship(admin, _78768, _78774) => admin_indi_has_citizenship_for_file(admin, _78768, _78771)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax37)).
% 0.37/1.42 fof(ax39, axiom, ! [_78976, _78979] : (state_file_is_not_working_paper(_78979) => admin_indi_has_citizenship_for_file(admin, _78976, _78979) => admin_indi_has_need_to_know_for_file(admin, _78976, _78979) => admin_indi_has_level_for_file(admin, _78976, _78979) => admin_indi_has_compartments_for_file(admin, _78976, _78979) => admin_indi_may_file(admin, _78976, _78979, read)), file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax39)).
% 0.37/1.42
% 0.37/1.42 cnf(1, plain, [admin_indi_may_file(admin, babu, not_secretfile, read)], clausify(babureadnotsecret)).
% 0.37/1.42 cnf(2, plain, [-(state_file_is_not_working_paper(not_secretfile))], clausify(ax61)).
% 0.37/1.42 cnf(3, plain, [-(system_file_needs_compartments(system, not_secretfile, nil))], clausify(ax62)).
% 0.37/1.42 cnf(4, plain, [-(system_file_needs_level(system, not_secretfile, unclassified))], clausify(ax63)).
% 0.37/1.42 cnf(5, plain, [-(system_file_needs_citizenship(system, not_secretfile, anycountry))], clausify(ax64)).
% 0.37/1.42 cnf(6, plain, [-(state_file_has_owner(not_secretfile, owner_not_secretfile))], clausify(ax65)).
% 0.37/1.42 cnf(7, plain, [-(owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile))], clausify(ax85)).
% 0.37/1.42 cnf(8, plain, [system_file_needs_compartments(system, _19768, _19823), admin_file_has_compartments_h(admin, _19768, _19823, _19823), -(admin_file_has_compartments(admin, _19768, _19823))], clausify(ax8)).
% 0.37/1.42 cnf(9, plain, [-(admin_file_has_compartments_h(admin, _20332, _20373, nil))], clausify(ax9)).
% 0.37/1.42 cnf(10, plain, [system_file_needs_level(system, _21702, _21769), admin_file_has_compartments(admin, _21702, _21835), admin_file_has_level_h(admin, _21702, _21769, _21835), -(admin_file_has_level(admin, _21702, _21769))], clausify(ax11)).
% 0.37/1.42 cnf(11, plain, [-(admin_file_has_level_h(admin, _22476, _22517, nil))], clausify(ax12)).
% 0.37/1.42 cnf(12, plain, [system_file_needs_citizenship(system, _24161, _24228), admin_file_has_compartments(admin, _24161, _24294), admin_file_has_citizenship_h(admin, _24161, _24228, _24294), -(admin_file_has_citizenship(admin, _24161, _24228))], clausify(ax14)).
% 0.37/1.42 cnf(13, plain, [-(admin_file_has_citizenship_h(admin, _24935, _24976, nil))], clausify(ax15)).
% 0.37/1.42 cnf(14, plain, [-(admin_indi_has_citizenship(admin, _28800, anycountry))], clausify(ax22)).
% 0.37/1.42 cnf(15, plain, [-(admin_indi_has_level(admin, _29409, unclassified))], clausify(ax24)).
% 0.37/1.42 cnf(16, plain, [-(admin_indi_has_compartments(admin, _31407, nil))], clausify(ax26)).
% 0.37/1.42 cnf(17, plain, [admin_file_has_compartments(admin, _40055, _40113), admin_indi_has_compartments(admin, _39996, _40113), -(admin_indi_has_compartments_for_file(admin, _39996, _40055))], clausify(ax34)).
% 0.37/1.42 cnf(18, plain, [admin_file_has_level(admin, _40651, _40709), admin_indi_has_level(admin, _40592, _40709), -(admin_indi_has_level_for_file(admin, _40592, _40651))], clausify(ax35)).
% 0.37/1.42 cnf(19, plain, [state_file_has_owner(_41246, _41303), owner_indi_has_need_to_know(_41303, _41188, _41246), -(admin_indi_has_need_to_know_for_file(admin, _41188, _41246))], clausify(ax36)).
% 0.37/1.42 cnf(20, plain, [admin_file_has_citizenship(admin, _41800, _41858), admin_indi_has_citizenship(admin, _41741, _41858), -(admin_indi_has_citizenship_for_file(admin, _41741, _41800))], clausify(ax37)).
% 0.37/1.42 cnf(21, plain, [state_file_is_not_working_paper(_42805), admin_indi_has_citizenship_for_file(admin, _42731, _42805), admin_indi_has_need_to_know_for_file(admin, _42731, _42805), admin_indi_has_level_for_file(admin, _42731, _42805), admin_indi_has_compartments_for_file(admin, _42731, _42805), -(admin_indi_may_file(admin, _42731, _42805, read))], clausify(ax39)).
% 0.37/1.42
% 0.37/1.42 cnf('1',plain,[admin_indi_may_file(admin, babu, not_secretfile, read)],start(1)).
% 0.37/1.42 cnf('1.1',plain,[-(admin_indi_may_file(admin, babu, not_secretfile, read)), state_file_is_not_working_paper(not_secretfile), admin_indi_has_citizenship_for_file(admin, babu, not_secretfile), admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile), admin_indi_has_level_for_file(admin, babu, not_secretfile), admin_indi_has_compartments_for_file(admin, babu, not_secretfile)],extension(21,bind([[_42731, _42805], [babu, not_secretfile]]))).
% 0.37/1.42 cnf('1.1.1',plain,[-(state_file_is_not_working_paper(not_secretfile))],extension(2)).
% 0.37/1.42 cnf('1.1.2',plain,[-(admin_indi_has_citizenship_for_file(admin, babu, not_secretfile)), admin_file_has_citizenship(admin, not_secretfile, anycountry), admin_indi_has_citizenship(admin, babu, anycountry)],extension(20,bind([[_41800, _41741, _41858], [not_secretfile, babu, anycountry]]))).
% 0.37/1.42 cnf('1.1.2.1',plain,[-(admin_file_has_citizenship(admin, not_secretfile, anycountry)), system_file_needs_citizenship(system, not_secretfile, anycountry), admin_file_has_compartments(admin, not_secretfile, nil), admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil)],extension(12,bind([[_24161, _24228, _24294], [not_secretfile, anycountry, nil]]))).
% 0.37/1.42 cnf('1.1.2.1.1',plain,[-(system_file_needs_citizenship(system, not_secretfile, anycountry))],extension(5)).
% 0.37/1.42 cnf('1.1.2.1.2',plain,[-(admin_file_has_compartments(admin, not_secretfile, nil)), system_file_needs_compartments(system, not_secretfile, nil), admin_file_has_compartments_h(admin, not_secretfile, nil, nil)],extension(8,bind([[_19768, _19823], [not_secretfile, nil]]))).
% 0.37/1.42 cnf('1.1.2.1.2.1',plain,[-(system_file_needs_compartments(system, not_secretfile, nil))],extension(3)).
% 0.37/1.42 cnf('1.1.2.1.2.2',plain,[-(admin_file_has_compartments_h(admin, not_secretfile, nil, nil))],extension(9,bind([[_20332, _20373], [not_secretfile, nil]]))).
% 0.37/1.42 cnf('1.1.2.1.3',plain,[-(admin_file_has_citizenship_h(admin, not_secretfile, anycountry, nil))],extension(13,bind([[_24935, _24976], [not_secretfile, anycountry]]))).
% 0.37/1.42 cnf('1.1.2.2',plain,[-(admin_indi_has_citizenship(admin, babu, anycountry))],extension(14,bind([[_28800], [babu]]))).
% 0.37/1.42 cnf('1.1.3',plain,[-(admin_indi_has_need_to_know_for_file(admin, babu, not_secretfile)), state_file_has_owner(not_secretfile, owner_not_secretfile), owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile)],extension(19,bind([[_41303, _41188, _41246], [owner_not_secretfile, babu, not_secretfile]]))).
% 0.37/1.42 cnf('1.1.3.1',plain,[-(state_file_has_owner(not_secretfile, owner_not_secretfile))],extension(6)).
% 0.37/1.42 cnf('1.1.3.2',plain,[-(owner_indi_has_need_to_know(owner_not_secretfile, babu, not_secretfile))],extension(7)).
% 0.37/1.42 cnf('1.1.4',plain,[-(admin_indi_has_level_for_file(admin, babu, not_secretfile)), admin_file_has_level(admin, not_secretfile, unclassified), admin_indi_has_level(admin, babu, unclassified)],extension(18,bind([[_40651, _40592, _40709], [not_secretfile, babu, unclassified]]))).
% 0.37/1.42 cnf('1.1.4.1',plain,[-(admin_file_has_level(admin, not_secretfile, unclassified)), system_file_needs_level(system, not_secretfile, unclassified), admin_file_has_compartments(admin, not_secretfile, nil), admin_file_has_level_h(admin, not_secretfile, unclassified, nil)],extension(10,bind([[_21702, _21769, _21835], [not_secretfile, unclassified, nil]]))).
% 0.37/1.42 cnf('1.1.4.1.1',plain,[-(system_file_needs_level(system, not_secretfile, unclassified))],extension(4)).
% 0.37/1.42 cnf('1.1.4.1.2',plain,[-(admin_file_has_compartments(admin, not_secretfile, nil)), system_file_needs_compartments(system, not_secretfile, nil), admin_file_has_compartments_h(admin, not_secretfile, nil, nil)],extension(8,bind([[_19768, _19823], [not_secretfile, nil]]))).
% 0.37/1.42 cnf('1.1.4.1.2.1',plain,[-(system_file_needs_compartments(system, not_secretfile, nil))],extension(3)).
% 0.37/1.42 cnf('1.1.4.1.2.2',plain,[-(admin_file_has_compartments_h(admin, not_secretfile, nil, nil))],extension(9,bind([[_20332, _20373], [not_secretfile, nil]]))).
% 0.37/1.42 cnf('1.1.4.1.3',plain,[-(admin_file_has_level_h(admin, not_secretfile, unclassified, nil))],extension(11,bind([[_22476, _22517], [not_secretfile, unclassified]]))).
% 0.37/1.42 cnf('1.1.4.2',plain,[-(admin_indi_has_level(admin, babu, unclassified))],extension(15,bind([[_29409], [babu]]))).
% 0.37/1.42 cnf('1.1.5',plain,[-(admin_indi_has_compartments_for_file(admin, babu, not_secretfile)), admin_file_has_compartments(admin, not_secretfile, nil), admin_indi_has_compartments(admin, babu, nil)],extension(17,bind([[_40055, _39996, _40113], [not_secretfile, babu, nil]]))).
% 0.37/1.42 cnf('1.1.5.1',plain,[-(admin_file_has_compartments(admin, not_secretfile, nil)), system_file_needs_compartments(system, not_secretfile, nil), admin_file_has_compartments_h(admin, not_secretfile, nil, nil)],extension(8,bind([[_19768, _19823], [not_secretfile, nil]]))).
% 0.37/1.42 cnf('1.1.5.1.1',plain,[-(system_file_needs_compartments(system, not_secretfile, nil))],extension(3)).
% 0.37/1.42 cnf('1.1.5.1.2',plain,[-(admin_file_has_compartments_h(admin, not_secretfile, nil, nil))],extension(9,bind([[_20332, _20373], [not_secretfile, nil]]))).
% 0.37/1.42 cnf('1.1.5.2',plain,[-(admin_indi_has_compartments(admin, babu, nil))],extension(16,bind([[_31407], [babu]]))).
% 0.37/1.42 %-----------------------------------------------------
% 0.37/1.43
% 0.37/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------