%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV438+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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 : 300s
% DateTime : Thu May 9 17:45:02 EDT 2024
% Result : Theorem 0.61s 0.81s
% Output : Refutation 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV438+1 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n002.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 9 06:01:53 EDT 2024
% 0.15/0.35 % CPUTime :
% 0.61/0.81 % Version: 1.5
% 0.61/0.81 % SZS status Theorem
% 0.61/0.81 % SZS output start CNFRefutation
% 0.61/0.81 fof(babureadnotsecret,conjecture,admin_indi_may_file(admin,babu,not_secretfile,read),file('/export/starexec/sandbox/benchmark/theBenchmark.p', babureadnotsecret)).
% 0.61/0.81 fof(c0,negated_conjecture,(~admin_indi_may_file(admin,babu,not_secretfile,read)),inference(assume_negation,[status(cth)],[babureadnotsecret])).
% 0.61/0.81 fof(c1,negated_conjecture,~admin_indi_may_file(admin,babu,not_secretfile,read),inference(fof_simplification,[status(thm)],[c0])).
% 0.61/0.81 cnf(c2,negated_conjecture,~admin_indi_may_file(admin,babu,not_secretfile,read),inference(split_conjunct,[status(thm)],[c1])).
% 0.61/0.81 fof(ax61,plain,state_file_is_not_working_paper(not_secretfile),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax61)).
% 0.61/0.81 cnf(c28,plain,state_file_is_not_working_paper(not_secretfile),inference(split_conjunct,[status(thm)],[ax61])).
% 0.61/0.81 fof(ax22,axiom,(![K]:admin_indi_has_citizenship(admin,K,anycountry)),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax22)).
% 0.61/0.81 fof(c119,plain,(![X72]:admin_indi_has_citizenship(admin,X72,anycountry)),inference(variable_rename,[status(thm)],[ax22])).
% 0.61/0.81 cnf(c120,plain,admin_indi_has_citizenship(admin,X135,anycountry),inference(split_conjunct,[status(thm)],[c119])).
% 0.61/0.81 fof(ax37,axiom,(![K]:(![F]:(![L]:(admin_file_has_citizenship(admin,F,L)=>(admin_indi_has_citizenship(admin,K,L)=>admin_indi_has_citizenship_for_file(admin,K,F)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax37)).
% 0.61/0.81 fof(c60,plain,(![K]:(![F]:(![L]:(~admin_file_has_citizenship(admin,F,L)|(~admin_indi_has_citizenship(admin,K,L)|admin_indi_has_citizenship_for_file(admin,K,F)))))),inference(fof_nnf,[status(thm)],[ax37])).
% 0.61/0.81 fof(c61,plain,(![X9]:(![X10]:(![X11]:(~admin_file_has_citizenship(admin,X10,X11)|(~admin_indi_has_citizenship(admin,X9,X11)|admin_indi_has_citizenship_for_file(admin,X9,X10)))))),inference(variable_rename,[status(thm)],[c60])).
% 0.61/0.81 cnf(c62,plain,~admin_file_has_citizenship(admin,X179,X178)|~admin_indi_has_citizenship(admin,X177,X178)|admin_indi_has_citizenship_for_file(admin,X177,X179),inference(split_conjunct,[status(thm)],[c61])).
% 0.61/0.81 cnf(c215,plain,~admin_file_has_citizenship(admin,X222,anycountry)|admin_indi_has_citizenship_for_file(admin,X221,X222),inference(resolution,[status(thm)],[c62, c120])).
% 0.61/0.81 fof(ax64,plain,system_file_needs_citizenship(system,not_secretfile,anycountry),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax64)).
% 0.61/0.81 cnf(c25,plain,system_file_needs_citizenship(system,not_secretfile,anycountry),inference(split_conjunct,[status(thm)],[ax64])).
% 0.61/0.81 fof(ax62,plain,system_file_needs_compartments(system,not_secretfile,nil),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax62)).
% 0.61/0.81 cnf(c27,plain,system_file_needs_compartments(system,not_secretfile,nil),inference(split_conjunct,[status(thm)],[ax62])).
% 0.61/0.81 fof(ax9,axiom,(![F]:(![CL]:admin_file_has_compartments_h(admin,F,CL,nil))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax9)).
% 0.61/0.81 fof(c164,plain,(![X111]:(![X112]:admin_file_has_compartments_h(admin,X111,X112,nil))),inference(variable_rename,[status(thm)],[ax9])).
% 0.61/0.81 cnf(c165,plain,admin_file_has_compartments_h(admin,X145,X146,nil),inference(split_conjunct,[status(thm)],[c164])).
% 0.61/0.81 fof(ax8,axiom,(![F]:(![CL]:(system_file_needs_compartments(system,F,CL)=>(admin_file_has_compartments_h(admin,F,CL,CL)=>admin_file_has_compartments(admin,F,CL))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax8)).
% 0.61/0.81 fof(c166,plain,(![F]:(![CL]:(~system_file_needs_compartments(system,F,CL)|(~admin_file_has_compartments_h(admin,F,CL,CL)|admin_file_has_compartments(admin,F,CL))))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.61/0.81 fof(c167,plain,(![X113]:(![X114]:(~system_file_needs_compartments(system,X113,X114)|(~admin_file_has_compartments_h(admin,X113,X114,X114)|admin_file_has_compartments(admin,X113,X114))))),inference(variable_rename,[status(thm)],[c166])).
% 0.61/0.81 cnf(c168,plain,~system_file_needs_compartments(system,X253,X254)|~admin_file_has_compartments_h(admin,X253,X254,X254)|admin_file_has_compartments(admin,X253,X254),inference(split_conjunct,[status(thm)],[c167])).
% 0.61/0.81 cnf(c244,plain,~system_file_needs_compartments(system,X262,nil)|admin_file_has_compartments(admin,X262,nil),inference(resolution,[status(thm)],[c168, c165])).
% 0.61/0.81 cnf(c247,plain,admin_file_has_compartments(admin,not_secretfile,nil),inference(resolution,[status(thm)],[c244, c27])).
% 0.61/0.81 fof(ax15,axiom,(![F]:(![U]:admin_file_has_citizenship_h(admin,F,U,nil))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax15)).
% 0.61/0.81 fof(c142,plain,(![X90]:(![X91]:admin_file_has_citizenship_h(admin,X90,X91,nil))),inference(variable_rename,[status(thm)],[ax15])).
% 0.61/0.81 cnf(c143,plain,admin_file_has_citizenship_h(admin,X142,X141,nil),inference(split_conjunct,[status(thm)],[c142])).
% 0.61/0.81 fof(ax14,axiom,(![F]:(![U]:(![CL]:(system_file_needs_citizenship(system,F,U)=>(admin_file_has_compartments(admin,F,CL)=>(admin_file_has_citizenship_h(admin,F,U,CL)=>admin_file_has_citizenship(admin,F,U))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax14)).
% 0.61/0.81 fof(c144,plain,(![F]:(![U]:(![CL]:(~system_file_needs_citizenship(system,F,U)|(~admin_file_has_compartments(admin,F,CL)|(~admin_file_has_citizenship_h(admin,F,U,CL)|admin_file_has_citizenship(admin,F,U))))))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.61/0.81 fof(c145,plain,(![F]:(![U]:(~system_file_needs_citizenship(system,F,U)|(![CL]:(~admin_file_has_compartments(admin,F,CL)|(~admin_file_has_citizenship_h(admin,F,U,CL)|admin_file_has_citizenship(admin,F,U))))))),inference(shift_quantors,[status(thm)],[c144])).
% 0.61/0.81 fof(c147,plain,(![X92]:(![X93]:(![X94]:(~system_file_needs_citizenship(system,X92,X93)|(~admin_file_has_compartments(admin,X92,X94)|(~admin_file_has_citizenship_h(admin,X92,X93,X94)|admin_file_has_citizenship(admin,X92,X93))))))),inference(shift_quantors,[status(thm)],[fof(c146,plain,(![X92]:(![X93]:(~system_file_needs_citizenship(system,X92,X93)|(![X94]:(~admin_file_has_compartments(admin,X92,X94)|(~admin_file_has_citizenship_h(admin,X92,X93,X94)|admin_file_has_citizenship(admin,X92,X93))))))),inference(variable_rename,[status(thm)],[c145])).])).
% 0.61/0.81 cnf(c148,plain,~system_file_needs_citizenship(system,X312,X313)|~admin_file_has_compartments(admin,X312,X311)|~admin_file_has_citizenship_h(admin,X312,X313,X311)|admin_file_has_citizenship(admin,X312,X313),inference(split_conjunct,[status(thm)],[c147])).
% 0.61/0.81 cnf(c279,plain,~system_file_needs_citizenship(system,X328,X329)|~admin_file_has_compartments(admin,X328,nil)|admin_file_has_citizenship(admin,X328,X329),inference(resolution,[status(thm)],[c148, c143])).
% 0.61/0.81 cnf(c284,plain,~system_file_needs_citizenship(system,not_secretfile,X330)|admin_file_has_citizenship(admin,not_secretfile,X330),inference(resolution,[status(thm)],[c279, c247])).
% 0.61/0.81 cnf(c285,plain,admin_file_has_citizenship(admin,not_secretfile,anycountry),inference(resolution,[status(thm)],[c284, c25])).
% 0.61/0.81 cnf(c286,plain,admin_indi_has_citizenship_for_file(admin,X331,not_secretfile),inference(resolution,[status(thm)],[c285, c215])).
% 0.61/0.81 fof(ax65,plain,state_file_has_owner(not_secretfile,owner_not_secretfile),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax65)).
% 0.61/0.81 cnf(c24,plain,state_file_has_owner(not_secretfile,owner_not_secretfile),inference(split_conjunct,[status(thm)],[ax65])).
% 0.61/0.81 fof(ax85,plain,owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax85)).
% 0.61/0.81 cnf(c4,plain,owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),inference(split_conjunct,[status(thm)],[ax85])).
% 0.61/0.81 fof(ax36,axiom,(![K]:(![F]:(![OWR]:(state_file_has_owner(F,OWR)=>(owner_indi_has_need_to_know(OWR,K,F)=>admin_indi_has_need_to_know_for_file(admin,K,F)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax36)).
% 0.61/0.81 fof(c63,plain,(![K]:(![F]:(![OWR]:(~state_file_has_owner(F,OWR)|(~owner_indi_has_need_to_know(OWR,K,F)|admin_indi_has_need_to_know_for_file(admin,K,F)))))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.61/0.81 fof(c64,plain,(![X12]:(![X13]:(![X14]:(~state_file_has_owner(X13,X14)|(~owner_indi_has_need_to_know(X14,X12,X13)|admin_indi_has_need_to_know_for_file(admin,X12,X13)))))),inference(variable_rename,[status(thm)],[c63])).
% 0.61/0.82 cnf(c65,plain,~state_file_has_owner(X160,X162)|~owner_indi_has_need_to_know(X162,X161,X160)|admin_indi_has_need_to_know_for_file(admin,X161,X160),inference(split_conjunct,[status(thm)],[c64])).
% 0.61/0.82 cnf(c202,plain,~state_file_has_owner(not_secretfile,owner_not_secretfile)|admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile),inference(resolution,[status(thm)],[c65, c4])).
% 0.61/0.82 cnf(c205,plain,admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile),inference(resolution,[status(thm)],[c202, c24])).
% 0.61/0.82 fof(ax24,axiom,(![K]:admin_indi_has_level(admin,K,unclassified)),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax24)).
% 0.61/0.82 fof(c114,plain,(![X69]:admin_indi_has_level(admin,X69,unclassified)),inference(variable_rename,[status(thm)],[ax24])).
% 0.61/0.82 cnf(c115,plain,admin_indi_has_level(admin,X134,unclassified),inference(split_conjunct,[status(thm)],[c114])).
% 0.61/0.82 fof(ax35,axiom,(![K]:(![F]:(![L]:(admin_file_has_level(admin,F,L)=>(admin_indi_has_level(admin,K,L)=>admin_indi_has_level_for_file(admin,K,F)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax35)).
% 0.61/0.82 fof(c66,plain,(![K]:(![F]:(![L]:(~admin_file_has_level(admin,F,L)|(~admin_indi_has_level(admin,K,L)|admin_indi_has_level_for_file(admin,K,F)))))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.61/0.82 fof(c67,plain,(![X15]:(![X16]:(![X17]:(~admin_file_has_level(admin,X16,X17)|(~admin_indi_has_level(admin,X15,X17)|admin_indi_has_level_for_file(admin,X15,X16)))))),inference(variable_rename,[status(thm)],[c66])).
% 0.61/0.82 cnf(c68,plain,~admin_file_has_level(admin,X187,X188)|~admin_indi_has_level(admin,X186,X188)|admin_indi_has_level_for_file(admin,X186,X187),inference(split_conjunct,[status(thm)],[c67])).
% 0.61/0.82 cnf(c222,plain,~admin_file_has_level(admin,X230,unclassified)|admin_indi_has_level_for_file(admin,X229,X230),inference(resolution,[status(thm)],[c68, c115])).
% 0.61/0.82 fof(ax63,plain,system_file_needs_level(system,not_secretfile,unclassified),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax63)).
% 0.61/0.82 cnf(c26,plain,system_file_needs_level(system,not_secretfile,unclassified),inference(split_conjunct,[status(thm)],[ax63])).
% 0.61/0.82 fof(ax12,axiom,(![F]:(![L]:admin_file_has_level_h(admin,F,L,nil))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax12)).
% 0.61/0.82 fof(c154,plain,(![X101]:(![X102]:admin_file_has_level_h(admin,X101,X102,nil))),inference(variable_rename,[status(thm)],[ax12])).
% 0.61/0.82 cnf(c155,plain,admin_file_has_level_h(admin,X144,X143,nil),inference(split_conjunct,[status(thm)],[c154])).
% 0.61/0.82 fof(ax11,axiom,(![F]:(![L]:(![CL]:(system_file_needs_level(system,F,L)=>(admin_file_has_compartments(admin,F,CL)=>(admin_file_has_level_h(admin,F,L,CL)=>admin_file_has_level(admin,F,L))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax11)).
% 0.61/0.82 fof(c156,plain,(![F]:(![L]:(![CL]:(~system_file_needs_level(system,F,L)|(~admin_file_has_compartments(admin,F,CL)|(~admin_file_has_level_h(admin,F,L,CL)|admin_file_has_level(admin,F,L))))))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.61/0.82 fof(c157,plain,(![F]:(![L]:(~system_file_needs_level(system,F,L)|(![CL]:(~admin_file_has_compartments(admin,F,CL)|(~admin_file_has_level_h(admin,F,L,CL)|admin_file_has_level(admin,F,L))))))),inference(shift_quantors,[status(thm)],[c156])).
% 0.61/0.82 fof(c159,plain,(![X103]:(![X104]:(![X105]:(~system_file_needs_level(system,X103,X104)|(~admin_file_has_compartments(admin,X103,X105)|(~admin_file_has_level_h(admin,X103,X104,X105)|admin_file_has_level(admin,X103,X104))))))),inference(shift_quantors,[status(thm)],[fof(c158,plain,(![X103]:(![X104]:(~system_file_needs_level(system,X103,X104)|(![X105]:(~admin_file_has_compartments(admin,X103,X105)|(~admin_file_has_level_h(admin,X103,X104,X105)|admin_file_has_level(admin,X103,X104))))))),inference(variable_rename,[status(thm)],[c157])).])).
% 0.61/0.82 cnf(c160,plain,~system_file_needs_level(system,X333,X332)|~admin_file_has_compartments(admin,X333,X334)|~admin_file_has_level_h(admin,X333,X332,X334)|admin_file_has_level(admin,X333,X332),inference(split_conjunct,[status(thm)],[c159])).
% 0.61/0.82 cnf(c287,plain,~system_file_needs_level(system,X335,X336)|~admin_file_has_compartments(admin,X335,nil)|admin_file_has_level(admin,X335,X336),inference(resolution,[status(thm)],[c160, c155])).
% 0.61/0.82 cnf(c288,plain,~system_file_needs_level(system,not_secretfile,X337)|admin_file_has_level(admin,not_secretfile,X337),inference(resolution,[status(thm)],[c287, c247])).
% 0.61/0.82 cnf(c289,plain,admin_file_has_level(admin,not_secretfile,unclassified),inference(resolution,[status(thm)],[c288, c26])).
% 0.61/0.82 cnf(c290,plain,admin_indi_has_level_for_file(admin,X338,not_secretfile),inference(resolution,[status(thm)],[c289, c222])).
% 0.61/0.82 fof(ax39,axiom,(![K]:(![F]:(state_file_is_not_working_paper(F)=>(admin_indi_has_citizenship_for_file(admin,K,F)=>(admin_indi_has_need_to_know_for_file(admin,K,F)=>(admin_indi_has_level_for_file(admin,K,F)=>(admin_indi_has_compartments_for_file(admin,K,F)=>admin_indi_may_file(admin,K,F,read)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax39)).
% 0.61/0.82 fof(c52,plain,(![K]:(![F]:(~state_file_is_not_working_paper(F)|(~admin_indi_has_citizenship_for_file(admin,K,F)|(~admin_indi_has_need_to_know_for_file(admin,K,F)|(~admin_indi_has_level_for_file(admin,K,F)|(~admin_indi_has_compartments_for_file(admin,K,F)|admin_indi_may_file(admin,K,F,read)))))))),inference(fof_nnf,[status(thm)],[ax39])).
% 0.61/0.82 fof(c53,plain,(![X5]:(![X6]:(~state_file_is_not_working_paper(X6)|(~admin_indi_has_citizenship_for_file(admin,X5,X6)|(~admin_indi_has_need_to_know_for_file(admin,X5,X6)|(~admin_indi_has_level_for_file(admin,X5,X6)|(~admin_indi_has_compartments_for_file(admin,X5,X6)|admin_indi_may_file(admin,X5,X6,read)))))))),inference(variable_rename,[status(thm)],[c52])).
% 0.61/0.82 cnf(c54,plain,~state_file_is_not_working_paper(X166)|~admin_indi_has_citizenship_for_file(admin,X167,X166)|~admin_indi_has_need_to_know_for_file(admin,X167,X166)|~admin_indi_has_level_for_file(admin,X167,X166)|~admin_indi_has_compartments_for_file(admin,X167,X166)|admin_indi_may_file(admin,X167,X166,read),inference(split_conjunct,[status(thm)],[c53])).
% 0.61/0.82 fof(ax26,axiom,(![K]:admin_indi_has_compartments(admin,K,nil)),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax26)).
% 0.61/0.82 fof(c107,plain,(![X63]:admin_indi_has_compartments(admin,X63,nil)),inference(variable_rename,[status(thm)],[ax26])).
% 0.61/0.82 cnf(c108,plain,admin_indi_has_compartments(admin,X133,nil),inference(split_conjunct,[status(thm)],[c107])).
% 0.61/0.82 fof(ax34,axiom,(![K]:(![F]:(![CL]:(admin_file_has_compartments(admin,F,CL)=>(admin_indi_has_compartments(admin,K,CL)=>admin_indi_has_compartments_for_file(admin,K,F)))))),file('/export/starexec/sandbox/benchmark/Axioms/SWV009+0.ax', ax34)).
% 0.61/0.82 fof(c69,plain,(![K]:(![F]:(![CL]:(~admin_file_has_compartments(admin,F,CL)|(~admin_indi_has_compartments(admin,K,CL)|admin_indi_has_compartments_for_file(admin,K,F)))))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.61/0.82 fof(c70,plain,(![X18]:(![X19]:(![X20]:(~admin_file_has_compartments(admin,X19,X20)|(~admin_indi_has_compartments(admin,X18,X20)|admin_indi_has_compartments_for_file(admin,X18,X19)))))),inference(variable_rename,[status(thm)],[c69])).
% 0.61/0.82 cnf(c71,plain,~admin_file_has_compartments(admin,X199,X197)|~admin_indi_has_compartments(admin,X198,X197)|admin_indi_has_compartments_for_file(admin,X198,X199),inference(split_conjunct,[status(thm)],[c70])).
% 0.61/0.82 cnf(c227,plain,~admin_file_has_compartments(admin,X231,nil)|admin_indi_has_compartments_for_file(admin,X232,X231),inference(resolution,[status(thm)],[c71, c108])).
% 0.61/0.82 cnf(c248,plain,admin_indi_has_compartments_for_file(admin,X263,not_secretfile),inference(resolution,[status(thm)],[c247, c227])).
% 0.61/0.82 cnf(c249,plain,~state_file_is_not_working_paper(not_secretfile)|~admin_indi_has_citizenship_for_file(admin,X354,not_secretfile)|~admin_indi_has_need_to_know_for_file(admin,X354,not_secretfile)|~admin_indi_has_level_for_file(admin,X354,not_secretfile)|admin_indi_may_file(admin,X354,not_secretfile,read),inference(resolution,[status(thm)],[c248, c54])).
% 0.61/0.82 cnf(c299,plain,~state_file_is_not_working_paper(not_secretfile)|~admin_indi_has_citizenship_for_file(admin,X355,not_secretfile)|~admin_indi_has_need_to_know_for_file(admin,X355,not_secretfile)|admin_indi_may_file(admin,X355,not_secretfile,read),inference(resolution,[status(thm)],[c249, c290])).
% 0.61/0.82 cnf(c300,plain,~state_file_is_not_working_paper(not_secretfile)|~admin_indi_has_citizenship_for_file(admin,babu,not_secretfile)|admin_indi_may_file(admin,babu,not_secretfile,read),inference(resolution,[status(thm)],[c299, c205])).
% 0.61/0.82 cnf(c301,plain,~state_file_is_not_working_paper(not_secretfile)|admin_indi_may_file(admin,babu,not_secretfile,read),inference(resolution,[status(thm)],[c300, c286])).
% 0.61/0.82 cnf(c302,plain,admin_indi_may_file(admin,babu,not_secretfile,read),inference(resolution,[status(thm)],[c301, c28])).
% 0.61/0.82 cnf(c303,plain,$false,inference(resolution,[status(thm)],[c302, c2])).
% 0.61/0.82 % SZS output end CNFRefutation
% 0.61/0.82
% 0.61/0.82 % Initial clauses : 88
% 0.61/0.82 % Processed clauses : 185
% 0.61/0.82 % Factors computed : 0
% 0.61/0.82 % Resolvents computed: 114
% 0.61/0.82 % Tautologies deleted: 0
% 0.61/0.82 % Forward subsumed : 5
% 0.61/0.82 % Backward subsumed : 22
% 0.61/0.82 % -------- CPU Time ---------
% 0.61/0.82 % User time : 0.442 s
% 0.61/0.82 % System time : 0.019 s
% 0.61/0.82 % Total time : 0.461 s
%------------------------------------------------------------------------------