%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : AGT003+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 03:38:16 EDT 2024
% Result : Theorem 0.56s 1.00s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : AGT003+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n029.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 : Wed Jun 19 04:04:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.55/0.58 start to proof:theBenchmark
% 0.56/0.99 %-------------------------------------------
% 0.56/0.99 % File :CSE---1.7
% 0.56/0.99 % Problem :theBenchmark
% 0.56/0.99 % Transform :cnf
% 0.56/0.99 % Format :tptp:raw
% 0.56/0.99 % Command :java -jar mcs_scs.jar %d %s
% 0.56/0.99
% 0.56/0.99 % Result :Theorem 0.190000s
% 0.56/0.99 % Output :CNFRefutation 0.190000s
% 0.56/0.99 %-------------------------------------------
% 0.56/1.00 %--------------------------------------------------------------------------
% 0.56/1.00 % File : AGT003+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.56/1.00 % Domain : Agents
% 0.56/1.00 % Problem : Problem for the CPlanT system
% 0.56/1.00 % Version : [Bar03] axioms : Especial.
% 0.56/1.00 % English :
% 0.56/1.00
% 0.56/1.00 % Refs : [Bar03] Barta, J. (2003), Email to G. Sutcliffe
% 0.56/1.00 % : [BT+03] Barta et al. (2003), Meta-Reasoning in CPlanT Multi-Ag
% 0.56/1.00 % : [TBP03] Tozicka et al. (2003), Meta-reasoning for Agents' Priv
% 0.56/1.00 % Source : [Bar03]
% 0.56/1.00 % Names :
% 0.56/1.00
% 0.56/1.00 % Status : Theorem
% 0.56/1.00 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.10 .0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.25 v6.2.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.26 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.25 .0, 0.24 v5.0.0, 0.25 .0, 0.17 v4.0.1, 0.13 v4.0.0, 0.08 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.21 v3.2.0, 0.36 .0
% 0.56/1.00 % Syntax : Number of formulae : 923 ( 891 unt; 0 def)
% 0.56/1.00 % Number of atoms : 1023 ( 2 equ)
% 0.56/1.00 % Maximal formula atoms : 6 ( 1 avg)
% 0.56/1.00 % Number of connectives : 148 ( 48 ~; 1 |; 67 &)
% 0.56/1.00 % ( 16 <=>; 16 =>; 0 <=; 0 <~>)
% 0.56/1.00 % Maximal formula depth : 8 ( 1 avg)
% 0.56/1.00 % Maximal term depth : 5 ( 2 avg)
% 0.56/1.00 % Number of predicates : 17 ( 16 usr; 0 prp; 1-4 aty)
% 0.56/1.00 % Number of functors : 290 ( 290 usr; 286 con; 0-2 aty)
% 0.56/1.00 % Number of variables : 70 ( 70 !; 0 ?)
% 0.56/1.00 % SPC : FOF_THM_RFO_SEQ
% 0.56/1.00
% 0.56/1.00 % Comments :
% 0.56/1.00 % Bugfixes : v3.0.0 - Bugfixes in NUM005+1.ax
% 0.56/1.00 % : v3.1.0 - Changes to NUM005 axioms
% 0.56/1.00 %--------------------------------------------------------------------------
% 0.56/1.00 %----Include axioms of CPlanT
% 0.56/1.00 include('Axioms/AGT001+0.ax').
% 0.56/1.00 %----Include events of CPlanT
% 0.56/1.00 include('Axioms/AGT001+1.ax').
% 0.56/1.00 %----Include lemmas of CPlanT
% 0.56/1.00 include('Axioms/AGT001+2.ax').
% 0.56/1.00 %----Include axioms for RDN and RDN less
% 0.56/1.00 include('Axioms/NUM005+0.ax').
% 0.56/1.00 include('Axioms/NUM005+1.ax').
% 0.56/1.00 %--------------------------------------------------------------------------
% 0.56/1.00 fof(query_3,conjecture,
% 0.56/1.00 accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n5) ).
% 0.56/1.00
% 0.56/1.00 %--------------------------------------------------------------------------
% 0.56/1.00 %-------------------------------------------
% 0.56/1.00 % Proof found
% 0.56/1.00 % SZS status Theorem for theBenchmark
% 0.56/1.00 % SZS output start Proof
% 0.56/1.00 %ClaNum:1041(EqnAxiom:45)
% 0.56/1.00 %VarNum:360(SingletonVarNum:158)
% 0.56/1.00 %MaxLitNum:6
% 0.56/1.00 %MaxfuncDepth:4
% 0.56/1.00 %SharedTerms:1446
% 0.56/1.00 %goalClause: 934
% 0.56/1.00 %singleGoalClaCount:1
% 0.56/1.00 [55]P2(a5,a6)
% 0.56/1.00 [56]P2(a5,a283)
% 0.56/1.00 [57]P2(a5,a7)
% 0.56/1.00 [58]P2(a15,a6)
% 0.56/1.00 [59]P2(a15,a283)
% 0.56/1.00 [60]P2(a15,a7)
% 0.56/1.00 [61]P2(a15,a289)
% 0.56/1.00 [62]P2(a16,a6)
% 0.56/1.00 [63]P2(a16,a283)
% 0.56/1.00 [64]P2(a16,a7)
% 0.56/1.00 [65]P2(a16,a289)
% 0.56/1.00 [66]P2(a8,a283)
% 0.56/1.00 [67]P2(a8,a7)
% 0.56/1.00 [68]P2(a8,a289)
% 0.56/1.00 [69]P2(a17,a283)
% 0.56/1.00 [70]P2(a17,a7)
% 0.56/1.00 [71]P2(a17,a289)
% 0.56/1.00 [72]P2(a18,a6)
% 0.56/1.00 [73]P2(a18,a283)
% 0.56/1.00 [74]P2(a18,a289)
% 0.56/1.00 [75]P2(a21,a6)
% 0.56/1.00 [76]P2(a21,a7)
% 0.56/1.00 [77]P2(a21,a289)
% 0.56/1.00 [78]P2(a22,a6)
% 0.56/1.00 [79]P2(a22,a283)
% 0.56/1.00 [80]P2(a22,a7)
% 0.56/1.00 [81]P2(a22,a289)
% 0.56/1.00 [82]P2(a19,a283)
% 0.56/1.00 [83]P2(a19,a7)
% 0.56/1.00 [84]P2(a19,a289)
% 0.56/1.00 [85]P2(a20,a6)
% 0.56/1.00 [86]P2(a20,a283)
% 0.56/1.00 [87]P2(a20,a7)
% 0.56/1.00 [88]P2(a20,a289)
% 0.56/1.00 [89]P2(a13,a6)
% 0.56/1.00 [90]P2(a13,a283)
% 0.56/1.00 [91]P2(a13,a7)
% 0.56/1.00 [92]P2(a13,a289)
% 0.56/1.00 [93]P2(a284,a6)
% 0.56/1.00 [94]P2(a284,a283)
% 0.56/1.00 [95]P2(a284,a7)
% 0.56/1.00 [96]P2(a284,a289)
% 0.56/1.00 [97]P3(a5,a15)
% 0.56/1.00 [98]P3(a5,a16)
% 0.56/1.00 [99]P3(a5,a8)
% 0.56/1.00 [100]P3(a5,a18)
% 0.56/1.00 [101]P3(a5,a19)
% 0.56/1.00 [102]P3(a5,a284)
% 0.56/1.00 [103]P3(a15,a5)
% 0.56/1.00 [104]P3(a15,a16)
% 0.56/1.00 [105]P3(a15,a8)
% 0.56/1.00 [106]P3(a15,a18)
% 0.56/1.00 [107]P3(a15,a19)
% 0.56/1.00 [108]P3(a15,a284)
% 0.56/1.00 [109]P3(a16,a5)
% 0.56/1.00 [110]P3(a16,a15)
% 0.56/1.00 [111]P3(a16,a8)
% 0.56/1.00 [112]P3(a16,a18)
% 0.56/1.00 [113]P3(a16,a19)
% 0.56/1.00 [114]P3(a16,a284)
% 0.56/1.00 [115]P3(a8,a5)
% 0.56/1.00 [116]P3(a8,a15)
% 0.56/1.01 [117]P3(a8,a17)
% 0.56/1.01 [118]P3(a8,a18)
% 0.56/1.01 [119]P3(a8,a21)
% 0.56/1.01 [120]P3(a8,a22)
% 0.56/1.01 [121]P3(a8,a20)
% 0.56/1.01 [122]P3(a8,a284)
% 0.56/1.01 [123]P3(a17,a5)
% 0.56/1.01 [124]P3(a17,a15)
% 0.56/1.01 [125]P3(a17,a18)
% 0.56/1.01 [126]P3(a17,a284)
% 0.56/1.01 [127]P3(a18,a5)
% 0.56/1.01 [128]P3(a18,a15)
% 0.56/1.01 [129]P3(a18,a8)
% 0.56/1.01 [130]P3(a18,a17)
% 0.56/1.01 [131]P3(a18,a21)
% 0.56/1.01 [132]P3(a18,a22)
% 0.56/1.01 [133]P3(a18,a20)
% 0.56/1.01 [134]P3(a18,a284)
% 0.56/1.01 [135]P3(a21,a5)
% 0.56/1.01 [136]P3(a21,a15)
% 0.56/1.01 [137]P3(a21,a8)
% 0.56/1.01 [138]P3(a21,a17)
% 0.56/1.01 [139]P3(a21,a18)
% 0.56/1.01 [140]P3(a21,a22)
% 0.56/1.01 [141]P3(a21,a20)
% 0.56/1.01 [142]P3(a21,a284)
% 0.56/1.01 [143]P3(a22,a5)
% 0.56/1.01 [144]P3(a22,a15)
% 0.56/1.01 [145]P3(a22,a8)
% 0.56/1.01 [146]P3(a22,a17)
% 0.56/1.01 [147]P3(a22,a18)
% 0.56/1.01 [148]P3(a22,a21)
% 0.56/1.01 [149]P3(a22,a20)
% 0.56/1.01 [150]P3(a22,a284)
% 0.56/1.01 [151]P3(a19,a5)
% 0.56/1.01 [152]P3(a19,a15)
% 0.56/1.01 [153]P3(a19,a8)
% 0.56/1.01 [154]P3(a19,a18)
% 0.56/1.01 [155]P3(a19,a284)
% 0.56/1.01 [156]P3(a20,a5)
% 0.56/1.01 [157]P3(a20,a15)
% 0.56/1.01 [158]P3(a20,a8)
% 0.56/1.01 [159]P3(a20,a17)
% 0.56/1.01 [160]P3(a20,a18)
% 0.56/1.01 [161]P3(a20,a21)
% 0.56/1.01 [162]P3(a20,a22)
% 0.56/1.01 [163]P3(a20,a284)
% 0.56/1.01 [164]P3(a13,a5)
% 0.56/1.01 [165]P3(a13,a15)
% 0.56/1.01 [166]P3(a13,a16)
% 0.56/1.01 [167]P3(a13,a8)
% 0.56/1.01 [168]P3(a13,a18)
% 0.56/1.01 [169]P3(a13,a19)
% 0.56/1.01 [170]P3(a284,a5)
% 0.56/1.01 [171]P3(a284,a15)
% 0.56/1.01 [172]P3(a284,a16)
% 0.56/1.01 [173]P3(a284,a8)
% 0.56/1.01 [174]P3(a284,a18)
% 0.56/1.01 [175]P3(a284,a19)
% 0.56/1.01 [176]P4(a5,a2)
% 0.56/1.01 [177]P4(a5,a3)
% 0.56/1.01 [178]P4(a5,a4)
% 0.56/1.01 [180]P4(a5,a25)
% 0.56/1.01 [182]P4(a5,a84)
% 0.56/1.01 [184]P4(a5,a95)
% 0.56/1.01 [185]P4(a15,a2)
% 0.56/1.01 [186]P4(a15,a3)
% 0.56/1.01 [187]P4(a15,a4)
% 0.56/1.01 [189]P4(a15,a25)
% 0.56/1.01 [190]P4(a15,a84)
% 0.56/1.01 [192]P4(a15,a95)
% 0.56/1.01 [193]P4(a16,a2)
% 0.56/1.01 [194]P4(a16,a3)
% 0.56/1.01 [195]P4(a16,a4)
% 0.56/1.01 [197]P4(a16,a25)
% 0.56/1.01 [198]P4(a16,a84)
% 0.56/1.01 [200]P4(a16,a95)
% 0.56/1.01 [201]P4(a8,a2)
% 0.56/1.01 [203]P4(a8,a3)
% 0.56/1.01 [204]P4(a8,a4)
% 0.56/1.01 [206]P4(a8,a25)
% 0.56/1.01 [208]P4(a8,a84)
% 0.56/1.01 [210]P4(a8,a95)
% 0.56/1.01 [212]P4(a17,a2)
% 0.56/1.01 [214]P4(a17,a3)
% 0.56/1.01 [215]P4(a17,a4)
% 0.56/1.01 [217]P4(a17,a25)
% 0.56/1.01 [219]P4(a18,a2)
% 0.56/1.01 [220]P4(a18,a3)
% 0.56/1.01 [222]P4(a18,a4)
% 0.56/1.01 [224]P4(a18,a25)
% 0.56/1.01 [226]P4(a18,a84)
% 0.56/1.01 [228]P4(a18,a95)
% 0.56/1.01 [229]P4(a21,a2)
% 0.56/1.01 [231]P4(a21,a3)
% 0.56/1.01 [232]P4(a21,a4)
% 0.56/1.01 [234]P4(a21,a25)
% 0.56/1.01 [235]P4(a21,a84)
% 0.56/1.01 [237]P4(a21,a95)
% 0.56/1.01 [239]P4(a22,a2)
% 0.56/1.01 [241]P4(a22,a3)
% 0.56/1.01 [242]P4(a22,a4)
% 0.56/1.01 [244]P4(a22,a25)
% 0.56/1.01 [246]P4(a22,a84)
% 0.56/1.01 [248]P4(a22,a95)
% 0.56/1.01 [249]P4(a19,a2)
% 0.56/1.01 [250]P4(a19,a3)
% 0.56/1.01 [251]P4(a19,a4)
% 0.56/1.01 [252]P4(a19,a25)
% 0.56/1.01 [253]P4(a19,a84)
% 0.56/1.01 [255]P4(a19,a95)
% 0.56/1.01 [256]P4(a20,a2)
% 0.56/1.01 [258]P4(a20,a3)
% 0.56/1.01 [259]P4(a20,a4)
% 0.56/1.01 [261]P4(a20,a25)
% 0.56/1.01 [263]P4(a20,a84)
% 0.56/1.01 [265]P4(a20,a95)
% 0.56/1.01 [266]P4(a13,a2)
% 0.56/1.01 [267]P4(a13,a3)
% 0.56/1.01 [268]P4(a13,a4)
% 0.56/1.01 [270]P4(a13,a25)
% 0.56/1.01 [271]P4(a13,a84)
% 0.56/1.01 [273]P4(a13,a95)
% 0.56/1.01 [274]P4(a284,a2)
% 0.56/1.01 [275]P4(a284,a3)
% 0.56/1.01 [276]P4(a284,a4)
% 0.56/1.01 [278]P4(a284,a25)
% 0.56/1.01 [280]P4(a284,a84)
% 0.56/1.01 [282]P4(a284,a95)
% 0.56/1.01 [311]P5(a5,a9,a26)
% 0.56/1.01 [312]P5(a5,a9,a119)
% 0.56/1.01 [313]P5(a5,a9,a125)
% 0.56/1.01 [314]P5(a5,a10,a64)
% 0.56/1.01 [315]P5(a5,a10,a3)
% 0.56/1.01 [316]P5(a5,a10,a65)
% 0.56/1.01 [317]P5(a5,a23,a4)
% 0.56/1.01 [318]P5(a5,a23,a24)
% 0.56/1.01 [319]P5(a5,a141,a24)
% 0.56/1.01 [320]P5(a5,a141,a129)
% 0.56/1.01 [321]P5(a5,a270,a4)
% 0.56/1.01 [322]P5(a5,a270,a24)
% 0.56/1.01 [323]P5(a15,a9,a74)
% 0.56/1.01 [324]P5(a15,a9,a26)
% 0.56/1.01 [325]P5(a15,a9,a119)
% 0.56/1.01 [326]P5(a15,a9,a125)
% 0.56/1.01 [327]P5(a15,a10,a64)
% 0.56/1.01 [328]P5(a15,a10,a3)
% 0.56/1.01 [329]P5(a15,a10,a24)
% 0.56/1.01 [330]P5(a15,a10,a65)
% 0.56/1.01 [331]P5(a15,a23,a106)
% 0.56/1.01 [332]P5(a15,a23,a4)
% 0.56/1.01 [333]P5(a15,a23,a24)
% 0.56/1.01 [334]P5(a15,a141,a24)
% 0.56/1.01 [335]P5(a15,a141,a129)
% 0.56/1.01 [336]P5(a15,a270,a4)
% 0.56/1.01 [337]P5(a15,a270,a24)
% 0.56/1.01 [338]P5(a15,a270,a84)
% 0.56/1.01 [339]P5(a16,a9,a74)
% 0.56/1.01 [340]P5(a16,a9,a26)
% 0.56/1.01 [341]P5(a16,a9,a119)
% 0.56/1.01 [342]P5(a16,a9,a125)
% 0.56/1.01 [343]P5(a16,a10,a64)
% 0.56/1.01 [344]P5(a16,a10,a3)
% 0.56/1.01 [345]P5(a16,a10,a24)
% 0.56/1.01 [346]P5(a16,a10,a65)
% 0.56/1.01 [347]P5(a16,a23,a106)
% 0.56/1.01 [348]P5(a16,a23,a4)
% 0.56/1.01 [349]P5(a16,a23,a24)
% 0.56/1.01 [350]P5(a16,a141,a24)
% 0.56/1.01 [351]P5(a16,a141,a129)
% 0.56/1.01 [352]P5(a16,a270,a4)
% 0.56/1.01 [353]P5(a16,a270,a24)
% 0.56/1.01 [354]P5(a16,a270,a84)
% 0.56/1.01 [355]P5(a8,a9,a74)
% 0.56/1.01 [356]P5(a8,a9,a119)
% 0.56/1.01 [357]P5(a8,a9,a125)
% 0.56/1.01 [358]P5(a8,a10,a64)
% 0.56/1.01 [359]P5(a8,a10,a24)
% 0.56/1.01 [360]P5(a8,a10,a65)
% 0.56/1.01 [361]P5(a8,a23,a106)
% 0.56/1.01 [362]P5(a8,a23,a4)
% 0.56/1.01 [363]P5(a8,a141,a24)
% 0.56/1.01 [364]P5(a8,a270,a4)
% 0.56/1.01 [365]P5(a8,a270,a24)
% 0.56/1.01 [366]P5(a8,a270,a84)
% 0.56/1.01 [367]P5(a17,a9,a74)
% 0.56/1.01 [368]P5(a17,a9,a119)
% 0.56/1.01 [369]P5(a17,a9,a125)
% 0.56/1.01 [370]P5(a17,a10,a64)
% 0.56/1.01 [371]P5(a17,a10,a24)
% 0.56/1.01 [372]P5(a17,a10,a65)
% 0.56/1.01 [373]P5(a17,a23,a106)
% 0.56/1.01 [374]P5(a17,a23,a4)
% 0.56/1.01 [375]P5(a17,a141,a24)
% 0.56/1.01 [376]P5(a17,a270,a4)
% 0.56/1.01 [377]P5(a17,a270,a24)
% 0.56/1.01 [378]P5(a17,a270,a84)
% 0.56/1.01 [379]P5(a18,a9,a74)
% 0.56/1.01 [380]P5(a18,a9,a26)
% 0.56/1.01 [381]P5(a18,a9,a119)
% 0.56/1.01 [382]P5(a18,a10,a3)
% 0.56/1.01 [383]P5(a18,a10,a24)
% 0.56/1.01 [384]P5(a18,a10,a65)
% 0.56/1.01 [385]P5(a18,a23,a106)
% 0.56/1.01 [386]P5(a18,a23,a4)
% 0.56/1.01 [387]P5(a18,a23,a24)
% 0.56/1.01 [388]P5(a18,a141,a24)
% 0.56/1.01 [389]P5(a18,a141,a129)
% 0.56/1.01 [390]P5(a18,a270,a24)
% 0.56/1.01 [391]P5(a18,a270,a84)
% 0.56/1.01 [392]P5(a21,a9,a74)
% 0.56/1.01 [393]P5(a21,a9,a26)
% 0.56/1.01 [394]P5(a21,a9,a125)
% 0.56/1.01 [395]P5(a21,a10,a64)
% 0.56/1.01 [396]P5(a21,a10,a3)
% 0.56/1.01 [397]P5(a21,a10,a24)
% 0.56/1.01 [398]P5(a21,a23,a106)
% 0.56/1.01 [399]P5(a21,a23,a4)
% 0.56/1.01 [400]P5(a21,a23,a24)
% 0.56/1.01 [401]P5(a21,a141,a24)
% 0.56/1.01 [402]P5(a21,a141,a129)
% 0.56/1.01 [403]P5(a21,a270,a4)
% 0.56/1.01 [404]P5(a21,a270,a24)
% 0.56/1.01 [405]P5(a21,a270,a84)
% 0.56/1.01 [406]P5(a22,a9,a74)
% 0.56/1.01 [407]P5(a22,a9,a26)
% 0.56/1.01 [408]P5(a22,a9,a119)
% 0.56/1.01 [409]P5(a22,a9,a125)
% 0.56/1.01 [410]P5(a22,a10,a64)
% 0.56/1.01 [411]P5(a22,a10,a3)
% 0.56/1.01 [412]P5(a22,a10,a24)
% 0.56/1.01 [413]P5(a22,a10,a65)
% 0.56/1.01 [414]P5(a22,a23,a106)
% 0.56/1.01 [415]P5(a22,a23,a4)
% 0.56/1.01 [416]P5(a22,a23,a24)
% 0.56/1.01 [417]P5(a22,a141,a24)
% 0.56/1.01 [418]P5(a22,a141,a129)
% 0.56/1.01 [419]P5(a22,a270,a4)
% 0.56/1.01 [420]P5(a22,a270,a24)
% 0.56/1.01 [421]P5(a22,a270,a84)
% 0.56/1.01 [422]P5(a19,a9,a74)
% 0.56/1.01 [423]P5(a19,a9,a119)
% 0.56/1.01 [424]P5(a19,a9,a125)
% 0.56/1.01 [425]P5(a19,a10,a64)
% 0.56/1.01 [426]P5(a19,a10,a24)
% 0.56/1.01 [427]P5(a19,a10,a65)
% 0.56/1.01 [428]P5(a19,a23,a106)
% 0.56/1.01 [429]P5(a19,a23,a4)
% 0.56/1.01 [430]P5(a19,a141,a24)
% 0.56/1.01 [431]P5(a19,a270,a4)
% 0.56/1.01 [432]P5(a19,a270,a24)
% 0.56/1.01 [433]P5(a19,a270,a84)
% 0.56/1.01 [434]P5(a20,a9,a74)
% 0.56/1.01 [435]P5(a20,a9,a26)
% 0.56/1.01 [436]P5(a20,a9,a119)
% 0.56/1.01 [437]P5(a20,a9,a125)
% 0.56/1.01 [438]P5(a20,a10,a64)
% 0.56/1.01 [439]P5(a20,a10,a3)
% 0.56/1.01 [440]P5(a20,a10,a24)
% 0.56/1.01 [441]P5(a20,a10,a65)
% 0.56/1.01 [442]P5(a20,a23,a106)
% 0.56/1.01 [443]P5(a20,a23,a4)
% 0.56/1.01 [444]P5(a20,a23,a24)
% 0.56/1.01 [445]P5(a20,a141,a24)
% 0.56/1.01 [446]P5(a20,a141,a129)
% 0.56/1.01 [447]P5(a20,a270,a4)
% 0.56/1.01 [448]P5(a20,a270,a24)
% 0.56/1.01 [449]P5(a20,a270,a84)
% 0.56/1.01 [450]P5(a13,a9,a74)
% 0.56/1.01 [451]P5(a13,a9,a26)
% 0.56/1.01 [452]P5(a13,a9,a119)
% 0.56/1.01 [453]P5(a13,a9,a125)
% 0.56/1.01 [454]P5(a13,a10,a64)
% 0.56/1.01 [455]P5(a13,a10,a3)
% 0.56/1.01 [456]P5(a13,a10,a24)
% 0.56/1.01 [457]P5(a13,a10,a65)
% 0.56/1.01 [458]P5(a13,a23,a106)
% 0.56/1.01 [459]P5(a13,a23,a4)
% 0.56/1.01 [460]P5(a13,a23,a24)
% 0.56/1.01 [461]P5(a13,a141,a24)
% 0.56/1.01 [462]P5(a13,a141,a129)
% 0.56/1.01 [463]P5(a13,a270,a4)
% 0.56/1.01 [464]P5(a13,a270,a24)
% 0.56/1.01 [465]P5(a13,a270,a84)
% 0.56/1.01 [466]P5(a284,a9,a74)
% 0.56/1.01 [467]P5(a284,a9,a26)
% 0.56/1.01 [468]P5(a284,a9,a119)
% 0.56/1.01 [469]P5(a284,a9,a125)
% 0.56/1.01 [470]P5(a284,a10,a64)
% 0.56/1.01 [471]P5(a284,a10,a3)
% 0.56/1.01 [472]P5(a284,a10,a24)
% 0.56/1.01 [473]P5(a284,a10,a65)
% 0.56/1.01 [474]P5(a284,a23,a106)
% 0.56/1.01 [475]P5(a284,a23,a4)
% 0.56/1.01 [476]P5(a284,a23,a24)
% 0.56/1.01 [477]P5(a284,a141,a24)
% 0.56/1.01 [478]P5(a284,a141,a129)
% 0.56/1.01 [479]P5(a284,a270,a4)
% 0.56/1.01 [480]P5(a284,a270,a24)
% 0.56/1.01 [481]P5(a284,a270,a84)
% 0.56/1.01 [482]P14(a5,a8,a6)
% 0.56/1.01 [483]P14(a5,a18,a7)
% 0.56/1.01 [484]P14(a15,a8,a6)
% 0.56/1.01 [485]P14(a15,a18,a7)
% 0.56/1.01 [486]P14(a16,a8,a6)
% 0.56/1.01 [487]P14(a16,a18,a7)
% 0.56/1.01 [488]P14(a8,a5,a289)
% 0.56/1.01 [489]P14(a8,a15,a283)
% 0.56/1.01 [490]P14(a8,a284,a283)
% 0.56/1.01 [491]P14(a17,a5,a289)
% 0.56/1.01 [492]P14(a17,a15,a283)
% 0.56/1.01 [493]P14(a17,a284,a283)
% 0.56/1.01 [494]P14(a18,a5,a289)
% 0.56/1.01 [495]P14(a18,a15,a283)
% 0.56/1.01 [496]P14(a18,a284,a283)
% 0.56/1.01 [497]P14(a21,a5,a289)
% 0.56/1.01 [498]P14(a22,a5,a289)
% 0.56/1.01 [499]P14(a22,a15,a283)
% 0.56/1.01 [500]P14(a22,a284,a283)
% 0.56/1.01 [501]P14(a19,a18,a7)
% 0.56/1.01 [502]P14(a20,a5,a289)
% 0.56/1.02 [503]P14(a20,a15,a283)
% 0.56/1.02 [504]P14(a20,a284,a283)
% 0.56/1.02 [505]P14(a13,a8,a6)
% 0.56/1.02 [506]P14(a13,a18,a7)
% 0.56/1.02 [507]P14(a284,a8,a6)
% 0.56/1.02 [508]P14(a284,a18,a7)
% 0.56/1.02 [509]P6(a5,a8,a6)
% 0.56/1.02 [510]P6(a5,a18,a7)
% 0.56/1.02 [511]P6(a15,a8,a6)
% 0.56/1.02 [512]P6(a15,a18,a7)
% 0.56/1.02 [513]P6(a16,a8,a6)
% 0.56/1.02 [514]P6(a16,a18,a7)
% 0.56/1.02 [515]P6(a8,a5,a289)
% 0.56/1.02 [516]P6(a8,a15,a283)
% 0.56/1.02 [517]P6(a8,a284,a283)
% 0.56/1.02 [518]P6(a17,a5,a289)
% 0.56/1.02 [519]P6(a17,a15,a283)
% 0.56/1.02 [520]P6(a17,a284,a283)
% 0.56/1.02 [521]P6(a18,a5,a289)
% 0.56/1.02 [522]P6(a18,a15,a283)
% 0.56/1.02 [523]P6(a18,a284,a283)
% 0.56/1.02 [524]P6(a21,a5,a289)
% 0.56/1.02 [525]P6(a21,a15,a283)
% 0.56/1.02 [526]P6(a21,a284,a283)
% 0.56/1.02 [527]P6(a22,a5,a289)
% 0.56/1.02 [528]P6(a22,a15,a283)
% 0.56/1.02 [529]P6(a22,a284,a283)
% 0.56/1.02 [530]P6(a19,a8,a6)
% 0.56/1.02 [531]P6(a19,a18,a7)
% 0.56/1.02 [532]P6(a20,a5,a289)
% 0.56/1.02 [533]P6(a20,a15,a283)
% 0.56/1.02 [534]P6(a20,a284,a283)
% 0.56/1.02 [535]P6(a13,a8,a6)
% 0.56/1.02 [536]P6(a13,a18,a7)
% 0.56/1.02 [537]P6(a284,a8,a6)
% 0.56/1.02 [538]P6(a284,a18,a7)
% 0.56/1.02 [539]P16(a21,a15,a283)
% 0.56/1.02 [540]P16(a21,a284,a283)
% 0.56/1.02 [541]P16(a19,a8,a6)
% 0.56/1.02 [779]P7(a5,a15,a6,a95)
% 0.56/1.02 [780]P7(a5,a15,a283,a95)
% 0.56/1.02 [781]P7(a5,a15,a7,a95)
% 0.56/1.02 [782]P7(a5,a16,a6,a95)
% 0.56/1.02 [783]P7(a5,a284,a283,a84)
% 0.56/1.02 [784]P7(a5,a284,a283,a95)
% 0.56/1.02 [785]P7(a15,a5,a6,a84)
% 0.56/1.02 [786]P7(a15,a5,a6,a95)
% 0.56/1.02 [787]P7(a15,a5,a7,a95)
% 0.56/1.02 [788]P7(a15,a5,a289,a95)
% 0.56/1.02 [789]P7(a15,a16,a6,a95)
% 0.56/1.02 [790]P7(a15,a284,a283,a84)
% 0.56/1.02 [791]P7(a15,a284,a283,a95)
% 0.56/1.02 [792]P7(a16,a5,a6,a84)
% 0.56/1.02 [793]P7(a16,a5,a6,a95)
% 0.56/1.02 [794]P7(a16,a5,a7,a95)
% 0.56/1.02 [795]P7(a16,a5,a289,a95)
% 0.56/1.02 [796]P7(a16,a15,a6,a95)
% 0.56/1.02 [797]P7(a16,a15,a283,a95)
% 0.56/1.02 [798]P7(a16,a15,a7,a95)
% 0.56/1.02 [799]P7(a16,a284,a283,a84)
% 0.56/1.02 [800]P7(a16,a284,a283,a95)
% 0.56/1.02 [801]P7(a8,a17,a283,a2)
% 0.56/1.02 [802]P7(a8,a17,a289,a2)
% 0.56/1.02 [803]P7(a8,a18,a283,a95)
% 0.56/1.02 [804]P7(a8,a18,a7,a2)
% 0.56/1.02 [805]P7(a8,a18,a7,a84)
% 0.56/1.02 [806]P7(a8,a18,a7,a95)
% 0.56/1.02 [807]P7(a8,a18,a289,a95)
% 0.56/1.02 [808]P7(a8,a21,a289,a95)
% 0.56/1.02 [809]P7(a8,a22,a283,a2)
% 0.56/1.02 [810]P7(a8,a22,a283,a84)
% 0.56/1.02 [811]P7(a8,a22,a283,a95)
% 0.56/1.02 [812]P7(a8,a22,a289,a95)
% 0.56/1.02 [813]P7(a8,a20,a283,a95)
% 0.56/1.02 [814]P7(a8,a20,a289,a95)
% 0.56/1.02 [815]P7(a17,a18,a7,a25)
% 0.56/1.02 [816]P7(a17,a22,a283,a2)
% 0.56/1.02 [817]P7(a18,a8,a6,a84)
% 0.56/1.02 [818]P7(a18,a8,a6,a95)
% 0.56/1.02 [819]P7(a18,a8,a283,a3)
% 0.56/1.02 [820]P7(a18,a8,a283,a95)
% 0.56/1.02 [821]P7(a18,a8,a289,a95)
% 0.56/1.02 [822]P7(a18,a17,a283,a3)
% 0.56/1.02 [823]P7(a18,a21,a289,a95)
% 0.56/1.02 [824]P7(a18,a22,a283,a3)
% 0.56/1.02 [825]P7(a18,a22,a283,a95)
% 0.56/1.02 [826]P7(a18,a22,a289,a95)
% 0.56/1.02 [827]P7(a18,a20,a283,a3)
% 0.56/1.02 [828]P7(a18,a20,a283,a95)
% 0.56/1.02 [829]P7(a18,a20,a289,a25)
% 0.56/1.02 [830]P7(a18,a20,a289,a95)
% 0.56/1.02 [831]P7(a21,a8,a6,a84)
% 0.56/1.02 [832]P7(a21,a8,a6,a95)
% 0.56/1.02 [833]P7(a21,a8,a289,a95)
% 0.56/1.02 [834]P7(a21,a17,a289,a2)
% 0.56/1.02 [835]P7(a21,a18,a7,a2)
% 0.56/1.02 [836]P7(a21,a18,a7,a84)
% 0.56/1.02 [837]P7(a21,a18,a7,a95)
% 0.56/1.02 [838]P7(a21,a18,a289,a95)
% 0.56/1.02 [839]P7(a21,a22,a289,a95)
% 0.56/1.02 [840]P7(a21,a20,a289,a95)
% 0.56/1.02 [841]P7(a22,a8,a6,a84)
% 0.56/1.02 [842]P7(a22,a8,a6,a95)
% 0.56/1.02 [843]P7(a22,a8,a283,a95)
% 0.56/1.02 [844]P7(a22,a8,a289,a95)
% 0.56/1.02 [845]P7(a22,a17,a283,a2)
% 0.56/1.02 [846]P7(a22,a17,a289,a2)
% 0.56/1.02 [847]P7(a22,a18,a283,a95)
% 0.56/1.02 [848]P7(a22,a18,a7,a84)
% 0.56/1.02 [849]P7(a22,a18,a7,a95)
% 0.56/1.02 [850]P7(a22,a18,a289,a95)
% 0.56/1.02 [851]P7(a22,a21,a289,a95)
% 0.56/1.02 [852]P7(a22,a20,a283,a95)
% 0.56/1.02 [853]P7(a22,a20,a289,a95)
% 0.56/1.02 [854]P7(a19,a5,a7,a95)
% 0.56/1.02 [855]P7(a19,a5,a289,a95)
% 0.56/1.02 [856]P7(a19,a15,a283,a95)
% 0.56/1.02 [857]P7(a19,a15,a7,a95)
% 0.56/1.02 [858]P7(a19,a284,a283,a84)
% 0.56/1.02 [859]P7(a19,a284,a283,a95)
% 0.56/1.02 [860]P7(a20,a8,a6,a84)
% 0.56/1.02 [861]P7(a20,a8,a6,a95)
% 0.56/1.02 [862]P7(a20,a8,a283,a95)
% 0.56/1.02 [863]P7(a20,a8,a289,a95)
% 0.56/1.02 [864]P7(a20,a17,a283,a2)
% 0.56/1.02 [865]P7(a20,a18,a283,a95)
% 0.56/1.02 [866]P7(a20,a18,a7,a2)
% 0.56/1.02 [867]P7(a20,a18,a7,a84)
% 0.56/1.02 [868]P7(a20,a18,a7,a95)
% 0.56/1.02 [869]P7(a20,a18,a289,a95)
% 0.56/1.02 [870]P7(a20,a21,a289,a95)
% 0.56/1.02 [871]P7(a20,a22,a283,a2)
% 0.56/1.02 [872]P7(a20,a22,a283,a84)
% 0.56/1.02 [873]P7(a20,a22,a283,a95)
% 0.56/1.02 [874]P7(a20,a22,a289,a95)
% 0.56/1.02 [875]P7(a13,a5,a6,a84)
% 0.56/1.02 [876]P7(a13,a5,a6,a95)
% 0.56/1.02 [877]P7(a13,a5,a7,a95)
% 0.56/1.02 [878]P7(a13,a5,a289,a95)
% 0.56/1.02 [879]P7(a13,a15,a6,a95)
% 0.56/1.02 [880]P7(a13,a15,a283,a95)
% 0.56/1.02 [881]P7(a13,a15,a7,a95)
% 0.56/1.02 [882]P7(a13,a16,a6,a95)
% 0.56/1.02 [883]P7(a284,a5,a6,a84)
% 0.56/1.02 [884]P7(a284,a5,a6,a95)
% 0.56/1.02 [885]P7(a284,a5,a7,a95)
% 0.56/1.02 [886]P7(a284,a5,a289,a95)
% 0.56/1.02 [887]P7(a284,a15,a6,a95)
% 0.56/1.02 [888]P7(a284,a15,a283,a95)
% 0.56/1.02 [889]P7(a284,a15,a7,a95)
% 0.56/1.02 [890]P7(a284,a16,a6,a95)
% 0.56/1.02 [891]~P2(a21,a283)
% 0.56/1.02 [892]~P2(a19,a6)
% 0.56/1.02 [893]~P3(a13,a284)
% 0.56/1.02 [894]~P4(a17,a84)
% 0.56/1.02 [895]~P4(a17,a95)
% 0.56/1.02 [896]~P7(a17,a8,a6,a84)
% 0.56/1.02 [897]~P7(a17,a8,a6,a95)
% 0.56/1.02 [898]~P7(a17,a8,a283,a95)
% 0.56/1.02 [899]~P7(a17,a8,a289,a95)
% 0.56/1.02 [900]~P7(a17,a18,a283,a95)
% 0.56/1.02 [901]~P7(a17,a18,a7,a84)
% 0.56/1.02 [902]~P7(a17,a18,a7,a95)
% 0.56/1.02 [903]~P7(a17,a18,a289,a95)
% 0.56/1.02 [904]~P7(a17,a21,a289,a95)
% 0.56/1.02 [905]~P7(a17,a22,a283,a84)
% 0.56/1.02 [906]~P7(a17,a22,a283,a95)
% 0.56/1.02 [907]~P7(a17,a22,a289,a95)
% 0.56/1.02 [908]~P7(a17,a20,a283,a95)
% 0.56/1.02 [909]~P7(a17,a20,a289,a95)
% 0.56/1.02 [910]~P7(a21,a8,a283,a3)
% 0.56/1.02 [911]~P7(a21,a8,a283,a25)
% 0.56/1.02 [912]~P7(a21,a8,a283,a95)
% 0.56/1.02 [913]~P7(a21,a17,a283,a2)
% 0.56/1.02 [914]~P7(a21,a17,a283,a3)
% 0.56/1.02 [915]~P7(a21,a17,a283,a25)
% 0.56/1.02 [916]~P7(a21,a18,a283,a25)
% 0.56/1.02 [917]~P7(a21,a18,a283,a95)
% 0.56/1.02 [918]~P7(a21,a22,a283,a2)
% 0.56/1.02 [919]~P7(a21,a22,a283,a3)
% 0.56/1.02 [920]~P7(a21,a22,a283,a25)
% 0.56/1.02 [921]~P7(a21,a22,a283,a84)
% 0.56/1.02 [922]~P7(a21,a22,a283,a95)
% 0.56/1.02 [923]~P7(a21,a20,a283,a3)
% 0.56/1.02 [924]~P7(a21,a20,a283,a25)
% 0.56/1.02 [925]~P7(a21,a20,a283,a95)
% 0.56/1.02 [926]~P7(a19,a5,a6,a25)
% 0.56/1.02 [927]~P7(a19,a5,a6,a95)
% 0.56/1.02 [928]~P7(a19,a15,a6,a25)
% 0.56/1.02 [929]~P7(a19,a15,a6,a95)
% 0.56/1.02 [930]~P7(a19,a16,a6,a25)
% 0.56/1.02 [931]~P7(a19,a16,a6,a95)
% 0.56/1.02 [932]~P7(a19,a13,a6,a25)
% 0.56/1.02 [933]~P7(a19,a284,a6,a25)
% 0.56/1.02 [934]~P7(a13,a16,a283,a84)
% 0.56/1.02 [935]~P7(a13,a284,a283,a25)
% 0.56/1.02 [936]~P7(a13,a284,a283,a95)
% 0.56/1.02 [46]P1(f116(a1))
% 0.56/1.02 [47]P1(f116(a2))
% 0.56/1.02 [48]P1(f116(a3))
% 0.56/1.02 [49]P1(f116(a4))
% 0.56/1.02 [50]P1(f116(a117))
% 0.56/1.02 [51]P1(f116(a118))
% 0.56/1.02 [52]P1(f116(a25))
% 0.56/1.02 [53]P1(f116(a84))
% 0.56/1.02 [54]P1(f116(a95))
% 0.56/1.02 [283]P12(f116(a1),f116(a118))
% 0.56/1.02 [284]P12(f116(a2),f116(a84))
% 0.56/1.02 [285]P12(f116(a3),f116(a2))
% 0.56/1.02 [286]P12(f116(a4),f116(a25))
% 0.56/1.02 [287]P12(f116(a118),f116(a117))
% 0.56/1.02 [288]P12(f116(a24),f116(a4))
% 0.56/1.02 [289]P12(f116(a25),f116(a3))
% 0.56/1.02 [290]P12(f116(a84),f116(a95))
% 0.56/1.02 [291]P12(f116(a95),f116(a1))
% 0.56/1.02 [292]P13(a1,f139(f116(a1)))
% 0.56/1.02 [293]P13(a2,f139(f116(a2)))
% 0.56/1.02 [294]P13(a3,f139(f116(a3)))
% 0.56/1.02 [295]P13(a4,f139(f116(a4)))
% 0.56/1.02 [296]P13(a117,f139(f116(a117)))
% 0.56/1.02 [297]P13(a118,f139(f116(a118)))
% 0.56/1.02 [298]P13(a24,f139(f116(a24)))
% 0.56/1.02 [299]P13(a25,f139(f116(a25)))
% 0.56/1.02 [300]P13(a84,f139(f116(a84)))
% 0.56/1.02 [301]P13(a95,f139(f116(a95)))
% 0.56/1.02 [302]P13(a140,f152(f116(a4)))
% 0.56/1.02 [303]P13(a153,f152(f116(a25)))
% 0.56/1.02 [304]P13(a193,f152(f116(a3)))
% 0.56/1.02 [305]P13(a204,f152(f116(a2)))
% 0.56/1.02 [306]P13(a215,f152(f116(a84)))
% 0.56/1.02 [307]P13(a226,f152(f116(a95)))
% 0.56/1.02 [308]P13(a237,f152(f116(a1)))
% 0.56/1.02 [309]P13(a248,f152(f116(a118)))
% 0.56/1.02 [310]P13(a259,f152(f116(a117)))
% 0.56/1.02 [542]P13(a106,f139(f282(f116(a84),f116(a95))))
% 0.56/1.02 [543]P13(a64,f139(f282(f116(a24),f116(a25))))
% 0.56/1.02 [544]P13(a96,f139(f282(f116(a2),f116(a84))))
% 0.56/1.02 [545]P13(a66,f139(f282(f116(a3),f116(a25))))
% 0.56/1.02 [546]P13(a74,f139(f282(f116(a24),f116(a3))))
% 0.56/1.02 [547]P13(a107,f139(f282(f116(a24),f116(a95))))
% 0.56/1.02 [548]P13(a120,f139(f282(f116(a24),f116(a1))))
% 0.56/1.02 [549]P13(a49,f139(f282(f116(a84),f116(a4))))
% 0.56/1.02 [550]P13(a27,f139(f282(f116(a24),f116(a4))))
% 0.56/1.02 [551]P13(a112,f139(f282(f116(a118),f116(a95))))
% 0.56/1.02 [552]P13(a60,f139(f282(f116(a95),f116(a4))))
% 0.56/1.02 [553]P13(a28,f139(f282(f116(a4),f116(a4))))
% 0.56/1.02 [554]P13(a50,f139(f282(f116(a3),f116(a4))))
% 0.56/1.02 [555]P13(a26,f139(f282(f116(a25),f116(a4))))
% 0.56/1.02 [556]P13(a129,f139(f282(f116(a84),f116(a118))))
% 0.56/1.02 [557]P13(a119,f139(f282(f116(a84),f116(a1))))
% 0.56/1.02 [558]P13(a65,f139(f282(f116(a2),f116(a25))))
% 0.56/1.02 [559]P13(a69,f139(f282(f116(a84),f116(a25))))
% 0.56/1.02 [560]P13(a125,f139(f282(f116(a118),f116(a1))))
% 0.56/1.02 [561]P13(a59,f139(f282(f116(a2),f116(a4))))
% 0.56/1.02 [562]P13(a61,f139(f282(f116(a1),f116(a4))))
% 0.56/1.02 [563]P13(a62,f139(f282(f116(a118),f116(a4))))
% 0.56/1.02 [564]P13(a63,f139(f282(f116(a117),f116(a4))))
% 0.56/1.02 [565]P13(a67,f139(f282(f116(a4),f116(a25))))
% 0.56/1.02 [566]P13(a68,f139(f282(f116(a25),f116(a25))))
% 0.56/1.02 [567]P13(a70,f139(f282(f116(a95),f116(a25))))
% 0.56/1.02 [568]P13(a71,f139(f282(f116(a1),f116(a25))))
% 0.56/1.02 [569]P13(a72,f139(f282(f116(a118),f116(a25))))
% 0.56/1.02 [570]P13(a73,f139(f282(f116(a117),f116(a25))))
% 0.56/1.02 [571]P13(a75,f139(f282(f116(a4),f116(a3))))
% 0.56/1.02 [572]P13(a76,f139(f282(f116(a25),f116(a3))))
% 0.56/1.02 [573]P13(a77,f139(f282(f116(a3),f116(a3))))
% 0.56/1.02 [574]P13(a78,f139(f282(f116(a2),f116(a3))))
% 0.56/1.02 [575]P13(a79,f139(f282(f116(a84),f116(a3))))
% 0.56/1.02 [576]P13(a80,f139(f282(f116(a95),f116(a3))))
% 0.56/1.02 [577]P13(a81,f139(f282(f116(a1),f116(a3))))
% 0.56/1.02 [578]P13(a82,f139(f282(f116(a118),f116(a3))))
% 0.56/1.02 [579]P13(a83,f139(f282(f116(a117),f116(a3))))
% 0.56/1.02 [580]P13(a85,f139(f282(f116(a24),f116(a2))))
% 0.56/1.02 [581]P13(a86,f139(f282(f116(a4),f116(a2))))
% 0.56/1.02 [582]P13(a87,f139(f282(f116(a25),f116(a2))))
% 0.56/1.02 [583]P13(a88,f139(f282(f116(a3),f116(a2))))
% 0.56/1.02 [584]P13(a89,f139(f282(f116(a2),f116(a2))))
% 0.56/1.02 [585]P13(a90,f139(f282(f116(a84),f116(a2))))
% 0.56/1.02 [586]P13(a91,f139(f282(f116(a95),f116(a2))))
% 0.56/1.02 [587]P13(a92,f139(f282(f116(a1),f116(a2))))
% 0.56/1.02 [588]P13(a93,f139(f282(f116(a118),f116(a2))))
% 0.56/1.02 [589]P13(a94,f139(f282(f116(a117),f116(a2))))
% 0.56/1.02 [590]P13(a97,f139(f282(f116(a24),f116(a84))))
% 0.56/1.02 [591]P13(a98,f139(f282(f116(a4),f116(a84))))
% 0.56/1.02 [592]P13(a99,f139(f282(f116(a25),f116(a84))))
% 0.56/1.02 [593]P13(a100,f139(f282(f116(a3),f116(a84))))
% 0.56/1.02 [594]P13(a101,f139(f282(f116(a84),f116(a84))))
% 0.56/1.02 [595]P13(a102,f139(f282(f116(a95),f116(a84))))
% 0.56/1.02 [596]P13(a103,f139(f282(f116(a1),f116(a84))))
% 0.56/1.02 [597]P13(a104,f139(f282(f116(a118),f116(a84))))
% 0.56/1.02 [598]P13(a105,f139(f282(f116(a117),f116(a84))))
% 0.56/1.02 [599]P13(a108,f139(f282(f116(a4),f116(a95))))
% 0.56/1.02 [600]P13(a109,f139(f282(f116(a25),f116(a95))))
% 0.56/1.02 [601]P13(a110,f139(f282(f116(a3),f116(a95))))
% 0.56/1.02 [602]P13(a111,f139(f282(f116(a2),f116(a95))))
% 0.56/1.02 [603]P13(a113,f139(f282(f116(a95),f116(a95))))
% 0.56/1.02 [604]P13(a114,f139(f282(f116(a1),f116(a95))))
% 0.56/1.02 [605]P13(a115,f139(f282(f116(a117),f116(a95))))
% 0.56/1.02 [606]P13(a121,f139(f282(f116(a4),f116(a1))))
% 0.56/1.02 [607]P13(a122,f139(f282(f116(a25),f116(a1))))
% 0.56/1.02 [608]P13(a123,f139(f282(f116(a3),f116(a1))))
% 0.56/1.02 [609]P13(a124,f139(f282(f116(a2),f116(a1))))
% 0.56/1.02 [610]P13(a126,f139(f282(f116(a95),f116(a1))))
% 0.56/1.02 [611]P13(a127,f139(f282(f116(a1),f116(a1))))
% 0.56/1.02 [612]P13(a128,f139(f282(f116(a117),f116(a1))))
% 0.56/1.02 [613]P13(a130,f139(f282(f116(a24),f116(a118))))
% 0.56/1.02 [614]P13(a131,f139(f282(f116(a4),f116(a118))))
% 0.56/1.02 [615]P13(a132,f139(f282(f116(a25),f116(a118))))
% 0.56/1.02 [616]P13(a133,f139(f282(f116(a3),f116(a118))))
% 0.56/1.02 [617]P13(a134,f139(f282(f116(a2),f116(a118))))
% 0.56/1.02 [618]P13(a135,f139(f282(f116(a95),f116(a118))))
% 0.56/1.02 [619]P13(a136,f139(f282(f116(a1),f116(a118))))
% 0.56/1.02 [620]P13(a137,f139(f282(f116(a118),f116(a118))))
% 0.56/1.02 [621]P13(a138,f139(f282(f116(a117),f116(a118))))
% 0.56/1.02 [622]P13(a142,f139(f282(f116(a24),f116(a117))))
% 0.56/1.02 [623]P13(a143,f139(f282(f116(a4),f116(a117))))
% 0.56/1.02 [624]P13(a144,f139(f282(f116(a25),f116(a117))))
% 0.56/1.02 [625]P13(a145,f139(f282(f116(a3),f116(a117))))
% 0.56/1.02 [626]P13(a146,f139(f282(f116(a2),f116(a117))))
% 0.56/1.02 [627]P13(a147,f139(f282(f116(a84),f116(a117))))
% 0.56/1.02 [628]P13(a148,f139(f282(f116(a95),f116(a117))))
% 0.56/1.02 [629]P13(a149,f139(f282(f116(a1),f116(a117))))
% 0.56/1.02 [630]P13(a150,f139(f282(f116(a118),f116(a117))))
% 0.56/1.02 [631]P13(a151,f139(f282(f116(a117),f116(a117))))
% 0.56/1.02 [632]P13(a154,f152(f282(f116(a24),f116(a4))))
% 0.56/1.02 [633]P13(a155,f152(f282(f116(a4),f116(a4))))
% 0.56/1.02 [634]P13(a166,f152(f282(f116(a25),f116(a4))))
% 0.56/1.02 [635]P13(a177,f152(f282(f116(a3),f116(a4))))
% 0.56/1.02 [636]P13(a187,f152(f282(f116(a2),f116(a4))))
% 0.56/1.02 [637]P13(a188,f152(f282(f116(a84),f116(a4))))
% 0.56/1.02 [638]P13(a189,f152(f282(f116(a95),f116(a4))))
% 0.56/1.02 [639]P13(a190,f152(f282(f116(a1),f116(a4))))
% 0.56/1.02 [640]P13(a191,f152(f282(f116(a118),f116(a4))))
% 0.56/1.02 [641]P13(a192,f152(f282(f116(a117),f116(a4))))
% 0.56/1.02 [642]P13(a194,f152(f282(f116(a24),f116(a25))))
% 0.56/1.02 [643]P13(a195,f152(f282(f116(a4),f116(a25))))
% 0.56/1.02 [644]P13(a196,f152(f282(f116(a25),f116(a25))))
% 0.56/1.02 [645]P13(a197,f152(f282(f116(a3),f116(a25))))
% 0.56/1.02 [646]P13(a198,f152(f282(f116(a2),f116(a25))))
% 0.56/1.02 [647]P13(a199,f152(f282(f116(a84),f116(a25))))
% 0.56/1.02 [648]P13(a200,f152(f282(f116(a95),f116(a25))))
% 0.56/1.02 [649]P13(a201,f152(f282(f116(a1),f116(a25))))
% 0.56/1.02 [650]P13(a202,f152(f282(f116(a118),f116(a25))))
% 0.56/1.02 [651]P13(a203,f152(f282(f116(a117),f116(a25))))
% 0.56/1.02 [652]P13(a205,f152(f282(f116(a24),f116(a3))))
% 0.56/1.02 [653]P13(a206,f152(f282(f116(a4),f116(a3))))
% 0.56/1.02 [654]P13(a207,f152(f282(f116(a25),f116(a3))))
% 0.56/1.02 [655]P13(a208,f152(f282(f116(a3),f116(a3))))
% 0.56/1.02 [656]P13(a209,f152(f282(f116(a2),f116(a3))))
% 0.56/1.02 [657]P13(a210,f152(f282(f116(a84),f116(a3))))
% 0.56/1.02 [658]P13(a211,f152(f282(f116(a95),f116(a3))))
% 0.56/1.02 [659]P13(a212,f152(f282(f116(a1),f116(a3))))
% 0.56/1.02 [660]P13(a213,f152(f282(f116(a118),f116(a3))))
% 0.56/1.02 [661]P13(a214,f152(f282(f116(a117),f116(a3))))
% 0.56/1.02 [662]P13(a216,f152(f282(f116(a24),f116(a2))))
% 0.56/1.02 [663]P13(a217,f152(f282(f116(a4),f116(a2))))
% 0.56/1.02 [664]P13(a218,f152(f282(f116(a25),f116(a2))))
% 0.56/1.02 [665]P13(a219,f152(f282(f116(a3),f116(a2))))
% 0.56/1.02 [666]P13(a220,f152(f282(f116(a2),f116(a2))))
% 0.56/1.02 [667]P13(a221,f152(f282(f116(a84),f116(a2))))
% 0.56/1.02 [668]P13(a222,f152(f282(f116(a95),f116(a2))))
% 0.56/1.02 [669]P13(a223,f152(f282(f116(a1),f116(a2))))
% 0.56/1.02 [670]P13(a224,f152(f282(f116(a118),f116(a2))))
% 0.56/1.02 [671]P13(a225,f152(f282(f116(a117),f116(a2))))
% 0.56/1.02 [672]P13(a227,f152(f282(f116(a24),f116(a84))))
% 0.56/1.02 [673]P13(a228,f152(f282(f116(a4),f116(a84))))
% 0.56/1.02 [674]P13(a229,f152(f282(f116(a25),f116(a84))))
% 0.56/1.02 [675]P13(a230,f152(f282(f116(a3),f116(a84))))
% 0.56/1.02 [676]P13(a231,f152(f282(f116(a2),f116(a84))))
% 0.56/1.02 [677]P13(a232,f152(f282(f116(a84),f116(a84))))
% 0.56/1.02 [678]P13(a233,f152(f282(f116(a95),f116(a84))))
% 0.56/1.02 [679]P13(a234,f152(f282(f116(a1),f116(a84))))
% 0.56/1.02 [680]P13(a235,f152(f282(f116(a118),f116(a84))))
% 0.56/1.02 [681]P13(a236,f152(f282(f116(a117),f116(a84))))
% 0.56/1.02 [682]P13(a238,f152(f282(f116(a24),f116(a95))))
% 0.56/1.02 [683]P13(a239,f152(f282(f116(a4),f116(a95))))
% 0.56/1.02 [684]P13(a240,f152(f282(f116(a25),f116(a95))))
% 0.56/1.02 [685]P13(a241,f152(f282(f116(a3),f116(a95))))
% 0.56/1.02 [686]P13(a242,f152(f282(f116(a2),f116(a95))))
% 0.56/1.02 [687]P13(a243,f152(f282(f116(a84),f116(a95))))
% 0.56/1.02 [688]P13(a244,f152(f282(f116(a95),f116(a95))))
% 0.56/1.02 [689]P13(a245,f152(f282(f116(a1),f116(a95))))
% 0.56/1.02 [690]P13(a246,f152(f282(f116(a118),f116(a95))))
% 0.56/1.02 [691]P13(a247,f152(f282(f116(a117),f116(a95))))
% 0.56/1.02 [692]P13(a249,f152(f282(f116(a24),f116(a1))))
% 0.56/1.02 [693]P13(a250,f152(f282(f116(a4),f116(a1))))
% 0.56/1.02 [694]P13(a251,f152(f282(f116(a25),f116(a1))))
% 0.56/1.02 [695]P13(a252,f152(f282(f116(a3),f116(a1))))
% 0.56/1.02 [696]P13(a253,f152(f282(f116(a2),f116(a1))))
% 0.56/1.02 [697]P13(a254,f152(f282(f116(a84),f116(a1))))
% 0.56/1.02 [698]P13(a255,f152(f282(f116(a95),f116(a1))))
% 0.56/1.02 [699]P13(a256,f152(f282(f116(a1),f116(a1))))
% 0.56/1.02 [700]P13(a257,f152(f282(f116(a118),f116(a1))))
% 0.56/1.02 [701]P13(a258,f152(f282(f116(a117),f116(a1))))
% 0.56/1.02 [702]P13(a260,f152(f282(f116(a24),f116(a118))))
% 0.56/1.02 [703]P13(a261,f152(f282(f116(a4),f116(a118))))
% 0.56/1.02 [704]P13(a262,f152(f282(f116(a25),f116(a118))))
% 0.56/1.02 [705]P13(a263,f152(f282(f116(a3),f116(a118))))
% 0.56/1.02 [706]P13(a264,f152(f282(f116(a2),f116(a118))))
% 0.56/1.02 [707]P13(a265,f152(f282(f116(a84),f116(a118))))
% 0.56/1.02 [708]P13(a266,f152(f282(f116(a95),f116(a118))))
% 0.56/1.02 [709]P13(a267,f152(f282(f116(a1),f116(a118))))
% 0.56/1.02 [710]P13(a268,f152(f282(f116(a118),f116(a118))))
% 0.56/1.02 [711]P13(a269,f152(f282(f116(a117),f116(a118))))
% 0.56/1.02 [712]P13(a271,f152(f282(f116(a24),f116(a117))))
% 0.56/1.02 [713]P13(a272,f152(f282(f116(a4),f116(a117))))
% 0.56/1.02 [714]P13(a273,f152(f282(f116(a25),f116(a117))))
% 0.56/1.02 [715]P13(a274,f152(f282(f116(a3),f116(a117))))
% 0.56/1.02 [716]P13(a275,f152(f282(f116(a2),f116(a117))))
% 0.56/1.02 [717]P13(a276,f152(f282(f116(a84),f116(a117))))
% 0.56/1.02 [718]P13(a277,f152(f282(f116(a95),f116(a117))))
% 0.56/1.02 [719]P13(a278,f152(f282(f116(a1),f116(a117))))
% 0.56/1.02 [720]P13(a279,f152(f282(f116(a118),f116(a117))))
% 0.56/1.02 [721]P13(a280,f152(f282(f116(a117),f116(a117))))
% 0.56/1.02 [722]P13(a29,f139(f282(f116(a24),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [723]P13(a30,f139(f282(f116(a4),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [724]P13(a31,f139(f282(f116(a25),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [725]P13(a32,f139(f282(f116(a3),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [726]P13(a33,f139(f282(f116(a2),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [727]P13(a34,f139(f282(f116(a84),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [728]P13(a35,f139(f282(f116(a95),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [729]P13(a36,f139(f282(f116(a1),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [730]P13(a37,f139(f282(f116(a118),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [731]P13(a38,f139(f282(f116(a117),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [732]P13(a39,f139(f282(f116(a24),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [733]P13(a40,f139(f282(f116(a4),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [734]P13(a41,f139(f282(f116(a25),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [735]P13(a42,f139(f282(f116(a3),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [736]P13(a43,f139(f282(f116(a2),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [737]P13(a44,f139(f282(f116(a84),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [738]P13(a45,f139(f282(f116(a95),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [739]P13(a46,f139(f282(f116(a1),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [740]P13(a47,f139(f282(f116(a118),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [741]P13(a48,f139(f282(f116(a117),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [742]P13(a51,f139(f282(f116(a24),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [743]P13(a52,f139(f282(f116(a4),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [744]P13(a53,f139(f282(f116(a25),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [745]P13(a54,f139(f282(f116(a3),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [746]P13(a55,f139(f282(f116(a2),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [747]P13(a56,f139(f282(f116(a84),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [748]P13(a57,f139(f282(f116(a95),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [749]P13(a58,f139(f282(f116(a1),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [750]P13(a156,f152(f282(f116(a24),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [751]P13(a157,f152(f282(f116(a4),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [752]P13(a158,f152(f282(f116(a25),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [753]P13(a159,f152(f282(f116(a3),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [754]P13(a160,f152(f282(f116(a2),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [755]P13(a161,f152(f282(f116(a84),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [756]P13(a162,f152(f282(f116(a95),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [757]P13(a163,f152(f282(f116(a1),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [758]P13(a164,f152(f282(f116(a118),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [759]P13(a165,f152(f282(f116(a117),f282(f116(a24),f116(a4)))))
% 0.56/1.02 [760]P13(a167,f152(f282(f116(a24),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [761]P13(a168,f152(f282(f116(a4),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [762]P13(a169,f152(f282(f116(a25),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [763]P13(a170,f152(f282(f116(a3),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [764]P13(a171,f152(f282(f116(a2),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [765]P13(a172,f152(f282(f116(a84),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [766]P13(a173,f152(f282(f116(a95),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [767]P13(a174,f152(f282(f116(a1),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [768]P13(a175,f152(f282(f116(a118),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [769]P13(a176,f152(f282(f116(a117),f282(f116(a4),f116(a4)))))
% 0.56/1.02 [770]P13(a178,f152(f282(f116(a24),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [771]P13(a179,f152(f282(f116(a4),f282(f116(a25),f116(a4)))))
% 0.56/1.02 [772]P13(a180,f152(f282(f116(a25),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [773]P13(a181,f152(f282(f116(a3),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [774]P13(a182,f152(f282(f116(a2),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [775]P13(a183,f152(f282(f116(a84),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [776]P13(a184,f152(f282(f116(a95),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [777]P13(a185,f152(f282(f116(a1),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [778]P13(a186,f152(f282(f116(a118),f282(f116(a25),f116(a4)))))
% 0.56/1.03 [948]~P2(x9481,a286)+P5(x9481,a9,a106)
% 0.56/1.03 [949]~P2(x9491,a11)+P5(x9491,a9,a96)
% 0.56/1.03 [950]~P2(x9501,a287)+P5(x9501,a9,a74)
% 0.56/1.03 [951]~P2(x9511,a289)+P5(x9511,a9,a74)
% 0.56/1.03 [952]~P2(x9521,a12)+P5(x9521,a9,a120)
% 0.56/1.03 [953]~P2(x9531,a281)+P5(x9531,a9,a120)
% 0.56/1.03 [954]~P2(x9541,a290)+P5(x9541,a9,a120)
% 0.56/1.03 [955]~P2(x9551,a285)+P5(x9551,a9,a112)
% 0.56/1.03 [956]~P2(x9561,a288)+P5(x9561,a9,a24)
% 0.56/1.03 [957]~P2(x9571,a6)+P5(x9571,a9,a26)
% 0.56/1.03 [958]~P2(x9581,a283)+P5(x9581,a9,a119)
% 0.56/1.03 [959]~P2(x9591,a14)+P5(x9591,a9,a119)
% 0.56/1.03 [960]~P2(x9601,a7)+P5(x9601,a9,a125)
% 0.56/1.03 [961]~P2(x9611,a286)+P5(x9611,a10,a64)
% 0.56/1.03 [962]~P2(x9621,a290)+P5(x9621,a10,a64)
% 0.56/1.03 [963]~P2(x9631,a7)+P5(x9631,a10,a64)
% 0.56/1.03 [964]~P2(x9641,a11)+P5(x9641,a10,a66)
% 0.56/1.03 [965]~P2(x9651,a6)+P5(x9651,a10,a3)
% 0.56/1.03 [966]~P2(x9661,a287)+P5(x9661,a10,a118)
% 0.56/1.03 [967]~P2(x9671,a12)+P5(x9671,a10,a49)
% 0.56/1.03 [968]~P2(x9681,a285)+P5(x9681,a10,a60)
% 0.56/1.03 [969]~P2(x9691,a281)+P5(x9691,a10,a50)
% 0.56/1.03 [970]~P2(x9701,a288)+P5(x9701,a10,a24)
% 0.56/1.03 [971]~P2(x9711,a289)+P5(x9711,a10,a24)
% 0.56/1.03 [972]~P2(x9721,a283)+P5(x9721,a10,a65)
% 0.56/1.03 [973]~P2(x9731,a14)+P5(x9731,a10,a69)
% 0.56/1.03 [974]~P2(x9741,a289)+P5(x9741,a23,a106)
% 0.56/1.03 [975]~P2(x9751,a286)+P5(x9751,a23,a1)
% 0.56/1.03 [976]~P2(x9761,a11)+P5(x9761,a23,a3)
% 0.56/1.03 [977]~P2(x9771,a12)+P5(x9771,a23,a4)
% 0.56/1.03 [978]~P2(x9781,a285)+P5(x9781,a23,a4)
% 0.56/1.03 [979]~P2(x9791,a283)+P5(x9791,a23,a4)
% 0.56/1.03 [980]~P2(x9801,a7)+P5(x9801,a23,a4)
% 0.56/1.03 [981]~P2(x9811,a290)+P5(x9811,a23,a118)
% 0.56/1.03 [982]~P2(x9821,a287)+P5(x9821,a23,a107)
% 0.56/1.03 [983]~P2(x9831,a281)+P5(x9831,a23,a24)
% 0.56/1.03 [984]~P2(x9841,a6)+P5(x9841,a23,a24)
% 0.56/1.03 [985]~P2(x9851,a288)+P5(x9851,a23,a24)
% 0.56/1.03 [986]~P2(x9861,a14)+P5(x9861,a23,a24)
% 0.56/1.03 [987]~P2(x9871,a286)+P5(x9871,a141,a2)
% 0.56/1.03 [988]~P2(x9881,a11)+P5(x9881,a141,a4)
% 0.56/1.03 [989]~P2(x9891,a287)+P5(x9891,a141,a4)
% 0.56/1.03 [990]~P2(x9901,a281)+P5(x9901,a141,a49)
% 0.56/1.03 [991]~P2(x9911,a12)+P5(x9911,a141,a27)
% 0.56/1.03 [992]~P2(x9921,a285)+P5(x9921,a141,a28)
% 0.56/1.03 [993]~P2(x9931,a283)+P5(x9931,a141,a24)
% 0.56/1.03 [994]~P2(x9941,a14)+P5(x9941,a141,a24)
% 0.56/1.03 [995]~P2(x9951,a290)+P5(x9951,a141,a24)
% 0.56/1.03 [996]~P2(x9961,a7)+P5(x9961,a141,a24)
% 0.56/1.03 [997]~P2(x9971,a289)+P5(x9971,a141,a24)
% 0.56/1.03 [998]~P2(x9981,a6)+P5(x9981,a141,a129)
% 0.56/1.03 [999]~P2(x9991,a288)+P5(x9991,a141,a29)
% 0.56/1.03 [1000]~P2(x10001,a286)+P5(x10001,a270,a2)
% 0.56/1.03 [1001]~P2(x10011,a12)+P5(x10011,a270,a2)
% 0.56/1.03 [1002]~P2(x10021,a285)+P5(x10021,a270,a2)
% 0.56/1.03 [1003]~P2(x10031,a287)+P5(x10031,a270,a4)
% 0.56/1.03 [1004]~P2(x10041,a7)+P5(x10041,a270,a4)
% 0.56/1.03 [1005]~P2(x10051,a11)+P5(x10051,a270,a117)
% 0.56/1.03 [1006]~P2(x10061,a6)+P5(x10061,a270,a24)
% 0.56/1.03 [1007]~P2(x10071,a288)+P5(x10071,a270,a24)
% 0.56/1.03 [1008]~P2(x10081,a283)+P5(x10081,a270,a24)
% 0.56/1.03 [1009]~P2(x10091,a14)+P5(x10091,a270,a24)
% 0.56/1.03 [1010]~P2(x10101,a281)+P5(x10101,a270,a25)
% 0.56/1.03 [1011]~P2(x10111,a290)+P5(x10111,a270,a25)
% 0.56/1.03 [1012]~P2(x10121,a289)+P5(x10121,a270,a84)
% 0.56/1.03 [939]P10(f116(x9391))+~P1(f116(x9391))
% 0.56/1.03 [937]~E(x9371,x9372)+P8(x9371,x9372)
% 0.56/1.03 [938]~P9(x9382,x9381)+~E(x9381,x9382)
% 0.56/1.03 [941]~P11(x9411,x9412)+P4(x9411,x9412)
% 0.56/1.03 [942]~P9(x9421,x9422)+P8(x9421,x9422)
% 0.56/1.03 [944]~P9(x9442,x9441)+~P9(x9441,x9442)
% 0.56/1.03 [945]~P10(x9452)+P10(f282(f116(x9451),x9452))
% 0.56/1.03 [1014]P2(x10141,x10142)+~P14(x10141,x10143,x10142)
% 0.56/1.03 [1015]P3(x10151,x10152)+~P14(x10151,x10152,x10153)
% 0.56/1.03 [1016]P3(x10161,x10162)+~P6(x10161,x10162,x10163)
% 0.56/1.03 [947]~P10(x9473)+P12(f116(x9471),f282(f116(x9472),x9473))
% 0.56/1.03 [1026]P2(x10261,x10262)+~P7(x10261,x10263,x10262,x10264)
% 0.56/1.03 [1027]P3(x10271,x10272)+~P7(x10271,x10272,x10273,x10274)
% 0.56/1.03 [1028]P4(x10281,x10282)+~P7(x10281,x10283,x10284,x10282)
% 0.56/1.03 [1020]~P12(x10202,x10204)+P12(f282(f116(x10201),x10202),f282(f116(x10203),x10204))
% 0.56/1.03 [940]P9(x9402,x9401)+P9(x9401,x9402)+E(x9401,x9402)
% 0.56/1.03 [943]P9(x9431,x9432)+~P8(x9431,x9432)+E(x9431,x9432)
% 0.56/1.03 [946]~P9(x9462,x9463)+P4(x9461,x9462)+~P4(x9461,x9463)
% 0.56/1.03 [1021]P8(x10211,x10212)+~P9(x10211,x10213)+~P15(x10212,a4,x10213)
% 0.56/1.03 [1022]~P16(x10221,x10223,x10222)+~P2(x10221,x10222)+~P3(x10221,x10223)
% 0.56/1.03 [1019]P12(f116(x10191),f116(x10192))+~P12(f116(x10193),f116(x10192))+~P12(f116(x10191),f116(x10193))
% 0.56/1.03 [1023]~P10(x10232)+~P12(f116(x10231),f116(x10233))+P12(f282(f116(x10231),x10232),f282(f116(x10233),x10232))
% 0.56/1.03 [1024]~P5(x10241,x10242,x10244)+P5(x10241,x10242,x10243)+~P9(x10243,x10244)
% 0.56/1.03 [1013]P9(x10131,x10132)+~P13(x10132,f139(x10133))+~P13(x10131,f152(x10134))
% 0.56/1.03 [1025]~P2(x10251,x10253)+~P3(x10251,x10252)+~P4(x10251,x10254)+P7(x10251,x10252,x10253,x10254)
% 0.56/1.03 [1017]P9(x10171,x10172)+~P12(x10173,x10174)+~P13(x10172,f152(x10173))+~P13(x10171,f152(x10174))
% 0.56/1.03 [1018]P9(x10181,x10182)+~P12(x10183,x10184)+~P13(x10182,f139(x10184))+~P13(x10181,f139(x10183))
% 0.56/1.03 [1029]P2(x10291,a286)+~P5(x10291,a9,a106)+~P5(x10291,a10,a64)+~P5(x10291,a23,a1)+~P5(x10291,a141,a2)+~P5(x10291,a270,a2)
% 0.56/1.03 [1030]P2(x10301,a11)+~P5(x10301,a9,a96)+~P5(x10301,a10,a66)+~P5(x10301,a23,a3)+~P5(x10301,a141,a4)+~P5(x10301,a270,a117)
% 0.56/1.03 [1031]P2(x10311,a287)+~P5(x10311,a9,a74)+~P5(x10311,a10,a118)+~P5(x10311,a23,a107)+~P5(x10311,a141,a4)+~P5(x10311,a270,a4)
% 0.56/1.03 [1032]P2(x10321,a12)+~P5(x10321,a9,a120)+~P5(x10321,a10,a49)+~P5(x10321,a23,a4)+~P5(x10321,a141,a27)+~P5(x10321,a270,a2)
% 0.56/1.03 [1033]P2(x10331,a285)+~P5(x10331,a9,a112)+~P5(x10331,a10,a60)+~P5(x10331,a23,a4)+~P5(x10331,a141,a28)+~P5(x10331,a270,a2)
% 0.56/1.03 [1034]P2(x10341,a281)+~P5(x10341,a9,a120)+~P5(x10341,a10,a50)+~P5(x10341,a23,a24)+~P5(x10341,a141,a49)+~P5(x10341,a270,a25)
% 0.56/1.03 [1035]P2(x10351,a6)+~P5(x10351,a9,a26)+~P5(x10351,a10,a3)+~P5(x10351,a23,a24)+~P5(x10351,a141,a129)+~P5(x10351,a270,a24)
% 0.56/1.03 [1036]P2(x10361,a288)+~P5(x10361,a9,a24)+~P5(x10361,a10,a24)+~P5(x10361,a23,a24)+~P5(x10361,a141,a29)+~P5(x10361,a270,a24)
% 0.56/1.03 [1037]P2(x10371,a283)+~P5(x10371,a9,a119)+~P5(x10371,a10,a65)+~P5(x10371,a23,a4)+~P5(x10371,a141,a24)+~P5(x10371,a270,a24)
% 0.56/1.03 [1038]P2(x10381,a14)+~P5(x10381,a9,a119)+~P5(x10381,a10,a69)+~P5(x10381,a23,a24)+~P5(x10381,a141,a24)+~P5(x10381,a270,a24)
% 0.56/1.03 [1039]P2(x10391,a290)+~P5(x10391,a9,a120)+~P5(x10391,a10,a64)+~P5(x10391,a23,a118)+~P5(x10391,a141,a24)+~P5(x10391,a270,a25)
% 0.56/1.03 [1040]P2(x10401,a7)+~P5(x10401,a9,a125)+~P5(x10401,a10,a64)+~P5(x10401,a23,a4)+~P5(x10401,a141,a24)+~P5(x10401,a270,a4)
% 0.56/1.03 [1041]P2(x10411,a289)+~P5(x10411,a9,a74)+~P5(x10411,a10,a24)+~P5(x10411,a23,a106)+~P5(x10411,a141,a24)+~P5(x10411,a270,a84)
% 0.56/1.03 %EqnAxiom
% 0.56/1.03 [1]E(x11,x11)
% 0.56/1.03 [2]E(x22,x21)+~E(x21,x22)
% 0.56/1.03 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.56/1.03 [4]~E(x41,x42)+E(f116(x41),f116(x42))
% 0.56/1.03 [5]~E(x51,x52)+E(f282(x51,x53),f282(x52,x53))
% 0.56/1.03 [6]~E(x61,x62)+E(f282(x63,x61),f282(x63,x62))
% 0.56/1.03 [7]~E(x71,x72)+E(f152(x71),f152(x72))
% 0.56/1.03 [8]~E(x81,x82)+E(f139(x81),f139(x82))
% 0.56/1.03 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 0.56/1.03 [10]P5(x102,x103,x104)+~E(x101,x102)+~P5(x101,x103,x104)
% 0.56/1.03 [11]P5(x113,x112,x114)+~E(x111,x112)+~P5(x113,x111,x114)
% 0.56/1.03 [12]P5(x123,x124,x122)+~E(x121,x122)+~P5(x123,x124,x121)
% 0.56/1.03 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133)
% 0.56/1.03 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141)
% 0.56/1.03 [15]P7(x152,x153,x154,x155)+~E(x151,x152)+~P7(x151,x153,x154,x155)
% 0.56/1.03 [16]P7(x163,x162,x164,x165)+~E(x161,x162)+~P7(x163,x161,x164,x165)
% 0.56/1.03 [17]P7(x173,x174,x172,x175)+~E(x171,x172)+~P7(x173,x174,x171,x175)
% 0.56/1.03 [18]P7(x183,x184,x185,x182)+~E(x181,x182)+~P7(x183,x184,x185,x181)
% 0.56/1.03 [19]P13(x192,x193)+~E(x191,x192)+~P13(x191,x193)
% 0.56/1.03 [20]P13(x203,x202)+~E(x201,x202)+~P13(x203,x201)
% 0.56/1.03 [21]P16(x212,x213,x214)+~E(x211,x212)+~P16(x211,x213,x214)
% 0.56/1.03 [22]P16(x223,x222,x224)+~E(x221,x222)+~P16(x223,x221,x224)
% 0.56/1.03 [23]P16(x233,x234,x232)+~E(x231,x232)+~P16(x233,x234,x231)
% 0.56/1.03 [24]P4(x242,x243)+~E(x241,x242)+~P4(x241,x243)
% 0.56/1.03 [25]P4(x253,x252)+~E(x251,x252)+~P4(x253,x251)
% 0.56/1.03 [26]P3(x262,x263)+~E(x261,x262)+~P3(x261,x263)
% 0.56/1.03 [27]P3(x273,x272)+~E(x271,x272)+~P3(x273,x271)
% 0.56/1.03 [28]P12(x282,x283)+~E(x281,x282)+~P12(x281,x283)
% 0.56/1.03 [29]P12(x293,x292)+~E(x291,x292)+~P12(x293,x291)
% 0.56/1.03 [30]P9(x302,x303)+~E(x301,x302)+~P9(x301,x303)
% 0.56/1.03 [31]P9(x313,x312)+~E(x311,x312)+~P9(x313,x311)
% 0.56/1.03 [32]~P10(x321)+P10(x322)+~E(x321,x322)
% 0.56/1.03 [33]P6(x332,x333,x334)+~E(x331,x332)+~P6(x331,x333,x334)
% 0.56/1.03 [34]P6(x343,x342,x344)+~E(x341,x342)+~P6(x343,x341,x344)
% 0.56/1.03 [35]P6(x353,x354,x352)+~E(x351,x352)+~P6(x353,x354,x351)
% 0.56/1.03 [36]P8(x362,x363)+~E(x361,x362)+~P8(x361,x363)
% 0.56/1.03 [37]P8(x373,x372)+~E(x371,x372)+~P8(x373,x371)
% 0.56/1.03 [38]P14(x382,x383,x384)+~E(x381,x382)+~P14(x381,x383,x384)
% 0.56/1.03 [39]P14(x393,x392,x394)+~E(x391,x392)+~P14(x393,x391,x394)
% 0.56/1.03 [40]P14(x403,x404,x402)+~E(x401,x402)+~P14(x403,x404,x401)
% 0.56/1.03 [41]P11(x412,x413)+~E(x411,x412)+~P11(x411,x413)
% 0.56/1.03 [42]P11(x423,x422)+~E(x421,x422)+~P11(x423,x421)
% 0.56/1.03 [43]P15(x432,x433,x434)+~E(x431,x432)+~P15(x431,x433,x434)
% 0.56/1.03 [44]P15(x443,x442,x444)+~E(x441,x442)+~P15(x443,x441,x444)
% 0.56/1.03 [45]P15(x453,x454,x452)+~E(x451,x452)+~P15(x453,x454,x451)
% 0.56/1.03
% 0.56/1.03 %-------------------------------------------
% 0.56/1.03 cnf(1043,plain,
% 0.56/1.03 (~P9(x10431,x10431)),
% 0.56/1.03 inference(equality_inference,[],[938])).
% 0.56/1.03 cnf(1075,plain,
% 0.56/1.03 (~P9(x10751,x10751)),
% 0.56/1.03 inference(rename_variables,[],[1043])).
% 0.56/1.03 cnf(1081,plain,
% 0.56/1.03 ($false),
% 0.56/1.03 inference(scs_inference,[],[934,55,56,76,90,97,102,165,166,182,212,271,779,815,831,875,901,929,1043,1075,489,505,517,891,893,894,292,302,941,1014,1015,1016,1026,1027,1028,15,16,17,18,946,13,14,24,25,26,27,1013,1022,30,31,33,38,39,1025]),
% 0.56/1.03 ['proof']).
% 0.56/1.03 % SZS output end Proof
% 0.56/1.03 % Total time :0.190000s
%------------------------------------------------------------------------------