%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWV438+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Fri Jul 25 04:47:00 PM UTC 2025
% Result : Theorem 0.12s 0.35s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV438+1 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n020.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 : 300
% 0.12/0.34 % DateTime : Tue Jul 22 09:37:34 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.35 % launching worker at depth: 11
% 0.12/0.35 % SZS status Theorem for theBenchmark
% 0.12/0.35 % SZS output start CNFRefutation
% 0.12/0.35 fof(babureadnotsecret, plain, admin_indi_may_file(admin,babu,not_secretfile,read), file('/export/starexec/sandbox/benchmark/theBenchmark.p', babureadnotsecret)).
% 0.12/0.35 fof(babureadnotsecret_negated, plain, ~(admin_indi_may_file(admin,babu,not_secretfile,read)), inference(negate_conjecture, [status(cth)], [babureadnotsecret])).
% 0.12/0.35 cnf(87, plain, ~admin_indi_may_file(admin,babu,not_secretfile,read), inference(cnf, [status(esa)], [babureadnotsecret_negated])).
% 0.12/0.35 cnf(l0, plain, ~admin_indi_may_file(admin,babu,not_secretfile,read), inference(instantiation, [status(thm)], [87])).
% 0.12/0.35 fof(ax39, 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)))))), file('Axioms/SWV009+0.ax', ax39)).
% 0.12/0.35 cnf(39, plain, ~admin_indi_has_citizenship_for_file(admin,X0,X1) | ~admin_indi_has_need_to_know_for_file(admin,X0,X1) | ~admin_indi_has_compartments_for_file(admin,X0,X1) | ~admin_indi_has_level_for_file(admin,X0,X1) | ~state_file_is_not_working_paper(X1) | admin_indi_may_file(admin,X0,X1,read), inference(cnf, [status(esa)], [ax39])).
% 0.12/0.35 cnf(l1, plain, ~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_compartments_for_file(admin,babu,not_secretfile) | ~admin_indi_has_level_for_file(admin,babu,not_secretfile) | ~state_file_is_not_working_paper(not_secretfile) | admin_indi_may_file(admin,babu,not_secretfile,read), inference(instantiation, [status(thm)], [39])).
% 0.12/0.35 % launching worker at depth: fof(ax37, 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))), file('Axioms/SWV009+0.ax', ax37)).
% 0.12/0.35 12
% 0.12/0.35 cnf(37, plain, ~admin_file_has_citizenship(admin,X0,X1) | ~admin_indi_has_citizenship(admin,X2,X1) | admin_indi_has_citizenship_for_file(admin,X2,X0), inference(cnf, [status(esa)], [ax37])).
% 0.12/0.35 cnf(l2, plain, ~admin_file_has_citizenship(admin,not_secretfile,anycountry) | ~admin_indi_has_citizenship(admin,babu,anycountry) | admin_indi_has_citizenship_for_file(admin,babu,not_secretfile), inference(instantiation, [status(thm)], [37])).
% 0.12/0.35 fof(ax35, 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))), file('Axioms/SWV009+0.ax', ax35)).
% 0.12/0.35 cnf(35, plain, ~admin_file_has_level(admin,X0,X1) | ~admin_indi_has_level(admin,X2,X1) | admin_indi_has_level_for_file(admin,X2,X0), inference(cnf, [status(esa)], [ax35])).
% 0.12/0.35 cnf(l4, plain, ~admin_file_has_level(admin,not_secretfile,unclassified) | ~admin_indi_has_level(admin,babu,unclassified) | admin_indi_has_level_for_file(admin,babu,not_secretfile), inference(instantiation, [status(thm)], [35])).
% 0.12/0.35 fof(ax34, 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))), file('Axioms/SWV009+0.ax', ax34)).
% 0.12/0.35 cnf(34, plain, ~admin_file_has_compartments(admin,X0,X1) | ~admin_indi_has_compartments(admin,X2,X1) | admin_indi_has_compartments_for_file(admin,X2,X0), inference(cnf, [status(esa)], [ax34])).
% 0.12/0.35 cnf(l5, plain, ~admin_file_has_compartments(admin,not_secretfile,nil) | ~admin_indi_has_compartments(admin,babu,nil) | admin_indi_has_compartments_for_file(admin,babu,not_secretfile), inference(instantiation, [status(thm)], [34])).
% 0.12/0.35 fof(ax8, 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))), file('Axioms/SWV009+0.ax', ax8)).
% 0.12/0.35 cnf(8, plain, ~admin_file_has_compartments_h(admin,X0,X1,X1) | ~system_file_needs_compartments(system,X0,X1) | admin_file_has_compartments(admin,X0,X1), inference(cnf, [status(esa)], [ax8])).
% 0.12/0.35 cnf(l14, plain, ~admin_file_has_compartments_h(admin,not_secretfile,nil,nil) | ~system_file_needs_compartments(system,not_secretfile,nil) | admin_file_has_compartments(admin,not_secretfile,nil), inference(instantiation, [status(thm)], [8])).
% 0.12/0.35 fof(ax11, 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)))), file('Axioms/SWV009+0.ax', ax11)).
% 0.12/0.35 cnf(11, plain, ~system_file_needs_level(system,X0,X1) | ~admin_file_has_compartments(admin,X0,X2) | ~admin_file_has_level_h(admin,X0,X1,X2) | admin_file_has_level(admin,X0,X1), inference(cnf, [status(esa)], [ax11])).
% 0.12/0.35 cnf(l23, plain, ~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) | admin_file_has_level(admin,not_secretfile,unclassified), inference(instantiation, [status(thm)], [11])).
% 0.12/0.35 fof(ax14, 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)))), file('Axioms/SWV009+0.ax', ax14)).
% 0.12/0.35 cnf(14, plain, ~admin_file_has_compartments(admin,X0,X1) | ~system_file_needs_citizenship(system,X0,X2) | ~admin_file_has_citizenship_h(admin,X0,X2,X1) | admin_file_has_citizenship(admin,X0,X2), inference(cnf, [status(esa)], [ax14])).
% 0.12/0.35 cnf(l10, plain, ~admin_file_has_compartments(admin,not_secretfile,nil) | ~system_file_needs_citizenship(system,not_secretfile,anycountry) | ~admin_file_has_citizenship_h(admin,not_secretfile,anycountry,nil) | admin_file_has_citizenship(admin,not_secretfile,anycountry), inference(instantiation, [status(thm)], [14])).
% 0.12/0.35 fof(ax24, plain, ![K]:admin_indi_has_level(admin,K,unclassified), file('Axioms/SWV009+0.ax', ax24)).
% 0.12/0.35 cnf(24, plain, admin_indi_has_level(admin,X0,unclassified), inference(cnf, [status(esa)], [ax24])).
% 0.12/0.35 cnf(l6, plain, admin_indi_has_level(admin,babu,unclassified), inference(instantiation, [status(thm)], [24])).
% 0.12/0.35 fof(ax9, plain, ![F,CL]:admin_file_has_compartments_h(admin,F,CL,nil), file('Axioms/SWV009+0.ax', ax9)).
% 0.12/0.35 cnf(9, plain, admin_file_has_compartments_h(admin,X0,X1,nil), inference(cnf, [status(esa)], [ax9])).
% 0.12/0.35 cnf(l28, plain, admin_file_has_compartments_h(admin,not_secretfile,nil,nil), inference(instantiation, [status(thm)], [9])).
% 0.12/0.35 fof(ax63, plain, system_file_needs_level(system,not_secretfile,unclassified), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax63)).
% 0.12/0.35 cnf(63, plain, system_file_needs_level(system,not_secretfile,unclassified), inference(cnf, [status(esa)], [ax63])).
% 0.12/0.35 cnf(l29, plain, system_file_needs_level(system,not_secretfile,unclassified), inference(instantiation, [status(thm)], [63])).
% 0.12/0.35 fof(ax62, plain, system_file_needs_compartments(system,not_secretfile,nil), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax62)).
% 0.12/0.35 cnf(62, plain, system_file_needs_compartments(system,not_secretfile,nil), inference(cnf, [status(esa)], [ax62])).
% 0.12/0.35 cnf(l21, plain, system_file_needs_compartments(system,not_secretfile,nil), inference(instantiation, [status(thm)], [62])).
% 0.12/0.35 cnf(l24, plain, ~admin_file_has_compartments_h(admin,not_secretfile,nil,nil) | ~system_file_needs_compartments(system,not_secretfile,nil) | admin_file_has_compartments(admin,not_secretfile,nil), inference(instantiation, [status(thm)], [8])).
% 0.12/0.35 fof(ax12, plain, ![F,L]:admin_file_has_level_h(admin,F,L,nil), file('Axioms/SWV009+0.ax', ax12)).
% 0.12/0.35 cnf(12, plain, admin_file_has_level_h(admin,X0,X1,nil), inference(cnf, [status(esa)], [ax12])).
% 0.12/0.35 cnf(l30, plain, admin_file_has_level_h(admin,not_secretfile,unclassified,nil), inference(instantiation, [status(thm)], [12])).
% 0.12/0.35 fof(ax61, plain, state_file_is_not_working_paper(not_secretfile), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax61)).
% 0.12/0.35 cnf(61, plain, state_file_is_not_working_paper(not_secretfile), inference(cnf, [status(esa)], [ax61])).
% 0.12/0.35 cnf(l9, plain, state_file_is_not_working_paper(not_secretfile), inference(instantiation, [status(thm)], [61])).
% 0.12/0.35 cnf(l11, plain, ~admin_file_has_compartments_h(admin,not_secretfile,nil,nil) | ~system_file_needs_compartments(system,not_secretfile,nil) | admin_file_has_compartments(admin,not_secretfile,nil), inference(instantiation, [status(thm)], [8])).
% 0.12/0.35 fof(ax36, 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))), file('Axioms/SWV009+0.ax', ax36)).
% 0.12/0.35 cnf(36, plain, ~state_file_has_owner(X0,X1) | ~owner_indi_has_need_to_know(X1,X2,X0) | admin_indi_has_need_to_know_for_file(admin,X2,X0), inference(cnf, [status(esa)], [ax36])).
% 0.12/0.35 cnf(l3, plain, ~state_file_has_owner(not_secretfile,owner_not_secretfile) | ~owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile) | admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile), inference(instantiation, [status(thm)], [36])).
% 0.12/0.35 cnf(l37, plain, system_file_needs_compartments(system,not_secretfile,nil), inference(instantiation, [status(thm)], [62])).
% 0.12/0.35 fof(ax85, plain, owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax85)).
% 0.12/0.35 cnf(85, plain, owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile), inference(cnf, [status(esa)], [ax85])).
% 0.12/0.35 cnf(l38, plain, owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile), inference(instantiation, [status(thm)], [85])).
% 0.12/0.35 fof(ax26, plain, ![K]:admin_indi_has_compartments(admin,K,nil), file('Axioms/SWV009+0.ax', ax26)).
% 0.12/0.35 cnf(26, plain, admin_indi_has_compartments(admin,X0,nil), inference(cnf, [status(esa)], [ax26])).
% 0.12/0.35 cnf(l32, plain, admin_indi_has_compartments(admin,babu,nil), inference(instantiation, [status(thm)], [26])).
% 0.12/0.35 fof(ax22, plain, ![K]:admin_indi_has_citizenship(admin,K,anycountry), file('Axioms/SWV009+0.ax', ax22)).
% 0.12/0.35 cnf(22, plain, admin_indi_has_citizenship(admin,X0,anycountry), inference(cnf, [status(esa)], [ax22])).
% 0.12/0.35 cnf(l13, plain, admin_indi_has_citizenship(admin,babu,anycountry), inference(instantiation, [status(thm)], [22])).
% 0.12/0.35 cnf(l39, plain, admin_file_has_compartments_h(admin,not_secretfile,nil,nil), inference(instantiation, [status(thm)], [9])).
% 0.12/0.35 cnf(l19, plain, admin_file_has_compartments_h(admin,not_secretfile,nil,nil), inference(instantiation, [status(thm)], [9])).
% 0.12/0.35 cnf(l40, plain, system_file_needs_compartments(system,not_secretfile,nil), inference(instantiation, [status(thm)], [62])).
% 0.12/0.35 fof(ax64, plain, system_file_needs_citizenship(system,not_secretfile,anycountry), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax64)).
% 0.12/0.35 cnf(64, plain, system_file_needs_citizenship(system,not_secretfile,anycountry), inference(cnf, [status(esa)], [ax64])).
% 0.12/0.35 cnf(l20, plain, system_file_needs_citizenship(system,not_secretfile,anycountry), inference(instantiation, [status(thm)], [64])).
% 0.12/0.35 fof(ax65, plain, state_file_has_owner(not_secretfile,owner_not_secretfile), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax65)).
% 0.12/0.35 cnf(65, plain, state_file_has_owner(not_secretfile,owner_not_secretfile), inference(cnf, [status(esa)], [ax65])).
% 0.12/0.35 cnf(l41, plain, state_file_has_owner(not_secretfile,owner_not_secretfile), inference(instantiation, [status(thm)], [65])).
% 0.12/0.35 fof(ax15, plain, ![F,U]:admin_file_has_citizenship_h(admin,F,U,nil), file('Axioms/SWV009+0.ax', ax15)).
% 0.12/0.35 cnf(15, plain, admin_file_has_citizenship_h(admin,X0,X1,nil), inference(cnf, [status(esa)], [ax15])).
% 0.12/0.35 cnf(l34, plain, admin_file_has_citizenship_h(admin,not_secretfile,anycountry,nil), inference(instantiation, [status(thm)], [15])).
% 0.12/0.35 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l2, l4, l5, l14, l23, l10, l6, l28, l29, l21, l24, l30, l9, l11, l3, l37, l38, l32, l13, l39, l19, l40, l20, l41, l34])).
% 0.12/0.35 % SZS output end CNFRefutation
%------------------------------------------------------------------------------