%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV437+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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 240.81s 240.81s
% Output : CNFRefutation 242.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV437+1 : TPTP v8.2.0. Released v4.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n017.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 20:42:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 240.72/240.75 %-------------------------------------------
% 240.72/240.75 % File :CSE---1.7
% 240.72/240.75 % Problem :theBenchmark
% 240.72/240.75 % Transform :cnf
% 240.72/240.75 % Format :tptp:raw
% 240.72/240.75 % Command :java -jar mcs_scs.jar %d %s
% 240.72/240.75
% 240.72/240.75 % Result :Theorem 240.100000s
% 240.72/240.75 % Output :CNFRefutation 240.100000s
% 240.72/240.75 %-------------------------------------------
% 240.81/240.81 %------------------------------------------------------------------------------
% 240.81/240.81 % File : SWV437+1 : TPTP v8.2.0. Released v4.0.0.
% 240.81/240.81 % Domain : Software Verification (Security)
% 240.81/240.81 % Problem : Can Alice read the secret file?
% 240.81/240.81 % Version : [Gar09] axioms.
% 240.81/240.81 % English :
% 240.81/240.81
% 240.81/240.81 % Refs : [Gar09] Garg (2006), Email to Geoff Sutcliffe
% 240.81/240.81 % Source : [Gar09]
% 240.81/240.81 % Names :
% 240.81/240.81
% 240.81/240.81 % Status : Theorem
% 240.81/240.81 % Rating : 0.06 v8.2.0, 0.07 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.27 v6.1.0, 0.20 v6.0.0, 0.50 v5.5.0, 0.29 v5.4.0, 0.26 v5.3.0, 0.30 v5.2.0, 0.14 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0
% 240.81/240.81 % Syntax : Number of formulae : 88 ( 59 unt; 0 def)
% 240.81/240.81 % Number of atoms : 176 ( 0 equ)
% 240.81/240.81 % Maximal formula atoms : 11 ( 2 avg)
% 240.81/240.81 % Number of connectives : 88 ( 0 ~; 0 |; 0 &)
% 240.81/240.81 % ( 0 <=>; 88 =>; 0 <=; 0 <~>)
% 240.81/240.81 % Maximal formula depth : 16 ( 3 avg)
% 240.81/240.81 % Maximal term depth : 3 ( 1 avg)
% 240.81/240.81 % Number of predicates : 55 ( 55 usr; 0 prp; 1-6 aty)
% 240.81/240.81 % Number of functors : 34 ( 34 usr; 33 con; 0-2 aty)
% 240.81/240.81 % Number of variables : 129 ( 129 !; 0 ?)
% 240.81/240.81 % SPC : FOF_THM_RFO_NEQ
% 240.81/240.81
% 240.81/240.81 % Comments : Formalization of policies governing access to classified
% 240.81/240.81 % information in the intelligence community in USA.
% 240.81/240.81 %------------------------------------------------------------------------------
% 240.81/240.81 %----Include axioms
% 240.81/240.81 include('Axioms/SWV009+0.ax').
% 240.81/240.81 %------------------------------------------------------------------------------
% 240.81/240.81 fof(ax41,hypothesis,
% 240.81/240.81 system_indi_is_oca(system,oca) ).
% 240.81/240.81
% 240.81/240.81 fof(ax42,hypothesis,
% 240.81/240.81 oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes) ).
% 240.81/240.81
% 240.81/240.81 fof(ax43,hypothesis,
% 240.81/240.81 oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no) ).
% 240.81/240.81
% 240.81/240.81 fof(ax44,hypothesis,
% 240.81/240.81 system_compartment_has_sso(system,compartmentb,sso_compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax45,hypothesis,
% 240.81/240.81 oca_compartment_has_scg(oca,compartmentb,scg_compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax46,hypothesis,
% 240.81/240.81 sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax47,hypothesis,
% 240.81/240.81 system_compartment_has_sso(system,compartmenta,sso_compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax48,hypothesis,
% 240.81/240.81 oca_compartment_has_scg(oca,compartmenta,scg_compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax49,hypothesis,
% 240.81/240.81 sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax50,hypothesis,
% 240.81/240.81 state_file_is_not_working_paper(secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax51,hypothesis,
% 240.81/240.81 system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))) ).
% 240.81/240.81
% 240.81/240.81 fof(ax52,hypothesis,
% 240.81/240.81 sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))) ).
% 240.81/240.81
% 240.81/240.81 fof(ax53,hypothesis,
% 240.81/240.81 sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))) ).
% 240.81/240.81
% 240.81/240.81 fof(ax54,hypothesis,
% 240.81/240.81 system_file_needs_level(system,secretfile,secret) ).
% 240.81/240.81
% 240.81/240.81 fof(ax55,hypothesis,
% 240.81/240.81 sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax56,hypothesis,
% 240.81/240.81 sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax57,hypothesis,
% 240.81/240.81 system_file_needs_citizenship(system,secretfile,usa) ).
% 240.81/240.81
% 240.81/240.81 fof(ax58,hypothesis,
% 240.81/240.81 sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax59,hypothesis,
% 240.81/240.81 sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax60,hypothesis,
% 240.81/240.81 state_file_has_owner(secretfile,owner_secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax61,hypothesis,
% 240.81/240.81 state_file_is_not_working_paper(not_secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax62,hypothesis,
% 240.81/240.81 system_file_needs_compartments(system,not_secretfile,nil) ).
% 240.81/240.81
% 240.81/240.81 fof(ax63,hypothesis,
% 240.81/240.81 system_file_needs_level(system,not_secretfile,unclassified) ).
% 240.81/240.81
% 240.81/240.81 fof(ax64,hypothesis,
% 240.81/240.81 system_file_needs_citizenship(system,not_secretfile,anycountry) ).
% 240.81/240.81
% 240.81/240.81 fof(ax65,hypothesis,
% 240.81/240.81 state_file_has_owner(not_secretfile,owner_not_secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax66,hypothesis,
% 240.81/240.81 system_indi_is_polygraph_admin(system,polygraph_admin) ).
% 240.81/240.81
% 240.81/240.81 fof(ax67,hypothesis,
% 240.81/240.81 system_indi_is_credit_admin(system,credit_admin) ).
% 240.81/240.81
% 240.81/240.81 fof(ax68,hypothesis,
% 240.81/240.81 system_indi_is_background_admin(system,background_admin) ).
% 240.81/240.81
% 240.81/240.81 fof(ax69,hypothesis,
% 240.81/240.81 system_indi_is_hr_admin(system,hr_admin) ).
% 240.81/240.81
% 240.81/240.81 fof(ax70,hypothesis,
% 240.81/240.81 system_indi_is_level_admin(system,level_admin) ).
% 240.81/240.81
% 240.81/240.81 fof(ax71,hypothesis,
% 240.81/240.81 system_indi_has_citizenship(system,alice,usa) ).
% 240.81/240.81
% 240.81/240.81 fof(ax72,hypothesis,
% 240.81/240.81 polygraph_admin_indi_has_polygraph(polygraph_admin,alice) ).
% 240.81/240.81
% 240.81/240.81 fof(ax73,hypothesis,
% 240.81/240.81 credit_admin_indi_has_credit(credit_admin,alice) ).
% 240.81/240.81
% 240.81/240.81 fof(ax74,hypothesis,
% 240.81/240.81 background_admin_indi_has_background(background_admin,alice,topsecret) ).
% 240.81/240.81
% 240.81/240.81 fof(ax75,hypothesis,
% 240.81/240.81 hr_admin_indi_has_employment(hr_admin,alice) ).
% 240.81/240.81
% 240.81/240.81 fof(ax76,hypothesis,
% 240.81/240.81 system_indi_needs_level(system,alice,secret) ).
% 240.81/240.81
% 240.81/240.81 fof(ax77,hypothesis,
% 240.81/240.81 level_admin_indi_has_level(level_admin,alice,topsecret) ).
% 240.81/240.81
% 240.81/240.81 fof(ax78,hypothesis,
% 240.81/240.81 system_indi_needs_compartment(system,alice,compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax79,hypothesis,
% 240.81/240.81 system_indi_needs_compartment(system,alice,compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax80,hypothesis,
% 240.81/240.81 sso_indi_has_compartment(sso_compartmentb,alice,compartmentb) ).
% 240.81/240.81
% 240.81/240.81 fof(ax81,hypothesis,
% 240.81/240.81 sso_indi_has_compartment(sso_compartmenta,alice,compartmenta) ).
% 240.81/240.81
% 240.81/240.81 fof(ax82,hypothesis,
% 240.81/240.81 owner_indi_has_need_to_know(owner_secretfile,alice,secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax83,hypothesis,
% 240.81/240.81 owner_indi_has_need_to_know(owner_secretfile,alice,not_secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax84,hypothesis,
% 240.81/240.81 system_indi_has_citizenship(system,babu,india) ).
% 240.81/240.81
% 240.81/240.81 fof(ax85,hypothesis,
% 240.81/240.81 owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(ax86,hypothesis,
% 240.81/240.81 system_indi_is_counterintelligence(system,ci,owner_secretfile) ).
% 240.81/240.81
% 240.81/240.81 fof(alicereadsecret,conjecture,
% 240.81/240.81 admin_indi_may_file(admin,alice,secretfile,read) ).
% 240.81/240.81
% 240.81/240.81 %------------------------------------------------------------------------------
% 240.81/240.81 %-------------------------------------------
% 240.81/240.81 % Proof found
% 240.81/240.81 % SZS status Theorem for theBenchmark
% 240.81/240.81 % SZS output start Proof
% 240.90/240.86 %ClaNum:88(EqnAxiom:0)
% 240.90/240.86 %VarNum:273(SingletonVarNum:129)
% 240.90/240.86 %MaxLitNum:11
% 240.90/240.86 %MaxfuncDepth:2
% 240.90/240.87 %SharedTerms:82
% 240.90/240.87 %goalClause: 59
% 240.90/240.87 %singleGoalClaCount:1
% 240.90/240.87 [1]P1(a1)
% 240.90/240.87 [2]P1(a2)
% 240.90/240.87 [3]P42(a28,a19)
% 240.90/240.87 [4]P53(a28,a20)
% 240.90/240.87 [5]P2(a20,a3)
% 240.90/240.87 [6]P43(a28,a5)
% 240.90/240.87 [7]P3(a5,a3)
% 240.90/240.87 [8]P44(a28,a6)
% 240.90/240.87 [9]P51(a28,a14)
% 240.90/240.87 [10]P29(a14,a3)
% 240.90/240.87 [11]P52(a28,a15)
% 240.90/240.87 [12]P36(a1,a21)
% 240.90/240.87 [13]P36(a2,a22)
% 240.90/240.87 [14]P45(a28,a9,a29)
% 240.90/240.87 [15]P45(a28,a10,a30)
% 240.90/240.87 [16]P30(a19,a9,a23)
% 240.90/240.87 [17]P30(a19,a10,a24)
% 240.90/240.87 [18]P37(a29,a9,a23)
% 240.90/240.87 [19]P37(a30,a10,a24)
% 240.90/240.87 [20]P46(a28,a2,a17)
% 240.90/240.87 [21]P48(a28,a1,a27)
% 240.90/240.87 [22]P48(a28,a2,a31)
% 240.90/240.87 [23]P47(a28,a1,a33)
% 240.90/240.87 [24]P47(a28,a2,a7)
% 240.90/240.87 [25]P4(a6,a3,a32)
% 240.90/240.87 [26]P49(a28,a3,a33)
% 240.90/240.87 [27]P49(a28,a8,a16)
% 240.90/240.87 [28]P54(a28,a3,a27)
% 240.90/240.87 [29]P31(a15,a3,a32)
% 240.90/240.87 [30]P55(a28,a3,a9)
% 240.90/240.87 [31]P55(a28,a3,a10)
% 240.90/240.87 [32]P38(a29,a3,a9)
% 240.90/240.87 [33]P38(a30,a3,a10)
% 240.90/240.87 [34]P34(a21,a3,a1)
% 240.90/240.87 [35]P34(a21,a3,a2)
% 240.90/240.87 [36]P34(a22,a8,a2)
% 240.90/240.87 [37]P50(a28,a11,a21)
% 240.90/240.87 [50]P41(a29,a1,a27,a23)
% 240.90/240.87 [51]P41(a30,a1,a27,a24)
% 240.90/240.87 [52]P40(a29,a1,a33,a23)
% 240.90/240.87 [53]P40(a30,a1,a33,a24)
% 240.90/240.87 [57]P35(a19,a9,a12,a32,a34,a34)
% 240.90/240.87 [58]P35(a19,a10,a25,a31,a18,a18)
% 240.90/240.87 [59]~P23(a4,a3,a1,a26)
% 240.90/240.87 [47]P46(a28,a1,f13(a9,f13(a10,a17)))
% 240.90/240.87 [48]P39(a29,a1,f13(a9,f13(a10,a17)))
% 240.90/240.87 [49]P39(a30,a1,f13(a9,f13(a10,a17)))
% 240.90/240.87 [38]P32(x381,a31,a25)
% 240.90/240.87 [39]P32(x391,a25,a12)
% 240.90/240.87 [40]P32(x401,a12,a27)
% 240.90/240.87 [41]P32(x411,a27,a32)
% 240.90/240.87 [42]P5(a4,x421,a31)
% 240.90/240.87 [43]P14(a4,x431,a7)
% 240.90/240.87 [44]P16(a4,x441,a31)
% 240.90/240.87 [45]P17(a4,x451,a17)
% 240.90/240.87 [46]P33(x461,x462,x462)
% 240.90/240.87 [54]P6(a4,x541,x542,a17)
% 240.90/240.87 [55]P12(a4,x551,x552,a17)
% 240.90/240.87 [56]P7(a4,x561,x562,a17)
% 240.90/240.87 [63]P18(a4,x631,x632)+~P14(a4,x631,a33)
% 240.90/240.87 [64]~P45(a28,x641,x642)+P8(a4,x641,x642)
% 240.90/240.87 [65]~P49(a28,x651,x652)+P14(a4,x651,x652)
% 240.90/240.87 [60]~P2(x602,x601)+~P53(a28,x602)+P24(a4,x601)
% 240.90/240.87 [61]~P3(x612,x611)+~P43(a28,x612)+P19(a4,x611)
% 240.90/240.87 [62]~P29(x622,x621)+~P51(a28,x622)+P21(a4,x621)
% 240.90/240.87 [74]~P6(a4,x741,x742,x742)+~P46(a28,x741,x742)+P11(a4,x741,x742)
% 240.90/240.87 [66]~P34(x663,x661,x662)+~P36(x662,x663)+P25(a4,x661,x662)
% 240.90/240.87 [67]~P17(a4,x671,x673)+P20(a4,x671,x672)+~P11(a4,x672,x673)
% 240.90/240.87 [68]~P16(a4,x681,x683)+P26(a4,x681,x682)+~P13(a4,x682,x683)
% 240.90/240.87 [69]~P14(a4,x691,x693)+P18(a4,x691,x692)+~P10(a4,x692,x693)
% 240.90/240.87 [73]~P36(x732,x733)+~P50(a28,x731,x733)+P23(a4,x731,x732,a26)
% 240.90/240.87 [70]~P33(x701,x702,x704)+P33(x701,x702,x703)+~P32(x701,x704,x703)
% 240.90/240.87 [83]~P35(x833,x832,x834,x835,x836,a18)+P28(a4,x831,x832)+~P42(a28,x833)
% 240.90/240.87 [84]~P35(x843,x842,x844,x845,a18,x846)+P22(a4,x841,x842)+~P42(a28,x843)
% 240.90/240.87 [76]~P12(a4,x761,x762,x763)+~P48(a28,x761,x762)+P13(a4,x761,x762)+~P11(a4,x761,x763)
% 240.90/240.87 [77]~P7(a4,x771,x772,x773)+~P47(a28,x771,x772)+P10(a4,x771,x772)+~P11(a4,x771,x773)
% 240.90/240.87 [71]~P4(x713,x711,x714)+~P33(a4,x712,x714)+P5(a4,x711,x712)+~P44(a28,x713)
% 240.90/240.87 [79]~P39(x795,x791,x792)+~P6(a4,x791,x792,x794)+~P8(a4,x793,x795)+P6(a4,x791,x792,f13(x793,x794))
% 240.90/240.87 [85]~P35(x853,x852,x854,x855,x856,a34)+P28(a4,x851,x852)+~P24(a4,x851)+~P42(a28,x853)
% 240.90/240.87 [86]~P35(x863,x862,x864,x865,a34,x866)+P22(a4,x861,x862)+~P19(a4,x861)+~P42(a28,x863)
% 240.90/240.87 [87]~P35(x873,x872,x875,x874,x876,x877)+P15(a4,x871,x872)+~P5(a4,x871,x874)+~P42(a28,x873)
% 240.90/240.87 [88]~P35(x883,x882,x884,x885,x886,x887)+P27(a4,x881,x882)+~P16(a4,x881,x884)+~P42(a28,x883)
% 240.90/240.87 [72]~P30(x723,x721,x722)+~P37(x724,x721,x722)+~P8(a4,x721,x724)+P9(a4,x721,x722)+~P42(a28,x723)
% 240.90/240.87 [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))
% 240.90/240.87 [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))
% 240.90/240.87 [75]~P1(x752)+~P20(a4,x751,x752)+~P26(a4,x751,x752)+~P25(a4,x751,x752)+~P18(a4,x751,x752)+P23(a4,x751,x752,a26)
% 240.90/240.87 [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))
% 240.90/240.87 [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)
% 240.90/240.87 %EqnAxiom
% 240.90/240.87
% 240.90/240.87 %-------------------------------------------
% 241.93/241.87 cnf(94,plain,
% 241.93/241.87 (P24(a4,a3)),
% 241.93/241.87 inference(scs_inference,[],[59,12,54,20,4,5,73,74,60])).
% 241.93/241.87 cnf(96,plain,
% 241.93/241.87 (P19(a4,a3)),
% 241.93/241.87 inference(scs_inference,[],[59,12,54,20,4,5,6,7,73,74,60,61])).
% 241.93/241.87 cnf(98,plain,
% 241.93/241.87 (P21(a4,a3)),
% 241.93/241.87 inference(scs_inference,[],[59,12,54,20,4,5,6,7,9,10,73,74,60,61,62])).
% 241.93/241.87 cnf(100,plain,
% 241.93/241.87 (P33(x1001,a31,a25)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,54,20,38,4,5,6,7,9,10,73,74,60,61,62,70])).
% 241.93/241.87 cnf(102,plain,
% 241.93/241.87 (P33(x1021,x1022,x1022)),
% 241.93/241.87 inference(rename_variables,[],[46])).
% 241.93/241.87 cnf(104,plain,
% 241.93/241.87 (P28(a4,x1041,a10)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,54,20,38,3,4,5,6,7,9,10,58,73,74,60,61,62,70,83])).
% 241.93/241.87 cnf(106,plain,
% 241.93/241.87 (P22(a4,x1061,a10)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,54,20,38,3,4,5,6,7,9,10,58,73,74,60,61,62,70,83,84])).
% 241.93/241.87 cnf(114,plain,
% 241.93/241.87 (P5(a4,a3,a32)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,102,54,55,56,20,22,24,38,3,4,5,6,7,8,9,10,25,58,73,74,60,61,62,70,83,84,76,77,71])).
% 241.93/241.87 cnf(117,plain,
% 241.93/241.87 (P28(a4,a3,a9)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,102,54,55,56,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])).
% 241.93/241.87 cnf(119,plain,
% 241.93/241.87 (P22(a4,a3,a9)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,102,54,55,56,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])).
% 241.93/241.87 cnf(121,plain,
% 241.93/241.87 (P15(a4,x1211,a10)),
% 241.93/241.87 inference(scs_inference,[],[59,12,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])).
% 241.93/241.87 cnf(123,plain,
% 241.93/241.87 (P20(a4,x1231,a2)),
% 241.93/241.87 inference(scs_inference,[],[59,12,45,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])).
% 241.93/241.87 cnf(125,plain,
% 241.93/241.87 (P26(a4,x1251,a2)),
% 241.93/241.87 inference(scs_inference,[],[59,12,45,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])).
% 241.93/241.87 cnf(127,plain,
% 241.93/241.87 (P18(a4,x1271,a2)),
% 241.93/241.87 inference(scs_inference,[],[59,12,45,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])).
% 241.93/241.87 cnf(131,plain,
% 241.93/241.87 (~P8(a4,a9,a29)+P9(a4,a9,a23)),
% 241.93/241.87 inference(scs_inference,[],[59,12,45,43,44,46,102,54,55,56,42,20,22,24,38,3,4,5,6,7,8,9,10,16,18,25,57,58,73,74,60,61,62,70,83,84,76,77,71,85,86,87,67,68,69,88,72])).
% 241.93/241.87 cnf(133,plain,
% 241.93/241.87 (~P26(a4,a3,a1)+~P25(a4,a3,a1)+~P18(a4,a3,a1)+~P20(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[59,12,45,1,43,44,46,102,54,55,56,42,20,22,24,38,3,4,5,6,7,8,9,10,16,18,25,57,58,73,74,60,61,62,70,83,84,76,77,71,85,86,87,67,68,69,75])).
% 241.93/241.87 cnf(134,plain,
% 241.93/241.87 (P33(x1341,a31,a12)),
% 241.93/241.87 inference(scs_inference,[],[100,39,70])).
% 241.93/241.87 cnf(139,plain,
% 241.93/241.87 (P15(a4,a3,a9)),
% 241.93/241.87 inference(scs_inference,[],[59,12,100,114,39,57,3,70,73,87])).
% 241.93/241.87 cnf(141,plain,
% 241.93/241.87 (~P6(a4,a1,f13(a9,f13(a10,a17)),f13(a9,f13(a10,a17)))+P11(a4,a1,f13(a9,f13(a10,a17)))),
% 241.93/241.87 inference(scs_inference,[],[59,12,100,114,47,39,57,3,70,73,87,74])).
% 241.93/241.87 cnf(147,plain,
% 241.93/241.87 (P33(x1471,a31,a27)),
% 241.93/241.87 inference(scs_inference,[],[59,12,134,40,73,70])).
% 241.93/241.87 cnf(150,plain,
% 241.93/241.87 (P13(a4,a1,a27)+~P11(a4,a1,a17)),
% 241.93/241.87 inference(scs_inference,[],[59,12,134,55,21,40,73,70,76])).
% 241.93/241.87 cnf(166,plain,
% 241.93/241.87 (~P8(a4,a10,a30)+P9(a4,a10,a24)),
% 241.93/241.87 inference(scs_inference,[],[59,12,44,147,23,56,3,41,17,19,70,73,88,77,72])).
% 241.93/241.87 cnf(171,plain,
% 241.93/241.87 (P33(x1711,a25,a12)),
% 241.93/241.87 inference(scs_inference,[],[59,12,46,39,73,70])).
% 241.93/241.87 cnf(178,plain,
% 241.93/241.87 (P33(x1781,a25,a27)),
% 241.93/241.87 inference(scs_inference,[],[171,40,70])).
% 241.93/241.87 cnf(188,plain,
% 241.93/241.87 (P33(x1881,a25,a32)),
% 241.93/241.87 inference(scs_inference,[],[59,12,178,41,73,70])).
% 241.93/241.87 cnf(239,plain,
% 241.93/241.87 (P18(a4,a3,x2391)),
% 241.93/241.87 inference(scs_inference,[],[26,63,65])).
% 241.93/241.87 cnf(240,plain,
% 241.93/241.87 (~P26(a4,a3,a1)+~P25(a4,a3,a1)+~P20(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[239,133])).
% 241.93/241.87 cnf(325,plain,
% 241.93/241.87 (P9(a4,a9,a23)),
% 241.93/241.87 inference(scs_inference,[],[14,64,131])).
% 241.93/241.87 cnf(598,plain,
% 241.93/241.87 (P9(a4,a10,a24)),
% 241.93/241.87 inference(scs_inference,[],[15,166,64])).
% 241.93/241.87 cnf(689,plain,
% 241.93/241.87 (~P6(a4,a1,f13(a9,f13(a10,a17)),f13(a9,f13(a10,a17)))+~P17(a4,x6891,f13(a9,f13(a10,a17)))+P20(a4,x6891,a1)),
% 241.93/241.87 inference(scs_inference,[],[141,67])).
% 241.93/241.87 cnf(780,plain,
% 241.93/241.87 (~P26(a4,a3,a1)+~P20(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[12,34,66,240])).
% 241.93/241.87 cnf(1606,plain,
% 241.93/241.87 (P5(a4,a3,a25)),
% 241.93/241.87 inference(scs_inference,[],[59,12,188,8,25,73,71])).
% 241.93/241.87 cnf(2074,plain,
% 241.93/241.87 (P33(x20741,a12,a27)),
% 241.93/241.87 inference(scs_inference,[],[46,40,70])).
% 241.93/241.87 cnf(2087,plain,
% 241.93/241.87 (P33(x20871,a12,a32)),
% 241.93/241.87 inference(scs_inference,[],[2074,41,70])).
% 241.93/241.87 cnf(2101,plain,
% 241.93/241.87 (P5(a4,a3,a12)),
% 241.93/241.87 inference(scs_inference,[],[59,12,2087,8,25,73,71])).
% 241.93/241.87 cnf(3068,plain,
% 241.93/241.87 (P33(x30681,a27,a32)),
% 241.93/241.87 inference(scs_inference,[],[46,41,70])).
% 241.93/241.87 cnf(3082,plain,
% 241.93/241.87 (P5(a4,a3,a27)),
% 241.93/241.87 inference(scs_inference,[],[59,12,3068,8,25,73,71])).
% 241.93/241.87 cnf(3647,plain,
% 241.93/241.87 (~P8(a4,a10,a30)+~P27(a4,a3,a10)+P17(a4,a3,f13(a10,a17))),
% 241.93/241.87 inference(scs_inference,[],[26,98,31,104,106,121,45,33,65,80])).
% 241.93/241.87 cnf(3779,plain,
% 241.93/241.87 (P17(a4,a3,f13(a10,a17))+~P27(a4,a3,a10)),
% 241.93/241.87 inference(scs_inference,[],[15,3647,64])).
% 241.93/241.87 cnf(5315,plain,
% 241.93/241.87 (~P11(a4,a1,a17)+~P16(a4,x53151,a27)+P26(a4,x53151,a1)),
% 241.93/241.87 inference(scs_inference,[],[150,68])).
% 241.93/241.87 cnf(238466,plain,
% 241.93/241.87 (P8(a4,a10,a30)),
% 241.93/241.87 inference(scs_inference,[],[15,64])).
% 241.93/241.87 cnf(238470,plain,
% 241.93/241.87 (P25(a4,a8,a2)),
% 241.93/241.87 inference(scs_inference,[],[13,36,27,15,64,65,66])).
% 241.93/241.87 cnf(238490,plain,
% 241.93/241.87 (P8(a4,a9,a29)),
% 241.93/241.87 inference(scs_inference,[],[14,64])).
% 241.93/241.87 cnf(238492,plain,
% 241.93/241.87 (P14(a4,a3,a33)),
% 241.93/241.87 inference(scs_inference,[],[14,26,64,65])).
% 241.93/241.87 cnf(238498,plain,
% 241.93/241.87 (P12(a4,a1,a27,f13(a10,a17))),
% 241.93/241.87 inference(scs_inference,[],[238466,34,37,51,598,14,26,12,55,64,65,66,73,81])).
% 241.93/241.87 cnf(238501,plain,
% 241.93/241.87 (P7(a4,a1,a33,f13(a10,a17))),
% 241.93/241.87 inference(scs_inference,[],[238466,34,37,51,53,598,14,26,56,12,55,64,65,66,73,81,82])).
% 241.93/241.87 cnf(238538,plain,
% 241.93/241.87 (P16(a4,a3,a12)),
% 241.93/241.87 inference(scs_inference,[],[238492,238470,127,37,123,125,2,28,29,11,98,96,12,2074,2087,94,2101,73,75,78])).
% 241.93/241.87 cnf(238546,plain,
% 241.93/241.87 (P27(a4,a3,a9)),
% 241.93/241.87 inference(scs_inference,[],[238538,37,12,57,3,73,88])).
% 241.93/241.87 cnf(238578,plain,
% 241.93/241.87 (~P16(a4,x2385781,a25)+P27(a4,x2385781,a10)),
% 241.93/241.87 inference(scs_inference,[],[238470,127,37,123,125,2,12,58,3,73,75,88])).
% 241.93/241.87 cnf(238593,plain,
% 241.93/241.87 (P27(a4,a3,a10)),
% 241.93/241.87 inference(scs_inference,[],[238492,238470,28,127,37,123,125,2,29,11,98,96,12,178,188,94,1606,73,75,78,238578])).
% 241.93/241.87 cnf(238595,plain,
% 241.93/241.87 (P17(a4,a3,f13(a10,a17))),
% 241.93/241.87 inference(scs_inference,[],[238593,3779])).
% 241.93/241.87 cnf(238605,plain,
% 241.93/241.87 (P16(a4,a3,a27)),
% 241.93/241.87 inference(scs_inference,[],[35,238492,238470,28,127,37,123,125,2,29,11,98,96,12,3068,46,94,3082,73,75,66,78])).
% 241.93/241.87 cnf(238609,plain,
% 241.93/241.87 (~P11(a4,a1,a17)+P26(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[35,238492,238470,28,127,37,123,125,2,29,11,98,96,12,3068,46,94,3082,73,75,66,78,5315])).
% 241.93/241.87 cnf(238615,plain,
% 241.93/241.87 (P12(a4,a1,a27,f13(a9,f13(a10,a17)))),
% 241.93/241.87 inference(scs_inference,[],[238501,238498,238490,50,52,325,37,12,73,82,81])).
% 241.93/241.87 cnf(238622,plain,
% 241.93/241.87 (P17(a4,a3,f13(a9,f13(a10,a17)))),
% 241.93/241.87 inference(scs_inference,[],[238595,238546,238501,238498,238490,117,119,139,30,32,50,52,325,238492,238470,127,37,123,125,2,98,12,73,82,81,75,80])).
% 241.93/241.87 cnf(238677,plain,
% 241.93/241.87 (~P11(a4,a1,f13(a9,f13(a10,a17)))+P13(a4,a1,a27)),
% 241.93/241.87 inference(scs_inference,[],[238615,35,238470,127,37,123,125,2,12,21,73,75,66,76])).
% 241.93/241.87 cnf(238726,plain,
% 241.93/241.87 (P6(a4,a1,f13(a9,f13(a10,a17)),f13(a10,a17))),
% 241.93/241.87 inference(scs_inference,[],[49,238466,238470,127,37,123,125,2,12,54,73,75,79])).
% 241.93/241.87 cnf(238765,plain,
% 241.93/241.87 (~P13(a4,x2387651,a27)+P26(a4,a3,x2387651)),
% 241.93/241.87 inference(scs_inference,[],[238605,238470,127,37,123,125,2,12,73,75,68])).
% 241.93/241.87 cnf(241220,plain,
% 241.93/241.87 (~P11(a4,a1,f13(a9,f13(a10,a17)))+P26(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[238677,238765])).
% 241.93/241.87 cnf(737394,plain,
% 241.93/241.87 (~P6(a4,a1,f13(a9,f13(a10,a17)),f13(a9,f13(a10,a17)))+P20(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[238622,37,238470,127,123,125,2,12,73,75,689])).
% 241.93/241.87 cnf(737439,plain,
% 241.93/241.87 (P20(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[238490,48,238726,737394,79])).
% 241.93/241.87 cnf(737440,plain,
% 241.93/241.87 (~P26(a4,a3,a1)),
% 241.93/241.87 inference(scs_inference,[],[737439,780])).
% 241.93/241.87 cnf(737451,plain,
% 241.93/241.87 (~P11(a4,a1,a17)),
% 241.93/241.87 inference(scs_inference,[],[737440,238609])).
% 241.93/241.87 cnf(737454,plain,
% 241.93/241.87 (~P11(a4,a1,f13(a9,f13(a10,a17)))),
% 241.93/241.87 inference(scs_inference,[],[737440,241220])).
% 241.93/241.87 cnf(737464,plain,
% 241.93/241.87 (~P6(a4,a1,f13(a9,f13(a10,a17)),f13(a9,f13(a10,a17)))),
% 241.93/241.87 inference(scs_inference,[],[737454,141])).
% 241.93/241.87 cnf(737480,plain,
% 241.93/241.87 ($false),
% 241.93/241.87 inference(scs_inference,[],[737464,737451,238726,48,238490,54,37,12,74,73,79]),
% 241.93/241.87 ['proof']).
% 242.50/242.47 % SZS output end Proof
% 242.50/242.47 % Total time :240.100000s
%------------------------------------------------------------------------------