%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV438+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n029.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 : Mon Jun 24 16:47:21 EDT 2024
% Result : Theorem 0.55s 0.82s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SWV438+1 : TPTP v8.2.0. Released v4.0.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 18:16:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.75 start to proof:theBenchmark
% 0.55/0.81 %-------------------------------------------
% 0.55/0.81 % File :CSE---1.7
% 0.55/0.81 % Problem :theBenchmark
% 0.55/0.81 % Transform :cnf
% 0.55/0.81 % Format :tptp:raw
% 0.55/0.81 % Command :java -jar mcs_scs.jar %d %s
% 0.55/0.81
% 0.55/0.81 % Result :Theorem 0.010000s
% 0.55/0.81 % Output :CNFRefutation 0.010000s
% 0.55/0.81 %-------------------------------------------
% 0.55/0.81 %------------------------------------------------------------------------------
% 0.55/0.81 % File : SWV438+1 : TPTP v8.2.0. Released v4.0.0.
% 0.55/0.81 % Domain : Software Verification (Security)
% 0.55/0.81 % Problem : Can Babu read the non-secret file?
% 0.55/0.81 % Version : [Gar09] axioms.
% 0.55/0.81 % English :
% 0.55/0.81
% 0.55/0.81 % Refs : [Gar09] Garg (2006), Email to Geoff Sutcliffe
% 0.55/0.81 % Source : [Gar09]
% 0.55/0.81 % Names :
% 0.55/0.81
% 0.55/0.81 % Status : Theorem
% 0.55/0.81 % Rating : 0.00 v8.1.0, 0.07 v7.5.0, 0.10 v7.4.0, 0.00 v6.1.0, 0.08 v6.0.0, 0.50 v5.5.0, 0.21 v5.4.0, 0.17 v5.3.0, 0.22 v5.2.0, 0.14 v5.0.0, 0.10 v4.1.0, 0.11 v4.0.1, 0.16 v4.0.0
% 0.55/0.81 % Syntax : Number of formulae : 88 ( 59 unt; 0 def)
% 0.55/0.81 % Number of atoms : 176 ( 0 equ)
% 0.55/0.81 % Maximal formula atoms : 11 ( 2 avg)
% 0.55/0.81 % Number of connectives : 88 ( 0 ~; 0 |; 0 &)
% 0.55/0.81 % ( 0 <=>; 88 =>; 0 <=; 0 <~>)
% 0.55/0.81 % Maximal formula depth : 16 ( 3 avg)
% 0.55/0.81 % Maximal term depth : 3 ( 1 avg)
% 0.55/0.81 % Number of predicates : 55 ( 55 usr; 0 prp; 1-6 aty)
% 0.55/0.81 % Number of functors : 34 ( 34 usr; 33 con; 0-2 aty)
% 0.55/0.81 % Number of variables : 129 ( 129 !; 0 ?)
% 0.55/0.81 % SPC : FOF_THM_RFO_NEQ
% 0.55/0.81
% 0.55/0.81 % Comments : Formalization of policies governing access to classified
% 0.55/0.81 % information in the intelligence community in USA.
% 0.55/0.81 %------------------------------------------------------------------------------
% 0.55/0.81 %----Include axioms
% 0.55/0.81 include('Axioms/SWV009+0.ax').
% 0.55/0.81 %------------------------------------------------------------------------------
% 0.55/0.81 fof(ax41,hypothesis,
% 0.55/0.81 system_indi_is_oca(system,oca) ).
% 0.55/0.81
% 0.55/0.81 fof(ax42,hypothesis,
% 0.55/0.81 oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes) ).
% 0.55/0.81
% 0.55/0.81 fof(ax43,hypothesis,
% 0.55/0.81 oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no) ).
% 0.55/0.81
% 0.55/0.81 fof(ax44,hypothesis,
% 0.55/0.82 system_compartment_has_sso(system,compartmentb,sso_compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax45,hypothesis,
% 0.55/0.82 oca_compartment_has_scg(oca,compartmentb,scg_compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax46,hypothesis,
% 0.55/0.82 sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax47,hypothesis,
% 0.55/0.82 system_compartment_has_sso(system,compartmenta,sso_compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax48,hypothesis,
% 0.55/0.82 oca_compartment_has_scg(oca,compartmenta,scg_compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax49,hypothesis,
% 0.55/0.82 sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax50,hypothesis,
% 0.55/0.82 state_file_is_not_working_paper(secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax51,hypothesis,
% 0.55/0.82 system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))) ).
% 0.55/0.82
% 0.55/0.82 fof(ax52,hypothesis,
% 0.55/0.82 sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))) ).
% 0.55/0.82
% 0.55/0.82 fof(ax53,hypothesis,
% 0.55/0.82 sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))) ).
% 0.55/0.82
% 0.55/0.82 fof(ax54,hypothesis,
% 0.55/0.82 system_file_needs_level(system,secretfile,secret) ).
% 0.55/0.82
% 0.55/0.82 fof(ax55,hypothesis,
% 0.55/0.82 sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax56,hypothesis,
% 0.55/0.82 sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax57,hypothesis,
% 0.55/0.82 system_file_needs_citizenship(system,secretfile,usa) ).
% 0.55/0.82
% 0.55/0.82 fof(ax58,hypothesis,
% 0.55/0.82 sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax59,hypothesis,
% 0.55/0.82 sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax60,hypothesis,
% 0.55/0.82 state_file_has_owner(secretfile,owner_secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax61,hypothesis,
% 0.55/0.82 state_file_is_not_working_paper(not_secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax62,hypothesis,
% 0.55/0.82 system_file_needs_compartments(system,not_secretfile,nil) ).
% 0.55/0.82
% 0.55/0.82 fof(ax63,hypothesis,
% 0.55/0.82 system_file_needs_level(system,not_secretfile,unclassified) ).
% 0.55/0.82
% 0.55/0.82 fof(ax64,hypothesis,
% 0.55/0.82 system_file_needs_citizenship(system,not_secretfile,anycountry) ).
% 0.55/0.82
% 0.55/0.82 fof(ax65,hypothesis,
% 0.55/0.82 state_file_has_owner(not_secretfile,owner_not_secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax66,hypothesis,
% 0.55/0.82 system_indi_is_polygraph_admin(system,polygraph_admin) ).
% 0.55/0.82
% 0.55/0.82 fof(ax67,hypothesis,
% 0.55/0.82 system_indi_is_credit_admin(system,credit_admin) ).
% 0.55/0.82
% 0.55/0.82 fof(ax68,hypothesis,
% 0.55/0.82 system_indi_is_background_admin(system,background_admin) ).
% 0.55/0.82
% 0.55/0.82 fof(ax69,hypothesis,
% 0.55/0.82 system_indi_is_hr_admin(system,hr_admin) ).
% 0.55/0.82
% 0.55/0.82 fof(ax70,hypothesis,
% 0.55/0.82 system_indi_is_level_admin(system,level_admin) ).
% 0.55/0.82
% 0.55/0.82 fof(ax71,hypothesis,
% 0.55/0.82 system_indi_has_citizenship(system,alice,usa) ).
% 0.55/0.82
% 0.55/0.82 fof(ax72,hypothesis,
% 0.55/0.82 polygraph_admin_indi_has_polygraph(polygraph_admin,alice) ).
% 0.55/0.82
% 0.55/0.82 fof(ax73,hypothesis,
% 0.55/0.82 credit_admin_indi_has_credit(credit_admin,alice) ).
% 0.55/0.82
% 0.55/0.82 fof(ax74,hypothesis,
% 0.55/0.82 background_admin_indi_has_background(background_admin,alice,topsecret) ).
% 0.55/0.82
% 0.55/0.82 fof(ax75,hypothesis,
% 0.55/0.82 hr_admin_indi_has_employment(hr_admin,alice) ).
% 0.55/0.82
% 0.55/0.82 fof(ax76,hypothesis,
% 0.55/0.82 system_indi_needs_level(system,alice,secret) ).
% 0.55/0.82
% 0.55/0.82 fof(ax77,hypothesis,
% 0.55/0.82 level_admin_indi_has_level(level_admin,alice,topsecret) ).
% 0.55/0.82
% 0.55/0.82 fof(ax78,hypothesis,
% 0.55/0.82 system_indi_needs_compartment(system,alice,compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax79,hypothesis,
% 0.55/0.82 system_indi_needs_compartment(system,alice,compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax80,hypothesis,
% 0.55/0.82 sso_indi_has_compartment(sso_compartmentb,alice,compartmentb) ).
% 0.55/0.82
% 0.55/0.82 fof(ax81,hypothesis,
% 0.55/0.82 sso_indi_has_compartment(sso_compartmenta,alice,compartmenta) ).
% 0.55/0.82
% 0.55/0.82 fof(ax82,hypothesis,
% 0.55/0.82 owner_indi_has_need_to_know(owner_secretfile,alice,secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax83,hypothesis,
% 0.55/0.82 owner_indi_has_need_to_know(owner_secretfile,alice,not_secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax84,hypothesis,
% 0.55/0.82 system_indi_has_citizenship(system,babu,india) ).
% 0.55/0.82
% 0.55/0.82 fof(ax85,hypothesis,
% 0.55/0.82 owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(ax86,hypothesis,
% 0.55/0.82 system_indi_is_counterintelligence(system,ci,owner_secretfile) ).
% 0.55/0.82
% 0.55/0.82 fof(babureadnotsecret,conjecture,
% 0.55/0.82 admin_indi_may_file(admin,babu,not_secretfile,read) ).
% 0.55/0.82
% 0.55/0.82 %------------------------------------------------------------------------------
% 0.55/0.82 %-------------------------------------------
% 0.55/0.82 % Proof found
% 0.55/0.82 % SZS status Theorem for theBenchmark
% 0.55/0.82 % SZS output start Proof
% 0.55/0.82 %ClaNum:88(EqnAxiom:0)
% 0.55/0.82 %VarNum:273(SingletonVarNum:129)
% 0.55/0.82 %MaxLitNum:11
% 0.55/0.82 %MaxfuncDepth:2
% 0.55/0.82 %SharedTerms:82
% 0.55/0.82 %goalClause: 59
% 0.55/0.82 %singleGoalClaCount:1
% 0.55/0.82 [1]P1(a1)
% 0.55/0.82 [2]P1(a2)
% 0.55/0.82 [3]P42(a28,a19)
% 0.55/0.82 [4]P53(a28,a20)
% 0.55/0.82 [5]P2(a20,a3)
% 0.55/0.82 [6]P43(a28,a5)
% 0.55/0.82 [7]P3(a5,a3)
% 0.55/0.82 [8]P44(a28,a6)
% 0.55/0.82 [9]P51(a28,a14)
% 0.55/0.82 [10]P29(a14,a3)
% 0.55/0.82 [11]P52(a28,a15)
% 0.55/0.82 [12]P36(a1,a21)
% 0.55/0.82 [13]P36(a2,a22)
% 0.55/0.82 [14]P45(a28,a9,a29)
% 0.55/0.82 [15]P45(a28,a10,a30)
% 0.55/0.82 [16]P30(a19,a9,a23)
% 0.55/0.82 [17]P30(a19,a10,a24)
% 0.55/0.82 [18]P37(a29,a9,a23)
% 0.55/0.82 [19]P37(a30,a10,a24)
% 0.55/0.82 [20]P46(a28,a2,a17)
% 0.55/0.82 [21]P48(a28,a1,a27)
% 0.55/0.82 [22]P48(a28,a2,a31)
% 0.55/0.82 [23]P47(a28,a1,a33)
% 0.55/0.82 [24]P47(a28,a2,a7)
% 0.55/0.82 [25]P4(a6,a3,a32)
% 0.55/0.82 [26]P49(a28,a3,a33)
% 0.55/0.82 [27]P49(a28,a8,a16)
% 0.55/0.82 [28]P54(a28,a3,a27)
% 0.55/0.82 [29]P31(a15,a3,a32)
% 0.55/0.82 [30]P55(a28,a3,a9)
% 0.55/0.82 [31]P55(a28,a3,a10)
% 0.55/0.82 [32]P38(a29,a3,a9)
% 0.55/0.82 [33]P38(a30,a3,a10)
% 0.55/0.82 [34]P34(a21,a3,a1)
% 0.55/0.82 [35]P34(a21,a3,a2)
% 0.55/0.82 [36]P34(a22,a8,a2)
% 0.55/0.82 [37]P50(a28,a11,a21)
% 0.55/0.82 [50]P41(a29,a1,a27,a23)
% 0.55/0.82 [51]P41(a30,a1,a27,a24)
% 0.55/0.82 [52]P40(a29,a1,a33,a23)
% 0.55/0.82 [53]P40(a30,a1,a33,a24)
% 0.55/0.82 [57]P35(a19,a9,a12,a32,a34,a34)
% 0.55/0.82 [58]P35(a19,a10,a25,a31,a18,a18)
% 0.55/0.82 [59]~P23(a4,a8,a2,a26)
% 0.55/0.82 [47]P46(a28,a1,f13(a9,f13(a10,a17)))
% 0.55/0.82 [48]P39(a29,a1,f13(a9,f13(a10,a17)))
% 0.55/0.82 [49]P39(a30,a1,f13(a9,f13(a10,a17)))
% 0.55/0.82 [38]P32(x381,a31,a25)
% 0.55/0.82 [39]P32(x391,a25,a12)
% 0.55/0.82 [40]P32(x401,a12,a27)
% 0.55/0.82 [41]P32(x411,a27,a32)
% 0.55/0.82 [42]P5(a4,x421,a31)
% 0.55/0.82 [43]P14(a4,x431,a7)
% 0.55/0.82 [44]P16(a4,x441,a31)
% 0.55/0.82 [45]P17(a4,x451,a17)
% 0.55/0.82 [46]P33(x461,x462,x462)
% 0.55/0.82 [54]P6(a4,x541,x542,a17)
% 0.55/0.82 [55]P12(a4,x551,x552,a17)
% 0.55/0.82 [56]P7(a4,x561,x562,a17)
% 0.55/0.82 [63]P18(a4,x631,x632)+~P14(a4,x631,a33)
% 0.55/0.82 [64]~P45(a28,x641,x642)+P8(a4,x641,x642)
% 0.55/0.82 [65]~P49(a28,x651,x652)+P14(a4,x651,x652)
% 0.55/0.82 [60]~P2(x602,x601)+~P53(a28,x602)+P24(a4,x601)
% 0.55/0.82 [61]~P3(x612,x611)+~P43(a28,x612)+P19(a4,x611)
% 0.55/0.82 [62]~P29(x622,x621)+~P51(a28,x622)+P21(a4,x621)
% 0.55/0.82 [74]~P6(a4,x741,x742,x742)+~P46(a28,x741,x742)+P11(a4,x741,x742)
% 0.55/0.82 [66]~P34(x663,x661,x662)+~P36(x662,x663)+P25(a4,x661,x662)
% 0.55/0.82 [67]~P17(a4,x671,x673)+P20(a4,x671,x672)+~P11(a4,x672,x673)
% 0.55/0.82 [68]~P16(a4,x681,x683)+P26(a4,x681,x682)+~P13(a4,x682,x683)
% 0.55/0.82 [69]~P14(a4,x691,x693)+P18(a4,x691,x692)+~P10(a4,x692,x693)
% 0.55/0.82 [73]~P36(x732,x733)+~P50(a28,x731,x733)+P23(a4,x731,x732,a26)
% 0.55/0.82 [70]~P33(x701,x702,x704)+P33(x701,x702,x703)+~P32(x701,x704,x703)
% 0.55/0.82 [83]~P35(x833,x832,x834,x835,x836,a18)+P28(a4,x831,x832)+~P42(a28,x833)
% 0.55/0.82 [84]~P35(x843,x842,x844,x845,a18,x846)+P22(a4,x841,x842)+~P42(a28,x843)
% 0.55/0.82 [76]~P12(a4,x761,x762,x763)+~P48(a28,x761,x762)+P13(a4,x761,x762)+~P11(a4,x761,x763)
% 0.55/0.82 [77]~P7(a4,x771,x772,x773)+~P47(a28,x771,x772)+P10(a4,x771,x772)+~P11(a4,x771,x773)
% 0.55/0.82 [71]~P4(x713,x711,x714)+~P33(a4,x712,x714)+P5(a4,x711,x712)+~P44(a28,x713)
% 0.55/0.82 [79]~P39(x795,x791,x792)+~P6(a4,x791,x792,x794)+~P8(a4,x793,x795)+P6(a4,x791,x792,f13(x793,x794))
% 0.55/0.82 [85]~P35(x853,x852,x854,x855,x856,a34)+P28(a4,x851,x852)+~P24(a4,x851)+~P42(a28,x853)
% 0.55/0.82 [86]~P35(x863,x862,x864,x865,a34,x866)+P22(a4,x861,x862)+~P19(a4,x861)+~P42(a28,x863)
% 0.55/0.82 [87]~P35(x873,x872,x875,x874,x876,x877)+P15(a4,x871,x872)+~P5(a4,x871,x874)+~P42(a28,x873)
% 0.55/0.82 [88]~P35(x883,x882,x884,x885,x886,x887)+P27(a4,x881,x882)+~P16(a4,x881,x884)+~P42(a28,x883)
% 0.55/0.82 [72]~P30(x723,x721,x722)+~P37(x724,x721,x722)+~P8(a4,x721,x724)+P9(a4,x721,x722)+~P42(a28,x723)
% 0.55/0.82 [81]~P41(x815,x811,x812,x816)+~P12(a4,x811,x812,x814)+~P8(a4,x813,x815)+~P9(a4,x813,x816)+P12(a4,x811,x812,f13(x813,x814))
% 0.55/0.82 [82]~P40(x825,x821,x822,x826)+~P7(a4,x821,x822,x824)+~P8(a4,x823,x825)+~P9(a4,x823,x826)+P7(a4,x821,x822,f13(x823,x824))
% 0.55/0.82 [75]~P1(x752)+~P20(a4,x751,x752)+~P26(a4,x751,x752)+~P25(a4,x751,x752)+~P18(a4,x751,x752)+P23(a4,x751,x752,a26)
% 0.55/0.82 [80]~P38(x804,x801,x802)+~P8(a4,x802,x804)+~P17(a4,x801,x803)+~P55(a28,x801,x802)+~P28(a4,x801,x802)+~P22(a4,x801,x802)+~P15(a4,x801,x802)+~P27(a4,x801,x802)+~P21(a4,x801)+~P14(a4,x801,a33)+P17(a4,x801,f13(x802,x803))
% 0.55/0.82 [78]~P31(x783,x781,x784)+~P33(a4,x782,x784)+~P5(a4,x781,x782)+~P54(a28,x781,x785)+P16(a4,x781,x782)+~P33(a4,x782,x785)+~P24(a4,x781)+~P19(a4,x781)+~P21(a4,x781)+~P52(a28,x783)+~P14(a4,x781,a33)
% 0.55/0.82 %EqnAxiom
% 0.55/0.82
% 0.55/0.82 %-------------------------------------------
% 0.55/0.82 cnf(100,plain,
% 0.55/0.82 (P33(x1001,a31,a25)),
% 0.55/0.82 inference(scs_inference,[],[59,13,46,54,20,38,4,5,6,7,9,10,73,74,60,61,62,70])).
% 0.55/0.82 cnf(102,plain,
% 0.55/0.82 (P33(x1021,x1022,x1022)),
% 0.55/0.83 inference(rename_variables,[],[46])).
% 0.55/0.83 cnf(131,plain,
% 0.55/0.83 (~P25(a4,a8,a2)),
% 0.55/0.83 inference(scs_inference,[],[59,45,2,13,43,44,46,102,54,55,56,42,20,22,24,38,3,4,5,6,7,8,9,10,25,57,58,73,74,60,61,62,70,83,84,76,77,71,85,86,87,67,68,69,88,75])).
% 0.55/0.83 cnf(140,plain,
% 0.55/0.83 ($false),
% 0.55/0.83 inference(scs_inference,[],[59,131,13,36,100,39,73,70,66]),
% 0.55/0.83 ['proof']).
% 0.55/0.83 % SZS output end Proof
% 0.55/0.83 % Total time :0.010000s
%------------------------------------------------------------------------------