%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : AGT015+1 : TPTP v8.2.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n009.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:20 EDT 2024
% Result : Theorem 63.06s 63.16s
% Output : CNFRefutation 63.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : AGT015+1 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n009.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 : Wed Jun 19 04:03:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.58 start to proof:theBenchmark
% 63.06/63.15 %-------------------------------------------
% 63.06/63.16 % File :CSE---1.7
% 63.06/63.16 % Problem :theBenchmark
% 63.06/63.16 % Transform :cnf
% 63.06/63.16 % Format :tptp:raw
% 63.06/63.16 % Command :java -jar mcs_scs.jar %d %s
% 63.06/63.16
% 63.06/63.16 % Result :Theorem 62.450000s
% 63.06/63.16 % Output :CNFRefutation 62.450000s
% 63.06/63.16 %-------------------------------------------
% 63.06/63.16 %--------------------------------------------------------------------------
% 63.06/63.16 % File : AGT015+1 : TPTP v8.2.0. Bugfixed v3.1.0.
% 63.06/63.16 % Domain : Agents
% 63.06/63.16 % Problem : Problem for the CPlanT system
% 63.06/63.16 % Version : [Bar03] axioms : Especial.
% 63.06/63.16 % English :
% 63.06/63.16
% 63.06/63.16 % Refs : [Bar03] Barta, J. (2003), Email to G. Sutcliffe
% 63.06/63.16 % : [BT+03] Barta et al. (2003), Meta-Reasoning in CPlanT Multi-Ag
% 63.06/63.16 % : [TBP03] Tozicka et al. (2003), Meta-reasoning for Agents' Priv
% 63.06/63.16 % Source : [Bar03]
% 63.06/63.16 % Names :
% 63.06/63.16
% 63.06/63.16 % Status : Theorem
% 63.06/63.16 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.23 v7.3.0, 0.24 .0, 0.22 v7.0.0, 0.20 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.20 .0, 0.13 v5.5.0, 0.19 v5.4.0, 0.14 v5.3.0, 0.22 v5.2.0, 0.15 .0, 0.19 v5.0.0, 0.25 .0, 0.22 v4.0.0, 0.21 v3.7.0, 0.20 v3.5.0, 0.21 v3.2.0, 0.27 .0
% 63.06/63.16 % Syntax : Number of formulae : 556 ( 524 unt; 0 def)
% 63.06/63.16 % Number of atoms : 656 ( 2 equ)
% 63.06/63.16 % Maximal formula atoms : 6 ( 1 avg)
% 63.06/63.16 % Number of connectives : 144 ( 44 ~; 1 |; 67 &)
% 63.06/63.16 % ( 16 <=>; 16 =>; 0 <=; 0 <~>)
% 63.06/63.16 % Maximal formula depth : 8 ( 1 avg)
% 63.06/63.16 % Maximal term depth : 5 ( 2 avg)
% 63.06/63.16 % Number of predicates : 17 ( 16 usr; 0 prp; 1-4 aty)
% 63.06/63.16 % Number of functors : 290 ( 290 usr; 286 con; 0-2 aty)
% 63.06/63.16 % Number of variables : 72 ( 70 !; 2 ?)
% 63.06/63.16 % SPC : FOF_THM_RFO_SEQ
% 63.06/63.16
% 63.06/63.16 % Comments :
% 63.06/63.16 % Bugfixes : v3.0.0 - Bugfixes in NUM005+1.ax
% 63.06/63.16 % : v3.1.0 - Changes to NUM005 axioms
% 63.06/63.16 %--------------------------------------------------------------------------
% 63.06/63.16 %----Include axioms of CPlanT
% 63.06/63.16 include('Axioms/AGT001+0.ax').
% 63.06/63.16 %----Include events of CPlanT
% 63.06/63.16 include('Axioms/AGT001+1.ax').
% 63.06/63.16 %----Include axioms for RDN and RDN less
% 63.06/63.16 include('Axioms/NUM005+0.ax').
% 63.06/63.16 include('Axioms/NUM005+1.ax').
% 63.06/63.16 %--------------------------------------------------------------------------
% 63.06/63.16 fof(query_15,conjecture,
% 63.06/63.16 ? [X,Y] : ~ accept_city(X,Y) ).
% 63.06/63.16
% 63.06/63.16 %--------------------------------------------------------------------------
% 63.06/63.16 %-------------------------------------------
% 63.06/63.16 % Proof found
% 63.06/63.16 % SZS status Theorem for theBenchmark
% 63.06/63.16 % SZS output start Proof
% 63.16/63.17 %ClaNum:656(EqnAxiom:43)
% 63.16/63.17 %VarNum:177(SingletonVarNum:113)
% 63.16/63.17 %MaxLitNum:4
% 63.16/63.17 %MaxfuncDepth:4
% 63.16/63.17 %SharedTerms:1120
% 63.16/63.17 %goalClause: 178 179 181 184 185 186 187 189 190 193 194 195 196 197 198 199 201 202 203 204 205 206 210 211 212 216 217 219 220 221 222 227 228 229 232 234 235 239 241 242 648 654
% 63.16/63.17 %singleGoalClaCount:40
% 63.16/63.17 [53]P2(a5,a22)
% 63.16/63.17 [54]P2(a5,a81)
% 63.16/63.17 [55]P2(a5,a92)
% 63.16/63.17 [56]P2(a6,a22)
% 63.16/63.17 [57]P2(a6,a92)
% 63.16/63.17 [58]P2(a13,a22)
% 63.16/63.17 [59]P2(a13,a92)
% 63.16/63.17 [60]P2(a7,a3)
% 63.16/63.17 [61]P2(a7,a22)
% 63.16/63.17 [62]P2(a7,a81)
% 63.16/63.17 [63]P2(a7,a92)
% 63.16/63.17 [64]P2(a14,a2)
% 63.16/63.17 [65]P2(a14,a3)
% 63.16/63.17 [66]P2(a14,a22)
% 63.16/63.17 [67]P2(a15,a2)
% 63.16/63.17 [68]P2(a15,a4)
% 63.16/63.17 [69]P2(a15,a22)
% 63.16/63.17 [70]P2(a15,a81)
% 63.16/63.17 [71]P2(a15,a92)
% 63.16/63.17 [72]P2(a18,a3)
% 63.16/63.17 [73]P2(a18,a22)
% 63.16/63.17 [74]P2(a18,a92)
% 63.16/63.17 [75]P2(a19,a2)
% 63.16/63.17 [76]P2(a19,a3)
% 63.16/63.17 [77]P2(a19,a22)
% 63.16/63.17 [78]P2(a19,a81)
% 63.16/63.17 [79]P2(a19,a92)
% 63.16/63.17 [80]P2(a16,a92)
% 63.16/63.17 [81]P2(a17,a3)
% 63.16/63.17 [82]P2(a17,a22)
% 63.16/63.17 [83]P2(a17,a81)
% 63.16/63.17 [84]P2(a17,a92)
% 63.16/63.17 [85]P2(a10,a22)
% 63.16/63.17 [86]P2(a10,a92)
% 63.16/63.17 [87]P2(a279,a22)
% 63.16/63.17 [88]P2(a279,a81)
% 63.16/63.17 [89]P2(a279,a92)
% 63.16/63.17 [118]P13(a5,a7,a11)
% 63.16/63.17 [119]P13(a5,a15,a12)
% 63.16/63.17 [120]P13(a6,a7,a11)
% 63.16/63.17 [121]P13(a6,a15,a12)
% 63.16/63.17 [122]P13(a13,a7,a11)
% 63.16/63.17 [123]P13(a13,a15,a12)
% 63.16/63.17 [124]P13(a7,a5,a280)
% 63.16/63.17 [125]P13(a7,a6,a281)
% 63.16/63.17 [126]P13(a7,a279,a281)
% 63.16/63.17 [127]P13(a14,a5,a280)
% 63.16/63.17 [128]P13(a14,a6,a281)
% 63.16/63.17 [129]P13(a14,a279,a281)
% 63.16/63.17 [130]P13(a15,a5,a280)
% 63.16/63.17 [131]P13(a15,a6,a281)
% 63.16/63.17 [132]P13(a15,a279,a281)
% 63.16/63.17 [133]P13(a18,a5,a280)
% 63.16/63.17 [134]P13(a19,a5,a280)
% 63.16/63.17 [135]P13(a19,a6,a281)
% 63.16/63.17 [136]P13(a19,a279,a281)
% 63.16/63.17 [137]P13(a16,a15,a12)
% 63.16/63.17 [138]P13(a17,a5,a280)
% 63.16/63.17 [139]P13(a17,a6,a281)
% 63.16/63.17 [140]P13(a17,a279,a281)
% 63.16/63.17 [141]P13(a10,a7,a11)
% 63.16/63.17 [142]P13(a10,a15,a12)
% 63.16/63.17 [143]P13(a279,a7,a11)
% 63.16/63.17 [144]P13(a279,a15,a12)
% 63.16/63.17 [145]P4(a5,a7,a11)
% 63.16/63.17 [146]P4(a5,a15,a12)
% 63.16/63.17 [147]P4(a6,a7,a11)
% 63.16/63.17 [148]P4(a6,a15,a12)
% 63.16/63.17 [149]P4(a13,a7,a11)
% 63.16/63.17 [150]P4(a13,a15,a12)
% 63.16/63.17 [151]P4(a7,a5,a280)
% 63.16/63.17 [152]P4(a7,a6,a281)
% 63.16/63.17 [153]P4(a7,a279,a281)
% 63.16/63.17 [154]P4(a14,a5,a280)
% 63.16/63.17 [155]P4(a14,a6,a281)
% 63.16/63.17 [156]P4(a14,a279,a281)
% 63.16/63.17 [157]P4(a15,a5,a280)
% 63.16/63.17 [158]P4(a15,a6,a281)
% 63.16/63.17 [159]P4(a15,a279,a281)
% 63.16/63.17 [160]P4(a18,a5,a280)
% 63.16/63.17 [161]P4(a18,a6,a281)
% 63.16/63.17 [162]P4(a18,a279,a281)
% 63.16/63.17 [163]P4(a19,a5,a280)
% 63.16/63.17 [164]P4(a19,a6,a281)
% 63.16/63.17 [165]P4(a19,a279,a281)
% 63.16/63.17 [166]P4(a16,a7,a11)
% 63.16/63.17 [167]P4(a16,a15,a12)
% 63.16/63.17 [168]P4(a17,a5,a280)
% 63.16/63.17 [169]P4(a17,a6,a281)
% 63.16/63.17 [170]P4(a17,a279,a281)
% 63.16/63.17 [171]P4(a10,a7,a11)
% 63.16/63.17 [172]P4(a10,a15,a12)
% 63.16/63.17 [173]P4(a279,a7,a11)
% 63.16/63.17 [174]P4(a279,a15,a12)
% 63.16/63.17 [175]P15(a18,a6,a281)
% 63.16/63.17 [176]P15(a18,a279,a281)
% 63.16/63.17 [177]P15(a16,a7,a11)
% 63.16/63.17 [480]P6(a5,a6,a11,a92)
% 63.16/63.17 [481]P6(a5,a6,a281,a92)
% 63.16/63.17 [482]P6(a5,a6,a12,a92)
% 63.16/63.17 [483]P6(a5,a13,a11,a92)
% 63.16/63.17 [484]P6(a5,a279,a281,a81)
% 63.16/63.17 [485]P6(a5,a279,a281,a92)
% 63.16/63.17 [486]P6(a6,a5,a11,a81)
% 63.16/63.17 [487]P6(a6,a5,a11,a92)
% 63.16/63.17 [488]P6(a6,a5,a12,a92)
% 63.16/63.17 [489]P6(a6,a5,a280,a92)
% 63.16/63.17 [490]P6(a6,a13,a11,a92)
% 63.16/63.17 [491]P6(a6,a279,a281,a81)
% 63.16/63.17 [492]P6(a6,a279,a281,a92)
% 63.16/63.17 [493]P6(a13,a5,a11,a81)
% 63.16/63.17 [494]P6(a13,a5,a11,a92)
% 63.16/63.17 [495]P6(a13,a5,a12,a92)
% 63.16/63.17 [496]P6(a13,a5,a280,a92)
% 63.16/63.17 [497]P6(a13,a6,a11,a92)
% 63.16/63.17 [498]P6(a13,a6,a281,a92)
% 63.16/63.17 [499]P6(a13,a6,a12,a92)
% 63.16/63.17 [500]P6(a13,a279,a281,a81)
% 63.16/63.17 [501]P6(a13,a279,a281,a92)
% 63.16/63.17 [502]P6(a7,a14,a281,a2)
% 63.16/63.17 [503]P6(a7,a14,a280,a2)
% 63.16/63.17 [504]P6(a7,a15,a281,a92)
% 63.16/63.17 [505]P6(a7,a15,a12,a2)
% 63.16/63.17 [506]P6(a7,a15,a12,a81)
% 63.16/63.17 [507]P6(a7,a15,a12,a92)
% 63.16/63.17 [508]P6(a7,a15,a280,a92)
% 63.16/63.17 [509]P6(a7,a18,a280,a92)
% 63.16/63.17 [510]P6(a7,a19,a281,a2)
% 63.16/63.17 [511]P6(a7,a19,a281,a81)
% 63.16/63.17 [512]P6(a7,a19,a281,a92)
% 63.16/63.17 [513]P6(a7,a19,a280,a92)
% 63.16/63.17 [514]P6(a7,a17,a281,a92)
% 63.16/63.17 [515]P6(a7,a17,a280,a92)
% 63.16/63.17 [516]P6(a14,a15,a12,a22)
% 63.16/63.17 [517]P6(a14,a19,a281,a2)
% 63.16/63.17 [518]P6(a15,a7,a11,a81)
% 63.16/63.17 [519]P6(a15,a7,a11,a92)
% 63.16/63.17 [520]P6(a15,a7,a281,a3)
% 63.16/63.17 [521]P6(a15,a7,a281,a92)
% 63.16/63.17 [522]P6(a15,a7,a280,a92)
% 63.16/63.17 [523]P6(a15,a14,a281,a3)
% 63.16/63.17 [524]P6(a15,a18,a280,a92)
% 63.16/63.17 [525]P6(a15,a19,a281,a3)
% 63.16/63.17 [526]P6(a15,a19,a281,a92)
% 63.16/63.17 [527]P6(a15,a19,a280,a92)
% 63.16/63.17 [528]P6(a15,a17,a281,a3)
% 63.16/63.17 [529]P6(a15,a17,a281,a92)
% 63.16/63.17 [530]P6(a15,a17,a280,a22)
% 63.16/63.17 [531]P6(a15,a17,a280,a92)
% 63.16/63.17 [532]P6(a18,a7,a11,a81)
% 63.16/63.17 [533]P6(a18,a7,a11,a92)
% 63.16/63.17 [534]P6(a18,a7,a280,a92)
% 63.16/63.17 [535]P6(a18,a14,a280,a2)
% 63.16/63.17 [536]P6(a18,a15,a12,a2)
% 63.16/63.17 [537]P6(a18,a15,a12,a81)
% 63.16/63.17 [538]P6(a18,a15,a12,a92)
% 63.16/63.17 [539]P6(a18,a15,a280,a92)
% 63.16/63.17 [540]P6(a18,a19,a280,a92)
% 63.16/63.17 [541]P6(a18,a17,a280,a92)
% 63.16/63.17 [542]P6(a19,a7,a11,a81)
% 63.16/63.17 [543]P6(a19,a7,a11,a92)
% 63.16/63.17 [544]P6(a19,a7,a281,a92)
% 63.16/63.17 [545]P6(a19,a7,a280,a92)
% 63.16/63.17 [546]P6(a19,a14,a281,a2)
% 63.16/63.17 [547]P6(a19,a14,a280,a2)
% 63.16/63.17 [548]P6(a19,a15,a281,a92)
% 63.16/63.17 [549]P6(a19,a15,a12,a81)
% 63.16/63.17 [550]P6(a19,a15,a12,a92)
% 63.16/63.17 [551]P6(a19,a15,a280,a92)
% 63.16/63.17 [552]P6(a19,a18,a280,a92)
% 63.16/63.17 [553]P6(a19,a17,a281,a92)
% 63.16/63.17 [554]P6(a19,a17,a280,a92)
% 63.16/63.17 [555]P6(a16,a5,a12,a92)
% 63.16/63.17 [556]P6(a16,a5,a280,a92)
% 63.16/63.17 [557]P6(a16,a6,a281,a92)
% 63.16/63.17 [558]P6(a16,a6,a12,a92)
% 63.16/63.17 [559]P6(a16,a279,a281,a81)
% 63.16/63.17 [560]P6(a16,a279,a281,a92)
% 63.16/63.17 [561]P6(a17,a7,a11,a81)
% 63.16/63.17 [562]P6(a17,a7,a11,a92)
% 63.16/63.17 [563]P6(a17,a7,a281,a92)
% 63.16/63.17 [564]P6(a17,a7,a280,a92)
% 63.16/63.17 [565]P6(a17,a14,a281,a2)
% 63.16/63.17 [566]P6(a17,a15,a281,a92)
% 63.16/63.17 [567]P6(a17,a15,a12,a2)
% 63.16/63.17 [568]P6(a17,a15,a12,a81)
% 63.16/63.17 [569]P6(a17,a15,a12,a92)
% 63.16/63.17 [570]P6(a17,a15,a280,a92)
% 63.16/63.17 [571]P6(a17,a18,a280,a92)
% 63.16/63.17 [572]P6(a17,a19,a281,a2)
% 63.16/63.17 [573]P6(a17,a19,a281,a81)
% 63.16/63.17 [574]P6(a17,a19,a281,a92)
% 63.16/63.17 [575]P6(a17,a19,a280,a92)
% 63.16/63.17 [576]P6(a10,a5,a11,a81)
% 63.16/63.17 [577]P6(a10,a5,a11,a92)
% 63.16/63.17 [578]P6(a10,a5,a12,a92)
% 63.16/63.17 [579]P6(a10,a5,a280,a92)
% 63.16/63.17 [580]P6(a10,a6,a11,a92)
% 63.16/63.17 [581]P6(a10,a6,a281,a92)
% 63.16/63.17 [582]P6(a10,a6,a12,a92)
% 63.16/63.17 [583]P6(a10,a13,a11,a92)
% 63.16/63.17 [584]P6(a279,a5,a11,a81)
% 63.16/63.17 [585]P6(a279,a5,a11,a92)
% 63.16/63.17 [586]P6(a279,a5,a12,a92)
% 63.16/63.17 [587]P6(a279,a5,a280,a92)
% 63.16/63.17 [588]P6(a279,a6,a11,a92)
% 63.16/63.17 [589]P6(a279,a6,a281,a92)
% 63.16/63.17 [590]P6(a279,a6,a12,a92)
% 63.16/63.18 [591]P6(a279,a13,a11,a92)
% 63.16/63.18 [592]~P6(a14,a7,a11,a81)
% 63.16/63.18 [593]~P6(a14,a7,a11,a92)
% 63.16/63.18 [594]~P6(a14,a7,a281,a92)
% 63.16/63.18 [595]~P6(a14,a7,a280,a92)
% 63.16/63.18 [596]~P6(a14,a15,a281,a92)
% 63.16/63.18 [597]~P6(a14,a15,a12,a81)
% 63.16/63.18 [598]~P6(a14,a15,a12,a92)
% 63.16/63.18 [599]~P6(a14,a15,a280,a92)
% 63.16/63.18 [600]~P6(a14,a18,a280,a92)
% 63.16/63.18 [601]~P6(a14,a19,a281,a81)
% 63.16/63.18 [602]~P6(a14,a19,a281,a92)
% 63.16/63.18 [603]~P6(a14,a19,a280,a92)
% 63.16/63.18 [604]~P6(a14,a17,a281,a92)
% 63.16/63.18 [605]~P6(a14,a17,a280,a92)
% 63.16/63.18 [606]~P6(a18,a7,a281,a3)
% 63.16/63.18 [607]~P6(a18,a7,a281,a22)
% 63.16/63.18 [608]~P6(a18,a7,a281,a92)
% 63.16/63.18 [609]~P6(a18,a14,a281,a2)
% 63.16/63.18 [610]~P6(a18,a14,a281,a3)
% 63.16/63.18 [611]~P6(a18,a14,a281,a22)
% 63.16/63.18 [612]~P6(a18,a15,a281,a22)
% 63.16/63.18 [613]~P6(a18,a15,a281,a92)
% 63.16/63.18 [614]~P6(a18,a19,a281,a2)
% 63.16/63.18 [615]~P6(a18,a19,a281,a3)
% 63.16/63.18 [616]~P6(a18,a19,a281,a22)
% 63.16/63.18 [617]~P6(a18,a19,a281,a81)
% 63.16/63.18 [618]~P6(a18,a19,a281,a92)
% 63.16/63.18 [619]~P6(a18,a17,a281,a3)
% 63.16/63.18 [620]~P6(a18,a17,a281,a22)
% 63.16/63.18 [621]~P6(a18,a17,a281,a92)
% 63.16/63.18 [622]~P6(a16,a5,a11,a22)
% 63.16/63.18 [623]~P6(a16,a5,a11,a92)
% 63.16/63.18 [624]~P6(a16,a6,a11,a22)
% 63.16/63.18 [625]~P6(a16,a6,a11,a92)
% 63.16/63.18 [626]~P6(a16,a13,a11,a22)
% 63.16/63.18 [627]~P6(a16,a13,a11,a92)
% 63.16/63.18 [628]~P6(a16,a10,a11,a22)
% 63.16/63.18 [629]~P6(a16,a279,a11,a22)
% 63.16/63.18 [630]~P6(a10,a279,a281,a22)
% 63.16/63.18 [631]~P6(a10,a279,a281,a92)
% 63.16/63.18 [44]P1(f113(a1))
% 63.16/63.18 [45]P1(f113(a2))
% 63.16/63.18 [46]P1(f113(a3))
% 63.16/63.18 [47]P1(f113(a4))
% 63.16/63.18 [48]P1(f113(a114))
% 63.16/63.18 [49]P1(f113(a115))
% 63.16/63.18 [50]P1(f113(a22))
% 63.16/63.18 [51]P1(f113(a81))
% 63.16/63.18 [52]P1(f113(a92))
% 63.16/63.18 [90]P11(f113(a1),f113(a115))
% 63.16/63.18 [91]P11(f113(a2),f113(a81))
% 63.16/63.18 [92]P11(f113(a3),f113(a2))
% 63.16/63.18 [93]P11(f113(a4),f113(a22))
% 63.16/63.18 [94]P11(f113(a115),f113(a114))
% 63.16/63.18 [95]P11(f113(a21),f113(a4))
% 63.16/63.18 [96]P11(f113(a22),f113(a3))
% 63.16/63.18 [97]P11(f113(a81),f113(a92))
% 63.16/63.18 [98]P11(f113(a92),f113(a1))
% 63.16/63.18 [99]P12(a1,f136(f113(a1)))
% 63.16/63.18 [100]P12(a2,f136(f113(a2)))
% 63.16/63.18 [101]P12(a3,f136(f113(a3)))
% 63.16/63.18 [102]P12(a4,f136(f113(a4)))
% 63.16/63.18 [103]P12(a114,f136(f113(a114)))
% 63.16/63.18 [104]P12(a115,f136(f113(a115)))
% 63.16/63.18 [105]P12(a21,f136(f113(a21)))
% 63.16/63.18 [106]P12(a22,f136(f113(a22)))
% 63.16/63.18 [107]P12(a81,f136(f113(a81)))
% 63.16/63.18 [108]P12(a92,f136(f113(a92)))
% 63.16/63.18 [109]P12(a137,f149(f113(a4)))
% 63.16/63.18 [110]P12(a150,f149(f113(a22)))
% 63.16/63.18 [111]P12(a190,f149(f113(a3)))
% 63.16/63.18 [112]P12(a201,f149(f113(a2)))
% 63.16/63.18 [113]P12(a212,f149(f113(a81)))
% 63.16/63.18 [114]P12(a223,f149(f113(a92)))
% 63.16/63.18 [115]P12(a234,f149(f113(a1)))
% 63.16/63.18 [116]P12(a245,f149(f113(a115)))
% 63.16/63.18 [117]P12(a256,f149(f113(a114)))
% 63.16/63.18 [243]P12(a103,f136(f278(f113(a81),f113(a92))))
% 63.16/63.18 [244]P12(a61,f136(f278(f113(a21),f113(a22))))
% 63.16/63.18 [245]P12(a93,f136(f278(f113(a2),f113(a81))))
% 63.16/63.18 [246]P12(a62,f136(f278(f113(a3),f113(a22))))
% 63.16/63.18 [247]P12(a71,f136(f278(f113(a21),f113(a3))))
% 63.16/63.18 [248]P12(a104,f136(f278(f113(a21),f113(a92))))
% 63.16/63.18 [249]P12(a116,f136(f278(f113(a21),f113(a1))))
% 63.16/63.18 [250]P12(a46,f136(f278(f113(a81),f113(a4))))
% 63.16/63.18 [251]P12(a24,f136(f278(f113(a21),f113(a4))))
% 63.16/63.18 [252]P12(a109,f136(f278(f113(a115),f113(a92))))
% 63.16/63.18 [253]P12(a57,f136(f278(f113(a92),f113(a4))))
% 63.16/63.18 [254]P12(a25,f136(f278(f113(a4),f113(a4))))
% 63.16/63.18 [255]P12(a47,f136(f278(f113(a3),f113(a4))))
% 63.16/63.18 [256]P12(a23,f136(f278(f113(a22),f113(a4))))
% 63.16/63.18 [257]P12(a126,f136(f278(f113(a81),f113(a115))))
% 63.16/63.18 [258]P12(a117,f136(f278(f113(a81),f113(a1))))
% 63.16/63.18 [259]P12(a65,f136(f278(f113(a2),f113(a22))))
% 63.16/63.18 [260]P12(a66,f136(f278(f113(a81),f113(a22))))
% 63.16/63.18 [261]P12(a122,f136(f278(f113(a115),f113(a1))))
% 63.16/63.18 [262]P12(a56,f136(f278(f113(a2),f113(a4))))
% 63.16/63.18 [263]P12(a58,f136(f278(f113(a1),f113(a4))))
% 63.16/63.18 [264]P12(a59,f136(f278(f113(a115),f113(a4))))
% 63.16/63.18 [265]P12(a60,f136(f278(f113(a114),f113(a4))))
% 63.16/63.18 [266]P12(a63,f136(f278(f113(a4),f113(a22))))
% 63.16/63.18 [267]P12(a64,f136(f278(f113(a22),f113(a22))))
% 63.16/63.18 [268]P12(a67,f136(f278(f113(a92),f113(a22))))
% 63.16/63.18 [269]P12(a68,f136(f278(f113(a1),f113(a22))))
% 63.16/63.18 [270]P12(a69,f136(f278(f113(a115),f113(a22))))
% 63.16/63.18 [271]P12(a70,f136(f278(f113(a114),f113(a22))))
% 63.16/63.18 [272]P12(a72,f136(f278(f113(a4),f113(a3))))
% 63.16/63.18 [273]P12(a73,f136(f278(f113(a22),f113(a3))))
% 63.16/63.18 [274]P12(a74,f136(f278(f113(a3),f113(a3))))
% 63.16/63.18 [275]P12(a75,f136(f278(f113(a2),f113(a3))))
% 63.16/63.18 [276]P12(a76,f136(f278(f113(a81),f113(a3))))
% 63.16/63.18 [277]P12(a77,f136(f278(f113(a92),f113(a3))))
% 63.16/63.18 [278]P12(a78,f136(f278(f113(a1),f113(a3))))
% 63.16/63.18 [279]P12(a79,f136(f278(f113(a115),f113(a3))))
% 63.16/63.18 [280]P12(a80,f136(f278(f113(a114),f113(a3))))
% 63.16/63.18 [281]P12(a82,f136(f278(f113(a21),f113(a2))))
% 63.16/63.18 [282]P12(a83,f136(f278(f113(a4),f113(a2))))
% 63.16/63.18 [283]P12(a84,f136(f278(f113(a22),f113(a2))))
% 63.16/63.18 [284]P12(a85,f136(f278(f113(a3),f113(a2))))
% 63.16/63.18 [285]P12(a86,f136(f278(f113(a2),f113(a2))))
% 63.16/63.18 [286]P12(a87,f136(f278(f113(a81),f113(a2))))
% 63.16/63.18 [287]P12(a88,f136(f278(f113(a92),f113(a2))))
% 63.16/63.18 [288]P12(a89,f136(f278(f113(a1),f113(a2))))
% 63.16/63.18 [289]P12(a90,f136(f278(f113(a115),f113(a2))))
% 63.16/63.18 [290]P12(a91,f136(f278(f113(a114),f113(a2))))
% 63.16/63.18 [291]P12(a94,f136(f278(f113(a21),f113(a81))))
% 63.16/63.18 [292]P12(a95,f136(f278(f113(a4),f113(a81))))
% 63.16/63.18 [293]P12(a96,f136(f278(f113(a22),f113(a81))))
% 63.16/63.18 [294]P12(a97,f136(f278(f113(a3),f113(a81))))
% 63.16/63.18 [295]P12(a98,f136(f278(f113(a81),f113(a81))))
% 63.16/63.18 [296]P12(a99,f136(f278(f113(a92),f113(a81))))
% 63.16/63.18 [297]P12(a100,f136(f278(f113(a1),f113(a81))))
% 63.16/63.18 [298]P12(a101,f136(f278(f113(a115),f113(a81))))
% 63.16/63.18 [299]P12(a102,f136(f278(f113(a114),f113(a81))))
% 63.16/63.18 [300]P12(a105,f136(f278(f113(a4),f113(a92))))
% 63.16/63.18 [301]P12(a106,f136(f278(f113(a22),f113(a92))))
% 63.16/63.18 [302]P12(a107,f136(f278(f113(a3),f113(a92))))
% 63.16/63.18 [303]P12(a108,f136(f278(f113(a2),f113(a92))))
% 63.16/63.18 [304]P12(a110,f136(f278(f113(a92),f113(a92))))
% 63.16/63.18 [305]P12(a111,f136(f278(f113(a1),f113(a92))))
% 63.16/63.18 [306]P12(a112,f136(f278(f113(a114),f113(a92))))
% 63.16/63.18 [307]P12(a118,f136(f278(f113(a4),f113(a1))))
% 63.16/63.18 [308]P12(a119,f136(f278(f113(a22),f113(a1))))
% 63.16/63.18 [309]P12(a120,f136(f278(f113(a3),f113(a1))))
% 63.16/63.18 [310]P12(a121,f136(f278(f113(a2),f113(a1))))
% 63.16/63.18 [311]P12(a123,f136(f278(f113(a92),f113(a1))))
% 63.16/63.18 [312]P12(a124,f136(f278(f113(a1),f113(a1))))
% 63.16/63.18 [313]P12(a125,f136(f278(f113(a114),f113(a1))))
% 63.16/63.18 [314]P12(a127,f136(f278(f113(a21),f113(a115))))
% 63.16/63.18 [315]P12(a128,f136(f278(f113(a4),f113(a115))))
% 63.16/63.18 [316]P12(a129,f136(f278(f113(a22),f113(a115))))
% 63.16/63.18 [317]P12(a130,f136(f278(f113(a3),f113(a115))))
% 63.16/63.18 [318]P12(a131,f136(f278(f113(a2),f113(a115))))
% 63.16/63.18 [319]P12(a132,f136(f278(f113(a92),f113(a115))))
% 63.16/63.18 [320]P12(a133,f136(f278(f113(a1),f113(a115))))
% 63.16/63.18 [321]P12(a134,f136(f278(f113(a115),f113(a115))))
% 63.16/63.18 [322]P12(a135,f136(f278(f113(a114),f113(a115))))
% 63.16/63.18 [323]P12(a139,f136(f278(f113(a21),f113(a114))))
% 63.16/63.18 [324]P12(a140,f136(f278(f113(a4),f113(a114))))
% 63.16/63.18 [325]P12(a141,f136(f278(f113(a22),f113(a114))))
% 63.16/63.18 [326]P12(a142,f136(f278(f113(a3),f113(a114))))
% 63.16/63.18 [327]P12(a143,f136(f278(f113(a2),f113(a114))))
% 63.16/63.18 [328]P12(a144,f136(f278(f113(a81),f113(a114))))
% 63.16/63.18 [329]P12(a145,f136(f278(f113(a92),f113(a114))))
% 63.16/63.18 [330]P12(a146,f136(f278(f113(a1),f113(a114))))
% 63.16/63.18 [331]P12(a147,f136(f278(f113(a115),f113(a114))))
% 63.16/63.18 [332]P12(a148,f136(f278(f113(a114),f113(a114))))
% 63.16/63.18 [333]P12(a151,f149(f278(f113(a21),f113(a4))))
% 63.16/63.18 [334]P12(a152,f149(f278(f113(a4),f113(a4))))
% 63.16/63.18 [335]P12(a163,f149(f278(f113(a22),f113(a4))))
% 63.16/63.18 [336]P12(a174,f149(f278(f113(a3),f113(a4))))
% 63.16/63.18 [337]P12(a184,f149(f278(f113(a2),f113(a4))))
% 63.16/63.18 [338]P12(a185,f149(f278(f113(a81),f113(a4))))
% 63.16/63.18 [339]P12(a186,f149(f278(f113(a92),f113(a4))))
% 63.16/63.18 [340]P12(a187,f149(f278(f113(a1),f113(a4))))
% 63.16/63.18 [341]P12(a188,f149(f278(f113(a115),f113(a4))))
% 63.16/63.18 [342]P12(a189,f149(f278(f113(a114),f113(a4))))
% 63.16/63.18 [343]P12(a191,f149(f278(f113(a21),f113(a22))))
% 63.16/63.18 [344]P12(a192,f149(f278(f113(a4),f113(a22))))
% 63.16/63.18 [345]P12(a193,f149(f278(f113(a22),f113(a22))))
% 63.16/63.18 [346]P12(a194,f149(f278(f113(a3),f113(a22))))
% 63.16/63.18 [347]P12(a195,f149(f278(f113(a2),f113(a22))))
% 63.16/63.18 [348]P12(a196,f149(f278(f113(a81),f113(a22))))
% 63.16/63.18 [349]P12(a197,f149(f278(f113(a92),f113(a22))))
% 63.16/63.18 [350]P12(a198,f149(f278(f113(a1),f113(a22))))
% 63.16/63.18 [351]P12(a199,f149(f278(f113(a115),f113(a22))))
% 63.16/63.18 [352]P12(a200,f149(f278(f113(a114),f113(a22))))
% 63.16/63.18 [353]P12(a202,f149(f278(f113(a21),f113(a3))))
% 63.16/63.18 [354]P12(a203,f149(f278(f113(a4),f113(a3))))
% 63.16/63.18 [355]P12(a204,f149(f278(f113(a22),f113(a3))))
% 63.16/63.18 [356]P12(a205,f149(f278(f113(a3),f113(a3))))
% 63.16/63.18 [357]P12(a206,f149(f278(f113(a2),f113(a3))))
% 63.16/63.18 [358]P12(a207,f149(f278(f113(a81),f113(a3))))
% 63.16/63.18 [359]P12(a208,f149(f278(f113(a92),f113(a3))))
% 63.16/63.18 [360]P12(a209,f149(f278(f113(a1),f113(a3))))
% 63.16/63.18 [361]P12(a210,f149(f278(f113(a115),f113(a3))))
% 63.16/63.18 [362]P12(a211,f149(f278(f113(a114),f113(a3))))
% 63.16/63.18 [363]P12(a213,f149(f278(f113(a21),f113(a2))))
% 63.16/63.18 [364]P12(a214,f149(f278(f113(a4),f113(a2))))
% 63.16/63.18 [365]P12(a215,f149(f278(f113(a22),f113(a2))))
% 63.16/63.18 [366]P12(a216,f149(f278(f113(a3),f113(a2))))
% 63.16/63.18 [367]P12(a217,f149(f278(f113(a2),f113(a2))))
% 63.16/63.18 [368]P12(a218,f149(f278(f113(a81),f113(a2))))
% 63.16/63.18 [369]P12(a219,f149(f278(f113(a92),f113(a2))))
% 63.16/63.18 [370]P12(a220,f149(f278(f113(a1),f113(a2))))
% 63.16/63.18 [371]P12(a221,f149(f278(f113(a115),f113(a2))))
% 63.16/63.18 [372]P12(a222,f149(f278(f113(a114),f113(a2))))
% 63.16/63.18 [373]P12(a224,f149(f278(f113(a21),f113(a81))))
% 63.16/63.18 [374]P12(a225,f149(f278(f113(a4),f113(a81))))
% 63.16/63.18 [375]P12(a226,f149(f278(f113(a22),f113(a81))))
% 63.16/63.18 [376]P12(a227,f149(f278(f113(a3),f113(a81))))
% 63.16/63.18 [377]P12(a228,f149(f278(f113(a2),f113(a81))))
% 63.16/63.18 [378]P12(a229,f149(f278(f113(a81),f113(a81))))
% 63.16/63.18 [379]P12(a230,f149(f278(f113(a92),f113(a81))))
% 63.16/63.18 [380]P12(a231,f149(f278(f113(a1),f113(a81))))
% 63.16/63.18 [381]P12(a232,f149(f278(f113(a115),f113(a81))))
% 63.16/63.18 [382]P12(a233,f149(f278(f113(a114),f113(a81))))
% 63.16/63.18 [383]P12(a235,f149(f278(f113(a21),f113(a92))))
% 63.16/63.18 [384]P12(a236,f149(f278(f113(a4),f113(a92))))
% 63.16/63.18 [385]P12(a237,f149(f278(f113(a22),f113(a92))))
% 63.16/63.18 [386]P12(a238,f149(f278(f113(a3),f113(a92))))
% 63.16/63.18 [387]P12(a239,f149(f278(f113(a2),f113(a92))))
% 63.16/63.18 [388]P12(a240,f149(f278(f113(a81),f113(a92))))
% 63.16/63.18 [389]P12(a241,f149(f278(f113(a92),f113(a92))))
% 63.16/63.18 [390]P12(a242,f149(f278(f113(a1),f113(a92))))
% 63.16/63.18 [391]P12(a243,f149(f278(f113(a115),f113(a92))))
% 63.16/63.18 [392]P12(a244,f149(f278(f113(a114),f113(a92))))
% 63.16/63.18 [393]P12(a246,f149(f278(f113(a21),f113(a1))))
% 63.16/63.18 [394]P12(a247,f149(f278(f113(a4),f113(a1))))
% 63.16/63.18 [395]P12(a248,f149(f278(f113(a22),f113(a1))))
% 63.16/63.18 [396]P12(a249,f149(f278(f113(a3),f113(a1))))
% 63.16/63.18 [397]P12(a250,f149(f278(f113(a2),f113(a1))))
% 63.16/63.18 [398]P12(a251,f149(f278(f113(a81),f113(a1))))
% 63.16/63.18 [399]P12(a252,f149(f278(f113(a92),f113(a1))))
% 63.16/63.18 [400]P12(a253,f149(f278(f113(a1),f113(a1))))
% 63.16/63.18 [401]P12(a254,f149(f278(f113(a115),f113(a1))))
% 63.16/63.18 [402]P12(a255,f149(f278(f113(a114),f113(a1))))
% 63.16/63.18 [403]P12(a257,f149(f278(f113(a21),f113(a115))))
% 63.16/63.18 [404]P12(a258,f149(f278(f113(a4),f113(a115))))
% 63.16/63.18 [405]P12(a259,f149(f278(f113(a22),f113(a115))))
% 63.16/63.18 [406]P12(a260,f149(f278(f113(a3),f113(a115))))
% 63.16/63.18 [407]P12(a261,f149(f278(f113(a2),f113(a115))))
% 63.16/63.18 [408]P12(a262,f149(f278(f113(a81),f113(a115))))
% 63.16/63.18 [409]P12(a263,f149(f278(f113(a92),f113(a115))))
% 63.16/63.18 [410]P12(a264,f149(f278(f113(a1),f113(a115))))
% 63.16/63.18 [411]P12(a265,f149(f278(f113(a115),f113(a115))))
% 63.16/63.18 [412]P12(a266,f149(f278(f113(a114),f113(a115))))
% 63.16/63.18 [413]P12(a268,f149(f278(f113(a21),f113(a114))))
% 63.16/63.18 [414]P12(a269,f149(f278(f113(a4),f113(a114))))
% 63.16/63.18 [415]P12(a270,f149(f278(f113(a22),f113(a114))))
% 63.16/63.18 [416]P12(a271,f149(f278(f113(a3),f113(a114))))
% 63.16/63.18 [417]P12(a272,f149(f278(f113(a2),f113(a114))))
% 63.16/63.18 [418]P12(a273,f149(f278(f113(a81),f113(a114))))
% 63.16/63.18 [419]P12(a274,f149(f278(f113(a92),f113(a114))))
% 63.16/63.18 [420]P12(a275,f149(f278(f113(a1),f113(a114))))
% 63.16/63.18 [421]P12(a276,f149(f278(f113(a115),f113(a114))))
% 63.16/63.18 [422]P12(a277,f149(f278(f113(a114),f113(a114))))
% 63.16/63.18 [423]P12(a26,f136(f278(f113(a21),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [424]P12(a27,f136(f278(f113(a4),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [425]P12(a28,f136(f278(f113(a22),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [426]P12(a29,f136(f278(f113(a3),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [427]P12(a30,f136(f278(f113(a2),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [428]P12(a31,f136(f278(f113(a81),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [429]P12(a32,f136(f278(f113(a92),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [430]P12(a33,f136(f278(f113(a1),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [431]P12(a34,f136(f278(f113(a115),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [432]P12(a35,f136(f278(f113(a114),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [433]P12(a36,f136(f278(f113(a21),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [434]P12(a37,f136(f278(f113(a4),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [435]P12(a38,f136(f278(f113(a22),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [436]P12(a39,f136(f278(f113(a3),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [437]P12(a40,f136(f278(f113(a2),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [438]P12(a41,f136(f278(f113(a81),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [439]P12(a42,f136(f278(f113(a92),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [440]P12(a43,f136(f278(f113(a1),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [441]P12(a44,f136(f278(f113(a115),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [442]P12(a45,f136(f278(f113(a114),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [443]P12(a48,f136(f278(f113(a21),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [444]P12(a49,f136(f278(f113(a4),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [445]P12(a50,f136(f278(f113(a22),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [446]P12(a51,f136(f278(f113(a3),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [447]P12(a52,f136(f278(f113(a2),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [448]P12(a53,f136(f278(f113(a81),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [449]P12(a54,f136(f278(f113(a92),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [450]P12(a55,f136(f278(f113(a1),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [451]P12(a153,f149(f278(f113(a21),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [452]P12(a154,f149(f278(f113(a4),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [453]P12(a155,f149(f278(f113(a22),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [454]P12(a156,f149(f278(f113(a3),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [455]P12(a157,f149(f278(f113(a2),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [456]P12(a158,f149(f278(f113(a81),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [457]P12(a159,f149(f278(f113(a92),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [458]P12(a160,f149(f278(f113(a1),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [459]P12(a161,f149(f278(f113(a115),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [460]P12(a162,f149(f278(f113(a114),f278(f113(a21),f113(a4)))))
% 63.16/63.18 [461]P12(a164,f149(f278(f113(a21),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [462]P12(a165,f149(f278(f113(a4),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [463]P12(a166,f149(f278(f113(a22),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [464]P12(a167,f149(f278(f113(a3),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [465]P12(a168,f149(f278(f113(a2),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [466]P12(a169,f149(f278(f113(a81),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [467]P12(a170,f149(f278(f113(a92),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [468]P12(a171,f149(f278(f113(a1),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [469]P12(a172,f149(f278(f113(a115),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [470]P12(a173,f149(f278(f113(a114),f278(f113(a4),f113(a4)))))
% 63.16/63.18 [471]P12(a175,f149(f278(f113(a21),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [472]P12(a176,f149(f278(f113(a4),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [473]P12(a177,f149(f278(f113(a22),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [474]P12(a178,f149(f278(f113(a3),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [475]P12(a179,f149(f278(f113(a2),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [476]P12(a180,f149(f278(f113(a81),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [477]P12(a181,f149(f278(f113(a92),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [478]P12(a182,f149(f278(f113(a1),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [479]P12(a183,f149(f278(f113(a115),f278(f113(a22),f113(a4)))))
% 63.16/63.18 [178]P5(x1781,a8,a103)
% 63.16/63.18 [179]P5(x1791,a8,a93)
% 63.16/63.18 [181]P5(x1811,a8,a71)
% 63.16/63.18 [184]P5(x1841,a8,a116)
% 63.16/63.18 [185]P5(x1851,a8,a109)
% 63.16/63.18 [186]P5(x1861,a8,a21)
% 63.16/63.18 [187]P5(x1871,a8,a23)
% 63.16/63.18 [189]P5(x1891,a8,a117)
% 63.16/63.18 [190]P5(x1901,a8,a122)
% 63.16/63.18 [193]P5(x1931,a9,a61)
% 63.16/63.18 [194]P5(x1941,a9,a62)
% 63.16/63.18 [195]P5(x1951,a9,a3)
% 63.16/63.18 [196]P5(x1961,a9,a115)
% 63.16/63.18 [197]P5(x1971,a9,a46)
% 63.16/63.18 [198]P5(x1981,a9,a57)
% 63.16/63.18 [199]P5(x1991,a9,a47)
% 63.16/63.18 [201]P5(x2011,a9,a21)
% 63.16/63.18 [202]P5(x2021,a9,a65)
% 63.16/63.18 [203]P5(x2031,a9,a66)
% 63.16/63.18 [204]P5(x2041,a20,a103)
% 63.16/63.18 [205]P5(x2051,a20,a1)
% 63.16/63.18 [206]P5(x2061,a20,a3)
% 63.16/63.18 [210]P5(x2101,a20,a4)
% 63.16/63.18 [211]P5(x2111,a20,a115)
% 63.16/63.18 [212]P5(x2121,a20,a104)
% 63.16/63.18 [216]P5(x2161,a20,a21)
% 63.16/63.18 [217]P5(x2171,a138,a2)
% 63.16/63.18 [219]P5(x2191,a138,a4)
% 63.16/63.18 [220]P5(x2201,a138,a46)
% 63.16/63.18 [221]P5(x2211,a138,a24)
% 63.16/63.18 [222]P5(x2221,a138,a25)
% 63.16/63.18 [227]P5(x2271,a138,a21)
% 63.16/63.18 [228]P5(x2281,a138,a126)
% 63.16/63.18 [229]P5(x2291,a138,a26)
% 63.16/63.18 [232]P5(x2321,a267,a2)
% 63.16/63.18 [234]P5(x2341,a267,a4)
% 63.16/63.18 [235]P5(x2351,a267,a114)
% 63.16/63.18 [239]P5(x2391,a267,a21)
% 63.16/63.18 [241]P5(x2411,a267,a22)
% 63.16/63.18 [242]P5(x2421,a267,a81)
% 63.16/63.18 [634]P9(f113(x6341))+~P1(f113(x6341))
% 63.16/63.18 [632]~E(x6321,x6322)+P7(x6321,x6322)
% 63.16/63.18 [633]~P8(x6332,x6331)+~E(x6331,x6332)
% 63.16/63.19 [636]~P10(x6361,x6362)+P2(x6361,x6362)
% 63.16/63.19 [637]~P8(x6371,x6372)+P7(x6371,x6372)
% 63.16/63.19 [639]~P8(x6392,x6391)+~P8(x6391,x6392)
% 63.16/63.19 [640]~P9(x6402)+P9(f278(f113(x6401),x6402))
% 63.16/63.19 [644]P3(x6441,x6442)+~P13(x6441,x6442,x6443)
% 63.16/63.19 [645]P3(x6451,x6452)+~P4(x6451,x6452,x6453)
% 63.16/63.19 [648]~P3(x6481,x6482)+~P15(x6481,x6482,x6483)
% 63.16/63.19 [642]~P9(x6423)+P11(f113(x6421),f278(f113(x6422),x6423))
% 63.16/63.19 [655]P3(x6551,x6552)+~P6(x6551,x6552,x6553,x6554)
% 63.16/63.19 [656]P2(x6561,x6562)+~P6(x6561,x6563,x6564,x6562)
% 63.16/63.19 [650]~P11(x6502,x6504)+P11(f278(f113(x6501),x6502),f278(f113(x6503),x6504))
% 63.16/63.19 [635]P8(x6352,x6351)+P8(x6351,x6352)+E(x6351,x6352)
% 63.16/63.19 [638]P8(x6381,x6382)+~P7(x6381,x6382)+E(x6381,x6382)
% 63.16/63.19 [641]~P8(x6412,x6413)+P2(x6411,x6412)+~P2(x6411,x6413)
% 63.16/63.19 [651]P7(x6511,x6512)+~P8(x6511,x6513)+~P14(x6512,a4,x6513)
% 63.16/63.19 [649]P11(f113(x6491),f113(x6492))+~P11(f113(x6493),f113(x6492))+~P11(f113(x6491),f113(x6493))
% 63.16/63.19 [652]~P9(x6522)+~P11(f113(x6521),f113(x6523))+P11(f278(f113(x6521),x6522),f278(f113(x6523),x6522))
% 63.16/63.19 [653]~P5(x6531,x6532,x6534)+P5(x6531,x6532,x6533)+~P8(x6533,x6534)
% 63.16/63.19 [654]~P3(x6541,x6542)+~P2(x6541,x6544)+P6(x6541,x6542,x6543,x6544)
% 63.16/63.19 [643]P8(x6431,x6432)+~P12(x6432,f136(x6433))+~P12(x6431,f149(x6434))
% 63.16/63.19 [646]P8(x6461,x6462)+~P11(x6463,x6464)+~P12(x6462,f149(x6463))+~P12(x6461,f149(x6464))
% 63.16/63.19 [647]P8(x6471,x6472)+~P11(x6473,x6474)+~P12(x6472,f136(x6474))+~P12(x6471,f136(x6473))
% 63.16/63.19 %EqnAxiom
% 63.16/63.19 [1]E(x11,x11)
% 63.16/63.19 [2]E(x22,x21)+~E(x21,x22)
% 63.16/63.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.16/63.19 [4]~E(x41,x42)+E(f113(x41),f113(x42))
% 63.16/63.19 [5]~E(x51,x52)+E(f278(x51,x53),f278(x52,x53))
% 63.16/63.19 [6]~E(x61,x62)+E(f278(x63,x61),f278(x63,x62))
% 63.16/63.19 [7]~E(x71,x72)+E(f149(x71),f149(x72))
% 63.16/63.19 [8]~E(x81,x82)+E(f136(x81),f136(x82))
% 63.16/63.19 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 63.16/63.19 [10]P6(x102,x103,x104,x105)+~E(x101,x102)+~P6(x101,x103,x104,x105)
% 63.16/63.19 [11]P6(x113,x112,x114,x115)+~E(x111,x112)+~P6(x113,x111,x114,x115)
% 63.16/63.19 [12]P6(x123,x124,x122,x125)+~E(x121,x122)+~P6(x123,x124,x121,x125)
% 63.16/63.19 [13]P6(x133,x134,x135,x132)+~E(x131,x132)+~P6(x133,x134,x135,x131)
% 63.16/63.19 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143)
% 63.16/63.19 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151)
% 63.16/63.19 [16]P5(x162,x163,x164)+~E(x161,x162)+~P5(x161,x163,x164)
% 63.16/63.19 [17]P5(x173,x172,x174)+~E(x171,x172)+~P5(x173,x171,x174)
% 63.16/63.19 [18]P5(x183,x184,x182)+~E(x181,x182)+~P5(x183,x184,x181)
% 63.16/63.19 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193)
% 63.16/63.19 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201)
% 63.16/63.19 [21]P7(x212,x213)+~E(x211,x212)+~P7(x211,x213)
% 63.16/63.19 [22]P7(x223,x222)+~E(x221,x222)+~P7(x223,x221)
% 63.16/63.19 [23]P12(x232,x233)+~E(x231,x232)+~P12(x231,x233)
% 63.16/63.19 [24]P12(x243,x242)+~E(x241,x242)+~P12(x243,x241)
% 63.16/63.19 [25]P11(x252,x253)+~E(x251,x252)+~P11(x251,x253)
% 63.16/63.19 [26]P11(x263,x262)+~E(x261,x262)+~P11(x263,x261)
% 63.16/63.19 [27]P4(x272,x273,x274)+~E(x271,x272)+~P4(x271,x273,x274)
% 63.16/63.19 [28]P4(x283,x282,x284)+~E(x281,x282)+~P4(x283,x281,x284)
% 63.16/63.19 [29]P4(x293,x294,x292)+~E(x291,x292)+~P4(x293,x294,x291)
% 63.16/63.19 [30]P8(x302,x303)+~E(x301,x302)+~P8(x301,x303)
% 63.16/63.19 [31]P8(x313,x312)+~E(x311,x312)+~P8(x313,x311)
% 63.16/63.19 [32]~P9(x321)+P9(x322)+~E(x321,x322)
% 63.16/63.19 [33]P13(x332,x333,x334)+~E(x331,x332)+~P13(x331,x333,x334)
% 63.16/63.19 [34]P13(x343,x342,x344)+~E(x341,x342)+~P13(x343,x341,x344)
% 63.16/63.19 [35]P13(x353,x354,x352)+~E(x351,x352)+~P13(x353,x354,x351)
% 63.16/63.19 [36]P15(x362,x363,x364)+~E(x361,x362)+~P15(x361,x363,x364)
% 63.16/63.19 [37]P15(x373,x372,x374)+~E(x371,x372)+~P15(x373,x371,x374)
% 63.16/63.19 [38]P15(x383,x384,x382)+~E(x381,x382)+~P15(x383,x384,x381)
% 63.16/63.19 [39]P14(x392,x393,x394)+~E(x391,x392)+~P14(x391,x393,x394)
% 63.16/63.19 [40]P14(x403,x402,x404)+~E(x401,x402)+~P14(x403,x401,x404)
% 63.16/63.19 [41]P14(x413,x414,x412)+~E(x411,x412)+~P14(x413,x414,x411)
% 63.16/63.19 [42]P10(x422,x423)+~E(x421,x422)+~P10(x421,x423)
% 63.16/63.19 [43]P10(x433,x432)+~E(x431,x432)+~P10(x433,x431)
% 63.16/63.19
% 63.16/63.19 %-------------------------------------------
% 63.16/63.19 cnf(660,plain,
% 63.16/63.19 (~E(a6,a279)),
% 63.16/63.19 inference(scs_inference,[],[625,631,480,581,10,11])).
% 63.16/63.19 cnf(2135,plain,
% 63.16/63.19 (P8(a255,a124)),
% 63.16/63.19 inference(scs_inference,[],[402,312,643])).
% 63.16/63.19 cnf(4759,plain,
% 63.16/63.19 (P8(a201,a28)),
% 63.16/63.19 inference(scs_inference,[],[425,112,643])).
% 63.16/63.19 cnf(4782,plain,
% 63.16/63.19 (~P3(a18,a279)),
% 63.16/63.19 inference(scs_inference,[],[660,4759,176,147,118,633,637,2,644,645,648])).
% 63.16/63.19 cnf(5841,plain,
% 63.16/63.19 ($false),
% 63.16/63.19 inference(scs_inference,[],[4782,2135,162,637,645]),
% 63.16/63.19 ['proof']).
% 63.16/63.19 % SZS output end Proof
% 63.16/63.19 % Total time :62.450000s
%------------------------------------------------------------------------------