%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV438+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n021.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 : Tue May 5 05:23:17 PM UTC 2026
% Result : Theorem 0.28s 1.62s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 21
% Syntax : Number of formulae : 71 ( 40 unt; 0 def)
% Number of atoms : 144 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 127 ( 54 ~; 52 |; 0 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 105 ( 14 sgn 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax11,axiom,
! [X9,X2,X10] :
( system_file_needs_level(system,X9,X2)
=> ( admin_file_has_compartments(admin,X9,X10)
=> ( admin_file_has_level_h(admin,X9,X2,X10)
=> admin_file_has_level(admin,X9,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax11) ).
fof(ax8,axiom,
! [X9,X10] :
( system_file_needs_compartments(system,X9,X10)
=> ( admin_file_has_compartments_h(admin,X9,X10,X10)
=> admin_file_has_compartments(admin,X9,X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax8) ).
fof(ax9,axiom,
! [X9,X10] : admin_file_has_compartments_h(admin,X9,X10,nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax9) ).
fof(ax14,axiom,
! [X9,X13,X10] :
( system_file_needs_citizenship(system,X9,X13)
=> ( admin_file_has_compartments(admin,X9,X10)
=> ( admin_file_has_citizenship_h(admin,X9,X13,X10)
=> admin_file_has_citizenship(admin,X9,X13) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax14) ).
fof(ax35,axiom,
! [X1,X9,X2] :
( admin_file_has_level(admin,X9,X2)
=> ( admin_indi_has_level(admin,X1,X2)
=> admin_indi_has_level_for_file(admin,X1,X9) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax35) ).
fof(ax24,axiom,
! [X1] : admin_indi_has_level(admin,X1,unclassified),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax24) ).
fof(ax63,hypothesis,
system_file_needs_level(system,not_secretfile,unclassified),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax63) ).
fof(ax62,hypothesis,
system_file_needs_compartments(system,not_secretfile,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax62) ).
fof(ax12,axiom,
! [X9,X2] : admin_file_has_level_h(admin,X9,X2,nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax12) ).
fof(ax37,axiom,
! [X1,X9,X2] :
( admin_file_has_citizenship(admin,X9,X2)
=> ( admin_indi_has_citizenship(admin,X1,X2)
=> admin_indi_has_citizenship_for_file(admin,X1,X9) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax37) ).
fof(ax22,axiom,
! [X1] : admin_indi_has_citizenship(admin,X1,anycountry),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax22) ).
fof(ax64,hypothesis,
system_file_needs_citizenship(system,not_secretfile,anycountry),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax64) ).
fof(ax15,axiom,
! [X9,X13] : admin_file_has_citizenship_h(admin,X9,X13,nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax15) ).
fof(ax39,axiom,
! [X1,X9] :
( state_file_is_not_working_paper(X9)
=> ( admin_indi_has_citizenship_for_file(admin,X1,X9)
=> ( admin_indi_has_need_to_know_for_file(admin,X1,X9)
=> ( admin_indi_has_level_for_file(admin,X1,X9)
=> ( admin_indi_has_compartments_for_file(admin,X1,X9)
=> admin_indi_may_file(admin,X1,X9,read) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax39) ).
fof(ax34,axiom,
! [X1,X9,X10] :
( admin_file_has_compartments(admin,X9,X10)
=> ( admin_indi_has_compartments(admin,X1,X10)
=> admin_indi_has_compartments_for_file(admin,X1,X9) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax34) ).
fof(ax26,axiom,
! [X1] : admin_indi_has_compartments(admin,X1,nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax26) ).
fof(ax61,hypothesis,
state_file_is_not_working_paper(not_secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax61) ).
fof(ax36,axiom,
! [X1,X9,X22] :
( state_file_has_owner(X9,X22)
=> ( owner_indi_has_need_to_know(X22,X1,X9)
=> admin_indi_has_need_to_know_for_file(admin,X1,X9) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV009+0.ax',ax36) ).
fof(ax85,hypothesis,
owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax85) ).
fof(ax65,hypothesis,
state_file_has_owner(not_secretfile,owner_not_secretfile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax65) ).
fof(babureadnotsecret,conjecture,
admin_indi_may_file(admin,babu,not_secretfile,read),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',babureadnotsecret) ).
fof(c_0_21,plain,
! [X178,X179,X180] :
( ~ system_file_needs_level(system,X178,X179)
| ~ admin_file_has_compartments(admin,X178,X180)
| ~ admin_file_has_level_h(admin,X178,X179,X180)
| admin_file_has_level(admin,X178,X179) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax11])]) ).
fof(c_0_22,plain,
! [X169,X170] :
( ~ system_file_needs_compartments(system,X169,X170)
| ~ admin_file_has_compartments_h(admin,X169,X170,X170)
| admin_file_has_compartments(admin,X169,X170) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax8])]) ).
fof(c_0_23,plain,
! [X171,X172] : admin_file_has_compartments_h(admin,X171,X172,nil),
inference(variable_rename,[status(thm)],[ax9]) ).
fof(c_0_24,plain,
! [X189,X190,X191] :
( ~ system_file_needs_citizenship(system,X189,X190)
| ~ admin_file_has_compartments(admin,X189,X191)
| ~ admin_file_has_citizenship_h(admin,X189,X190,X191)
| admin_file_has_citizenship(admin,X189,X190) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax14])]) ).
fof(c_0_25,plain,
! [X266,X267,X268] :
( ~ admin_file_has_level(admin,X267,X268)
| ~ admin_indi_has_level(admin,X266,X268)
| admin_indi_has_level_for_file(admin,X266,X267) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax35])]) ).
fof(c_0_26,plain,
! [X214] : admin_indi_has_level(admin,X214,unclassified),
inference(variable_rename,[status(thm)],[ax24]) ).
cnf(c_0_27,plain,
( admin_file_has_level(admin,X1,X2)
| ~ system_file_needs_level(system,X1,X2)
| ~ admin_file_has_compartments(admin,X1,X3)
| ~ admin_file_has_level_h(admin,X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_28,hypothesis,
system_file_needs_level(system,not_secretfile,unclassified),
inference(split_conjunct,[status(thm)],[ax63]) ).
cnf(c_0_29,plain,
( admin_file_has_compartments(admin,X1,X2)
| ~ system_file_needs_compartments(system,X1,X2)
| ~ admin_file_has_compartments_h(admin,X1,X2,X2) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_30,hypothesis,
system_file_needs_compartments(system,not_secretfile,nil),
inference(split_conjunct,[status(thm)],[ax62]) ).
cnf(c_0_31,plain,
admin_file_has_compartments_h(admin,X1,X2,nil),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
fof(c_0_32,plain,
! [X181,X182] : admin_file_has_level_h(admin,X181,X182,nil),
inference(variable_rename,[status(thm)],[ax12]) ).
fof(c_0_33,plain,
! [X272,X273,X274] :
( ~ admin_file_has_citizenship(admin,X273,X274)
| ~ admin_indi_has_citizenship(admin,X272,X274)
| admin_indi_has_citizenship_for_file(admin,X272,X273) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax37])]) ).
fof(c_0_34,plain,
! [X211] : admin_indi_has_citizenship(admin,X211,anycountry),
inference(variable_rename,[status(thm)],[ax22]) ).
cnf(c_0_35,plain,
( admin_file_has_citizenship(admin,X1,X2)
| ~ system_file_needs_citizenship(system,X1,X2)
| ~ admin_file_has_compartments(admin,X1,X3)
| ~ admin_file_has_citizenship_h(admin,X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_36,hypothesis,
system_file_needs_citizenship(system,not_secretfile,anycountry),
inference(split_conjunct,[status(thm)],[ax64]) ).
fof(c_0_37,plain,
! [X192,X193] : admin_file_has_citizenship_h(admin,X192,X193,nil),
inference(variable_rename,[status(thm)],[ax15]) ).
cnf(c_0_38,plain,
( admin_indi_has_level_for_file(admin,X3,X1)
| ~ admin_file_has_level(admin,X1,X2)
| ~ admin_indi_has_level(admin,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_39,plain,
admin_indi_has_level(admin,X1,unclassified),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_40,hypothesis,
( admin_file_has_level(admin,not_secretfile,unclassified)
| ~ admin_file_has_level_h(admin,not_secretfile,unclassified,X1)
| ~ admin_file_has_compartments(admin,not_secretfile,X1) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_41,hypothesis,
admin_file_has_compartments(admin,not_secretfile,nil),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31])]) ).
cnf(c_0_42,plain,
admin_file_has_level_h(admin,X1,X2,nil),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_43,plain,
( admin_indi_has_citizenship_for_file(admin,X3,X1)
| ~ admin_file_has_citizenship(admin,X1,X2)
| ~ admin_indi_has_citizenship(admin,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
cnf(c_0_44,plain,
admin_indi_has_citizenship(admin,X1,anycountry),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_45,hypothesis,
( admin_file_has_citizenship(admin,not_secretfile,anycountry)
| ~ admin_file_has_citizenship_h(admin,not_secretfile,anycountry,X1)
| ~ admin_file_has_compartments(admin,not_secretfile,X1) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_46,plain,
admin_file_has_citizenship_h(admin,X1,X2,nil),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
fof(c_0_47,plain,
! [X277,X278] :
( ~ state_file_is_not_working_paper(X278)
| ~ admin_indi_has_citizenship_for_file(admin,X277,X278)
| ~ admin_indi_has_need_to_know_for_file(admin,X277,X278)
| ~ admin_indi_has_level_for_file(admin,X277,X278)
| ~ admin_indi_has_compartments_for_file(admin,X277,X278)
| admin_indi_may_file(admin,X277,X278,read) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax39])]) ).
cnf(c_0_48,plain,
( admin_indi_has_level_for_file(admin,X1,X2)
| ~ admin_file_has_level(admin,X2,unclassified) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_49,hypothesis,
admin_file_has_level(admin,not_secretfile,unclassified),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_42])]) ).
cnf(c_0_50,plain,
( admin_indi_has_citizenship_for_file(admin,X1,X2)
| ~ admin_file_has_citizenship(admin,X2,anycountry) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_51,hypothesis,
admin_file_has_citizenship(admin,not_secretfile,anycountry),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_41]),c_0_46])]) ).
fof(c_0_52,plain,
! [X263,X264,X265] :
( ~ admin_file_has_compartments(admin,X264,X265)
| ~ admin_indi_has_compartments(admin,X263,X265)
| admin_indi_has_compartments_for_file(admin,X263,X264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax34])]) ).
fof(c_0_53,plain,
! [X220] : admin_indi_has_compartments(admin,X220,nil),
inference(variable_rename,[status(thm)],[ax26]) ).
cnf(c_0_54,plain,
( admin_indi_may_file(admin,X2,X1,read)
| ~ state_file_is_not_working_paper(X1)
| ~ admin_indi_has_citizenship_for_file(admin,X2,X1)
| ~ admin_indi_has_need_to_know_for_file(admin,X2,X1)
| ~ admin_indi_has_level_for_file(admin,X2,X1)
| ~ admin_indi_has_compartments_for_file(admin,X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_55,hypothesis,
admin_indi_has_level_for_file(admin,X1,not_secretfile),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
cnf(c_0_56,hypothesis,
state_file_is_not_working_paper(not_secretfile),
inference(split_conjunct,[status(thm)],[ax61]) ).
cnf(c_0_57,hypothesis,
admin_indi_has_citizenship_for_file(admin,X1,not_secretfile),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_58,plain,
( admin_indi_has_compartments_for_file(admin,X3,X1)
| ~ admin_file_has_compartments(admin,X1,X2)
| ~ admin_indi_has_compartments(admin,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_59,plain,
admin_indi_has_compartments(admin,X1,nil),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
fof(c_0_60,plain,
! [X269,X270,X271] :
( ~ state_file_has_owner(X270,X271)
| ~ owner_indi_has_need_to_know(X271,X269,X270)
| admin_indi_has_need_to_know_for_file(admin,X269,X270) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax36])]) ).
cnf(c_0_61,hypothesis,
( admin_indi_may_file(admin,X1,not_secretfile,read)
| ~ admin_indi_has_need_to_know_for_file(admin,X1,not_secretfile)
| ~ admin_indi_has_compartments_for_file(admin,X1,not_secretfile) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_56])]),c_0_57])]) ).
cnf(c_0_62,plain,
( admin_indi_has_compartments_for_file(admin,X1,X2)
| ~ admin_file_has_compartments(admin,X2,nil) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_63,plain,
( admin_indi_has_need_to_know_for_file(admin,X3,X1)
| ~ state_file_has_owner(X1,X2)
| ~ owner_indi_has_need_to_know(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_64,hypothesis,
owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),
inference(split_conjunct,[status(thm)],[ax85]) ).
cnf(c_0_65,hypothesis,
state_file_has_owner(not_secretfile,owner_not_secretfile),
inference(split_conjunct,[status(thm)],[ax65]) ).
fof(c_0_66,negated_conjecture,
~ admin_indi_may_file(admin,babu,not_secretfile,read),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[babureadnotsecret])]) ).
cnf(c_0_67,hypothesis,
( admin_indi_may_file(admin,X1,not_secretfile,read)
| ~ admin_indi_has_need_to_know_for_file(admin,X1,not_secretfile) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_62]),c_0_41])]) ).
cnf(c_0_68,hypothesis,
admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_65])]) ).
cnf(c_0_69,negated_conjecture,
~ admin_indi_may_file(admin,babu,not_secretfile,read),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_70,hypothesis,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_68]),c_0_69]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV438+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n021.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 05:16:55 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.28/1.62 % Version : CSE_E---1.7
% 0.28/1.62 % Problem : theBenchmark.p
% 0.28/1.62 % SZS status Theorem for theBenchmark.p
% 0.28/1.62 % SZS output start CNFRefutation
% See solution above
% 0.28/1.62 % Total time : 1.270s
%------------------------------------------------------------------------------