%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV438+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 02:50:51 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV438+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:56:39 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f9,axiom,(
% 0.09/0.39 (! [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) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f10,axiom,(
% 0.09/0.39 (! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f12,axiom,(
% 0.09/0.39 (! [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) ) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f13,axiom,(
% 0.09/0.39 (! [F,L] : admin_file_has_level_h(admin,F,L,nil) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f15,axiom,(
% 0.09/0.39 (! [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) ) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f16,axiom,(
% 0.09/0.39 (! [F,U] : admin_file_has_citizenship_h(admin,F,U,nil) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f23,axiom,(
% 0.09/0.39 (! [K] : admin_indi_has_citizenship(admin,K,anycountry) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f25,axiom,(
% 0.09/0.39 (! [K] : admin_indi_has_level(admin,K,unclassified) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f27,axiom,(
% 0.09/0.39 (! [K] : admin_indi_has_compartments(admin,K,nil) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f35,axiom,(
% 0.09/0.39 (! [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) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f36,axiom,(
% 0.09/0.39 (! [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) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f37,axiom,(
% 0.09/0.39 (! [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) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f38,axiom,(
% 0.09/0.39 (! [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) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f40,axiom,(
% 0.09/0.39 (! [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) ) ) ) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f62,hypothesis,(
% 0.09/0.39 state_file_is_not_working_paper(not_secretfile) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f63,hypothesis,(
% 0.09/0.39 system_file_needs_compartments(system,not_secretfile,nil) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f64,hypothesis,(
% 0.09/0.39 system_file_needs_level(system,not_secretfile,unclassified) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f65,hypothesis,(
% 0.09/0.39 system_file_needs_citizenship(system,not_secretfile,anycountry) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f66,hypothesis,(
% 0.09/0.39 state_file_has_owner(not_secretfile,owner_not_secretfile) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f86,hypothesis,(
% 0.09/0.39 owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f88,conjecture,(
% 0.09/0.39 admin_indi_may_file(admin,babu,not_secretfile,read) ),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f89,negated_conjecture,(
% 0.09/0.39 ~(admin_indi_may_file(admin,babu,not_secretfile,read) )),
% 0.09/0.39 inference(negated_conjecture,[status(cth)],[f88])).
% 0.09/0.39 fof(f103,plain,(
% 0.09/0.39 ![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)))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.09/0.39 fof(f104,plain,(
% 0.09/0.39 ![X0,X1]: (~system_file_needs_compartments(system,X0,X1)|~admin_file_has_compartments_h(admin,X0,X1,X1)|admin_file_has_compartments(admin,X0,X1))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f103])).
% 0.09/0.39 fof(f105,plain,(
% 0.09/0.39 ![X0,X1]: (admin_file_has_compartments_h(admin,X0,X1,nil))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f10])).
% 0.09/0.39 fof(f109,plain,(
% 0.09/0.39 ![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))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.09/0.39 fof(f110,plain,(
% 0.09/0.39 ![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)))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f109])).
% 0.09/0.39 fof(f111,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~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))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f110])).
% 0.09/0.39 fof(f112,plain,(
% 0.09/0.39 ![X0,X1]: (admin_file_has_level_h(admin,X0,X1,nil))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f13])).
% 0.09/0.39 fof(f116,plain,(
% 0.09/0.39 ![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))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.09/0.39 fof(f117,plain,(
% 0.09/0.39 ![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)))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f116])).
% 0.09/0.39 fof(f118,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~system_file_needs_citizenship(system,X0,X1)|~admin_file_has_compartments(admin,X0,X2)|~admin_file_has_citizenship_h(admin,X0,X1,X2)|admin_file_has_citizenship(admin,X0,X1))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f117])).
% 0.09/0.39 fof(f119,plain,(
% 0.09/0.39 ![X0,X1]: (admin_file_has_citizenship_h(admin,X0,X1,nil))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f16])).
% 0.09/0.39 fof(f136,plain,(
% 0.09/0.39 ![X0]: (admin_indi_has_citizenship(admin,X0,anycountry))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f23])).
% 0.09/0.39 fof(f139,plain,(
% 0.09/0.39 ![X0]: (admin_indi_has_level(admin,X0,unclassified))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f25])).
% 0.09/0.39 fof(f143,plain,(
% 0.09/0.39 ![X0]: (admin_indi_has_compartments(admin,X0,nil))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f27])).
% 0.09/0.39 fof(f165,plain,(
% 0.09/0.39 ![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)))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.09/0.39 fof(f166,plain,(
% 0.09/0.39 ![F,CL]: (~admin_file_has_compartments(admin,F,CL)|(![K]: (~admin_indi_has_compartments(admin,K,CL)|admin_indi_has_compartments_for_file(admin,K,F))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f165])).
% 0.09/0.39 fof(f167,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~admin_file_has_compartments(admin,X0,X1)|~admin_indi_has_compartments(admin,X2,X1)|admin_indi_has_compartments_for_file(admin,X2,X0))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f166])).
% 0.09/0.39 fof(f168,plain,(
% 0.09/0.39 ![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)))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.09/0.39 fof(f169,plain,(
% 0.09/0.39 ![F,L]: (~admin_file_has_level(admin,F,L)|(![K]: (~admin_indi_has_level(admin,K,L)|admin_indi_has_level_for_file(admin,K,F))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f168])).
% 0.09/0.39 fof(f170,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~admin_file_has_level(admin,X0,X1)|~admin_indi_has_level(admin,X2,X1)|admin_indi_has_level_for_file(admin,X2,X0))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f169])).
% 0.09/0.39 fof(f171,plain,(
% 0.09/0.39 ![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)))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.09/0.39 fof(f172,plain,(
% 0.09/0.39 ![F,OWR]: (~state_file_has_owner(F,OWR)|(![K]: (~owner_indi_has_need_to_know(OWR,K,F)|admin_indi_has_need_to_know_for_file(admin,K,F))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f171])).
% 0.09/0.39 fof(f173,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~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))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f172])).
% 0.09/0.39 fof(f174,plain,(
% 0.09/0.39 ![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)))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.09/0.39 fof(f175,plain,(
% 0.09/0.39 ![F,L]: (~admin_file_has_citizenship(admin,F,L)|(![K]: (~admin_indi_has_citizenship(admin,K,L)|admin_indi_has_citizenship_for_file(admin,K,F))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f174])).
% 0.09/0.39 fof(f176,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~admin_file_has_citizenship(admin,X0,X1)|~admin_indi_has_citizenship(admin,X2,X1)|admin_indi_has_citizenship_for_file(admin,X2,X0))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f175])).
% 0.09/0.39 fof(f180,plain,(
% 0.09/0.39 ![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))))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.09/0.39 fof(f181,plain,(
% 0.09/0.39 ![F]: (~state_file_is_not_working_paper(F)|(![K]: (~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)))))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f180])).
% 0.09/0.39 fof(f182,plain,(
% 0.09/0.39 ![X0,X1]: (~state_file_is_not_working_paper(X0)|~admin_indi_has_citizenship_for_file(admin,X1,X0)|~admin_indi_has_need_to_know_for_file(admin,X1,X0)|~admin_indi_has_level_for_file(admin,X1,X0)|~admin_indi_has_compartments_for_file(admin,X1,X0)|admin_indi_may_file(admin,X1,X0,read))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f181])).
% 0.09/0.39 fof(f206,plain,(
% 0.09/0.39 state_file_is_not_working_paper(not_secretfile)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f62])).
% 0.09/0.39 fof(f207,plain,(
% 0.09/0.39 system_file_needs_compartments(system,not_secretfile,nil)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.39 fof(f208,plain,(
% 0.09/0.39 system_file_needs_level(system,not_secretfile,unclassified)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f64])).
% 0.09/0.39 fof(f209,plain,(
% 0.09/0.39 system_file_needs_citizenship(system,not_secretfile,anycountry)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f65])).
% 0.09/0.39 fof(f210,plain,(
% 0.09/0.39 state_file_has_owner(not_secretfile,owner_not_secretfile)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f66])).
% 0.09/0.39 fof(f230,plain,(
% 0.09/0.39 owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f86])).
% 0.09/0.39 fof(f232,plain,(
% 0.09/0.39 ~admin_indi_may_file(admin,babu,not_secretfile,read)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f89])).
% 0.09/0.39 fof(f306,plain,(
% 0.09/0.39 ~admin_file_has_compartments_h(admin,not_secretfile,nil,nil)|admin_file_has_compartments(admin,not_secretfile,nil)),
% 0.09/0.39 inference(resolution,[status(thm)],[f207,f104])).
% 0.09/0.39 fof(f307,definition,(
% 0.09/0.39 sQ15_spl <=> (admin_file_has_compartments_h(admin,not_secretfile,nil,nil))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f309,plain,(
% 0.09/0.39 ~admin_file_has_compartments_h(admin,not_secretfile,nil,nil)|sQ15_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f307])).
% 0.09/0.39 fof(f310,definition,(
% 0.09/0.39 sQ16_spl <=> (admin_file_has_compartments(admin,not_secretfile,nil))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f311,plain,(
% 0.09/0.39 admin_file_has_compartments(admin,not_secretfile,nil)|~sQ16_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f310])).
% 0.09/0.39 fof(f313,plain,(
% 0.09/0.39 ~sQ15_spl|sQ16_spl),
% 0.09/0.39 inference(split_clause,[status(thm)],[f306,f307,f310])).
% 0.09/0.39 fof(f314,plain,(
% 0.09/0.39 $false|sQ15_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f309,f105])).
% 0.09/0.39 fof(f315,plain,(
% 0.09/0.39 sQ15_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f314])).
% 0.09/0.39 fof(f316,plain,(
% 0.09/0.39 ![X0]: (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_file_has_level_h(admin,not_secretfile,unclassified,X0)|admin_file_has_level(admin,not_secretfile,unclassified))),
% 0.09/0.39 inference(resolution,[status(thm)],[f208,f111])).
% 0.09/0.39 fof(f317,definition,(
% 0.09/0.39 ![X0]: (sQ17_spl <=> (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_file_has_level_h(admin,not_secretfile,unclassified,X0)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f318,plain,(
% 0.09/0.39 ![X0]: (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_file_has_level_h(admin,not_secretfile,unclassified,X0)|~sQ17_spl)),
% 0.09/0.39 inference(component_clause,[status(thm)],[f317])).
% 0.09/0.39 fof(f320,definition,(
% 0.09/0.39 sQ18_spl <=> (admin_file_has_level(admin,not_secretfile,unclassified))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f321,plain,(
% 0.09/0.39 admin_file_has_level(admin,not_secretfile,unclassified)|~sQ18_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f320])).
% 0.09/0.39 fof(f323,plain,(
% 0.09/0.39 sQ17_spl|sQ18_spl),
% 0.09/0.39 inference(split_clause,[status(thm)],[f316,f317,f320])).
% 0.09/0.39 fof(f324,plain,(
% 0.09/0.39 ![X0]: (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_file_has_citizenship_h(admin,not_secretfile,anycountry,X0)|admin_file_has_citizenship(admin,not_secretfile,anycountry))),
% 0.09/0.39 inference(resolution,[status(thm)],[f209,f118])).
% 0.09/0.39 fof(f325,definition,(
% 0.09/0.39 ![X0]: (sQ19_spl <=> (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_file_has_citizenship_h(admin,not_secretfile,anycountry,X0)))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f326,plain,(
% 0.09/0.39 ![X0]: (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_file_has_citizenship_h(admin,not_secretfile,anycountry,X0)|~sQ19_spl)),
% 0.09/0.39 inference(component_clause,[status(thm)],[f325])).
% 0.09/0.39 fof(f328,definition,(
% 0.09/0.39 sQ20_spl <=> (admin_file_has_citizenship(admin,not_secretfile,anycountry))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f329,plain,(
% 0.09/0.39 admin_file_has_citizenship(admin,not_secretfile,anycountry)|~sQ20_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f328])).
% 0.09/0.39 fof(f331,plain,(
% 0.09/0.39 sQ19_spl|sQ20_spl),
% 0.09/0.39 inference(split_clause,[status(thm)],[f324,f325,f328])).
% 0.09/0.39 fof(f340,plain,(
% 0.09/0.39 ~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)),
% 0.09/0.39 inference(resolution,[status(thm)],[f232,f182])).
% 0.09/0.39 fof(f341,definition,(
% 0.09/0.39 sQ21_spl <=> (state_file_is_not_working_paper(not_secretfile))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f343,plain,(
% 0.09/0.39 ~state_file_is_not_working_paper(not_secretfile)|sQ21_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f341])).
% 0.09/0.39 fof(f344,definition,(
% 0.09/0.39 sQ22_spl <=> (admin_indi_has_citizenship_for_file(admin,babu,not_secretfile))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f346,plain,(
% 0.09/0.39 ~admin_indi_has_citizenship_for_file(admin,babu,not_secretfile)|sQ22_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f344])).
% 0.09/0.39 fof(f347,definition,(
% 0.09/0.39 sQ23_spl <=> (admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f349,plain,(
% 0.09/0.39 ~admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile)|sQ23_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f347])).
% 0.09/0.39 fof(f350,definition,(
% 0.09/0.39 sQ24_spl <=> (admin_indi_has_level_for_file(admin,babu,not_secretfile))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f352,plain,(
% 0.09/0.39 ~admin_indi_has_level_for_file(admin,babu,not_secretfile)|sQ24_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f350])).
% 0.09/0.39 fof(f353,definition,(
% 0.09/0.39 sQ25_spl <=> (admin_indi_has_compartments_for_file(admin,babu,not_secretfile))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f355,plain,(
% 0.09/0.39 ~admin_indi_has_compartments_for_file(admin,babu,not_secretfile)|sQ25_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f353])).
% 0.09/0.39 fof(f356,plain,(
% 0.09/0.39 ~sQ21_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl|~sQ25_spl),
% 0.09/0.39 inference(split_clause,[status(thm)],[f340,f341,f344,f347,f350,f353])).
% 0.09/0.39 fof(f361,plain,(
% 0.09/0.39 ~admin_file_has_compartments(admin,not_secretfile,nil)|~sQ17_spl),
% 0.09/0.39 inference(resolution,[status(thm)],[f318,f112])).
% 0.09/0.39 fof(f362,plain,(
% 0.09/0.39 $false|~sQ16_spl|~sQ17_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f361,f311])).
% 0.09/0.39 fof(f363,plain,(
% 0.09/0.39 ~sQ16_spl|~sQ17_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f362])).
% 0.09/0.39 fof(f364,plain,(
% 0.09/0.39 ~admin_file_has_compartments(admin,not_secretfile,nil)|~sQ19_spl),
% 0.09/0.39 inference(resolution,[status(thm)],[f326,f119])).
% 0.09/0.39 fof(f365,plain,(
% 0.09/0.39 $false|~sQ16_spl|~sQ19_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f364,f311])).
% 0.09/0.39 fof(f366,plain,(
% 0.09/0.39 ~sQ16_spl|~sQ19_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f365])).
% 0.09/0.39 fof(f367,plain,(
% 0.09/0.39 ![X0]: (~admin_file_has_compartments(admin,not_secretfile,X0)|~admin_indi_has_compartments(admin,babu,X0)|sQ25_spl)),
% 0.09/0.39 inference(resolution,[status(thm)],[f355,f167])).
% 0.09/0.39 fof(f368,plain,(
% 0.09/0.39 ![X0]: (~admin_indi_has_citizenship(admin,X0,anycountry)|admin_indi_has_citizenship_for_file(admin,X0,not_secretfile)|~sQ20_spl)),
% 0.09/0.39 inference(resolution,[status(thm)],[f329,f176])).
% 0.09/0.39 fof(f369,plain,(
% 0.09/0.39 ![X0]: (admin_indi_has_citizenship_for_file(admin,X0,not_secretfile)|~sQ20_spl)),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f368,f136])).
% 0.09/0.39 fof(f370,plain,(
% 0.09/0.39 ~admin_file_has_compartments(admin,not_secretfile,nil)|sQ25_spl),
% 0.09/0.39 inference(resolution,[status(thm)],[f367,f143])).
% 0.09/0.39 fof(f371,plain,(
% 0.09/0.39 $false|~sQ16_spl|sQ25_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f370,f311])).
% 0.09/0.39 fof(f372,plain,(
% 0.09/0.39 ~sQ16_spl|sQ25_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f371])).
% 0.09/0.39 fof(f373,plain,(
% 0.09/0.39 ![X0]: (~admin_file_has_level(admin,not_secretfile,X0)|~admin_indi_has_level(admin,babu,X0)|sQ24_spl)),
% 0.09/0.39 inference(resolution,[status(thm)],[f352,f170])).
% 0.09/0.39 fof(f374,plain,(
% 0.09/0.39 ~admin_indi_has_level(admin,babu,unclassified)|sQ24_spl|~sQ18_spl),
% 0.09/0.39 inference(resolution,[status(thm)],[f373,f321])).
% 0.09/0.39 fof(f375,plain,(
% 0.09/0.39 $false|sQ24_spl|~sQ18_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f374,f139])).
% 0.09/0.39 fof(f376,plain,(
% 0.09/0.39 sQ24_spl|~sQ18_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f375])).
% 0.09/0.39 fof(f377,plain,(
% 0.09/0.39 ![X0]: (~state_file_has_owner(not_secretfile,X0)|~owner_indi_has_need_to_know(X0,babu,not_secretfile)|sQ23_spl)),
% 0.09/0.39 inference(resolution,[status(thm)],[f349,f173])).
% 0.09/0.39 fof(f378,plain,(
% 0.09/0.39 ~state_file_has_owner(not_secretfile,owner_not_secretfile)|sQ23_spl),
% 0.09/0.39 inference(resolution,[status(thm)],[f377,f230])).
% 0.09/0.39 fof(f379,plain,(
% 0.09/0.39 $false|sQ23_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f378,f210])).
% 0.09/0.39 fof(f380,plain,(
% 0.09/0.39 sQ23_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f379])).
% 0.09/0.39 fof(f381,plain,(
% 0.09/0.39 $false|sQ21_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f343,f206])).
% 0.09/0.39 fof(f382,plain,(
% 0.09/0.39 sQ21_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f381])).
% 0.09/0.39 fof(f383,plain,(
% 0.09/0.39 $false|~sQ20_spl|sQ22_spl),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f346,f369])).
% 0.09/0.39 fof(f384,plain,(
% 0.09/0.39 ~sQ20_spl|sQ22_spl),
% 0.09/0.39 inference(contradiction_clause,[status(thm)],[f383])).
% 0.09/0.39 fof(f385,plain,(
% 0.09/0.39 $false),
% 0.09/0.39 inference(sat_refutation,[status(thm)],[f313,f315,f323,f331,f356,f363,f366,f372,f376,f380,f382,f384])).
% 0.09/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.41 % Elapsed time: 0.048111 seconds
% 0.09/0.41 % CPU time: 0.134575 seconds
% 0.09/0.41 % Total memory used: 45.231 MB
% 0.09/0.41 % Net memory used: 45.200 MB
%------------------------------------------------------------------------------