%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : AGT014+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 : n032.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:19 EDT 2024
% Result : Theorem 0.45s 0.59s
% Output : CNFRefutation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.09 % Problem : AGT014+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.08/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.29 % Computer : n032.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Wed Jun 19 04:11:23 EDT 2024
% 0.08/0.29 % CPUTime :
% 0.14/0.46 start to proof:theBenchmark
% 0.45/0.58 %-------------------------------------------
% 0.45/0.58 % File :CSE---1.7
% 0.45/0.58 % Problem :theBenchmark
% 0.45/0.58 % Transform :cnf
% 0.45/0.58 % Format :tptp:raw
% 0.45/0.58 % Command :java -jar mcs_scs.jar %d %s
% 0.45/0.58
% 0.45/0.58 % Result :Theorem 0.010000s
% 0.45/0.58 % Output :CNFRefutation 0.010000s
% 0.45/0.58 %-------------------------------------------
% 0.45/0.59 %--------------------------------------------------------------------------
% 0.45/0.59 % File : AGT014+2 : TPTP v8.2.0. Bugfixed v3.1.0.
% 0.45/0.59 % Domain : Agents
% 0.45/0.59 % Problem : Problem for the CPlanT system
% 0.45/0.59 % Version : [Bar03] axioms : Especial.
% 0.45/0.59 % English :
% 0.45/0.59
% 0.45/0.59 % Refs : [Bar03] Barta, J. (2003), Email to G. Sutcliffe
% 0.45/0.59 % : [BT+03] Barta et al. (2003), Meta-Reasoning in CPlanT Multi-Ag
% 0.45/0.59 % : [TBP03] Tozicka et al. (2003), Meta-reasoning for Agents' Priv
% 0.45/0.59 % Source : [Bar03]
% 0.45/0.59 % Names :
% 0.45/0.59
% 0.45/0.59 % Status : Theorem
% 0.45/0.59 % Rating : 0.11 v7.5.0, 0.12 v7.4.0, 0.17 .0, 0.22 v7.0.0, 0.17 v6.4.0, 0.15 v6.3.0, 0.25 v6.2.0, 0.24 .0, 0.23 v6.0.0, 0.22 v5.5.0, 0.30 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.15 .0, 0.19 v5.0.0, 0.21 .0, 0.22 v4.0.0, 0.21 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0, 0.21 v3.2.0, 0.27 .0
% 0.45/0.59 % Syntax : Number of formulae : 923 ( 891 unt; 0 def)
% 0.45/0.59 % Number of atoms : 1023 ( 2 equ)
% 0.45/0.59 % Maximal formula atoms : 6 ( 1 avg)
% 0.45/0.59 % Number of connectives : 149 ( 49 ~; 1 |; 67 &)
% 0.45/0.59 % ( 16 <=>; 16 =>; 0 <=; 0 <~>)
% 0.45/0.59 % Maximal formula depth : 8 ( 1 avg)
% 0.45/0.59 % Maximal term depth : 5 ( 2 avg)
% 0.45/0.59 % Number of predicates : 17 ( 16 usr; 0 prp; 1-4 aty)
% 0.45/0.59 % Number of functors : 290 ( 290 usr; 286 con; 0-2 aty)
% 0.45/0.59 % Number of variables : 73 ( 70 !; 3 ?)
% 0.45/0.59 % SPC : FOF_THM_RFO_SEQ
% 0.45/0.59
% 0.45/0.59 % Comments :
% 0.45/0.59 % Bugfixes : v3.0.0 - Bugfixes in NUM005+1.ax
% 0.45/0.59 % : v3.1.0 - Changes to NUM005 axioms
% 0.45/0.59 %--------------------------------------------------------------------------
% 0.45/0.59 %----Include axioms of CPlanT
% 0.45/0.59 include('Axioms/AGT001+0.ax').
% 0.45/0.59 %----Include events of CPlanT
% 0.45/0.59 include('Axioms/AGT001+1.ax').
% 0.45/0.59 %----Include lemmas of CPlanT
% 0.45/0.59 include('Axioms/AGT001+2.ax').
% 0.45/0.59 %----Include axioms for RDN and RDN less
% 0.45/0.59 include('Axioms/NUM005+0.ax').
% 0.45/0.59 include('Axioms/NUM005+1.ax').
% 0.45/0.59 %--------------------------------------------------------------------------
% 0.45/0.59 fof(query_14,conjecture,
% 0.45/0.59 ? [X,Y,Z] : ~ accept_population(X,Y,Z) ).
% 0.45/0.59
% 0.45/0.59 %--------------------------------------------------------------------------
% 0.45/0.59 %-------------------------------------------
% 0.45/0.59 % Proof found
% 0.45/0.59 % SZS status Theorem for theBenchmark
% 0.45/0.59 % SZS output start Proof
% 0.45/0.59 %ClaNum:800(EqnAxiom:42)
% 0.45/0.59 %VarNum:157(SingletonVarNum:89)
% 0.45/0.59 %MaxLitNum:4
% 0.45/0.59 %MaxfuncDepth:4
% 0.45/0.59 %SharedTerms:1226
% 0.45/0.59 %goalClause: 280 281 282 283 284 285 286 287 288 289 290 291 292
% 0.45/0.59 %singleGoalClaCount:13
% 0.45/0.59 [94]P3(a5,a13)
% 0.45/0.59 [95]P3(a5,a14)
% 0.45/0.59 [96]P3(a5,a8)
% 0.45/0.59 [97]P3(a5,a16)
% 0.45/0.59 [98]P3(a5,a17)
% 0.45/0.59 [99]P3(a5,a279)
% 0.45/0.59 [100]P3(a13,a5)
% 0.45/0.59 [101]P3(a13,a14)
% 0.45/0.59 [102]P3(a13,a8)
% 0.45/0.59 [103]P3(a13,a16)
% 0.45/0.59 [104]P3(a13,a17)
% 0.45/0.59 [105]P3(a13,a279)
% 0.45/0.59 [106]P3(a14,a5)
% 0.45/0.59 [107]P3(a14,a13)
% 0.45/0.59 [108]P3(a14,a8)
% 0.45/0.59 [109]P3(a14,a16)
% 0.45/0.59 [110]P3(a14,a17)
% 0.45/0.59 [111]P3(a14,a279)
% 0.45/0.59 [112]P3(a8,a5)
% 0.45/0.59 [113]P3(a8,a13)
% 0.45/0.59 [114]P3(a8,a15)
% 0.45/0.59 [115]P3(a8,a16)
% 0.45/0.59 [116]P3(a8,a19)
% 0.45/0.59 [117]P3(a8,a20)
% 0.45/0.59 [118]P3(a8,a18)
% 0.45/0.59 [119]P3(a8,a279)
% 0.45/0.59 [120]P3(a15,a5)
% 0.45/0.59 [121]P3(a15,a13)
% 0.45/0.59 [122]P3(a15,a16)
% 0.45/0.59 [123]P3(a15,a279)
% 0.45/0.59 [124]P3(a16,a5)
% 0.45/0.59 [125]P3(a16,a13)
% 0.45/0.59 [126]P3(a16,a8)
% 0.45/0.59 [127]P3(a16,a15)
% 0.45/0.59 [128]P3(a16,a19)
% 0.45/0.59 [129]P3(a16,a20)
% 0.45/0.59 [130]P3(a16,a18)
% 0.45/0.59 [131]P3(a16,a279)
% 0.45/0.59 [132]P3(a19,a5)
% 0.45/0.59 [133]P3(a19,a13)
% 0.45/0.59 [134]P3(a19,a8)
% 0.45/0.59 [135]P3(a19,a15)
% 0.45/0.59 [136]P3(a19,a16)
% 0.45/0.59 [137]P3(a19,a20)
% 0.45/0.59 [138]P3(a19,a18)
% 0.45/0.59 [139]P3(a19,a279)
% 0.45/0.59 [140]P3(a20,a5)
% 0.45/0.59 [141]P3(a20,a13)
% 0.45/0.59 [142]P3(a20,a8)
% 0.45/0.59 [143]P3(a20,a15)
% 0.45/0.59 [144]P3(a20,a16)
% 0.45/0.59 [145]P3(a20,a19)
% 0.45/0.59 [146]P3(a20,a18)
% 0.45/0.59 [147]P3(a20,a279)
% 0.45/0.59 [148]P3(a17,a5)
% 0.45/0.59 [149]P3(a17,a13)
% 0.45/0.59 [150]P3(a17,a8)
% 0.45/0.59 [151]P3(a17,a16)
% 0.45/0.59 [152]P3(a17,a279)
% 0.45/0.59 [153]P3(a18,a5)
% 0.45/0.59 [154]P3(a18,a13)
% 0.45/0.59 [155]P3(a18,a8)
% 0.45/0.59 [156]P3(a18,a15)
% 0.45/0.59 [157]P3(a18,a16)
% 0.45/0.59 [158]P3(a18,a19)
% 0.45/0.59 [159]P3(a18,a20)
% 0.45/0.59 [160]P3(a18,a279)
% 0.45/0.59 [161]P3(a11,a5)
% 0.45/0.59 [162]P3(a11,a13)
% 0.45/0.59 [163]P3(a11,a14)
% 0.45/0.59 [164]P3(a11,a8)
% 0.45/0.59 [165]P3(a11,a16)
% 0.45/0.59 [166]P3(a11,a17)
% 0.45/0.59 [167]P3(a279,a5)
% 0.45/0.59 [168]P3(a279,a13)
% 0.45/0.59 [169]P3(a279,a14)
% 0.45/0.59 [170]P3(a279,a8)
% 0.45/0.59 [171]P3(a279,a16)
% 0.45/0.59 [172]P3(a279,a17)
% 0.45/0.59 [173]P4(a5,a2)
% 0.45/0.59 [174]P4(a5,a3)
% 0.45/0.59 [175]P4(a5,a4)
% 0.45/0.59 [177]P4(a5,a22)
% 0.45/0.59 [179]P4(a5,a81)
% 0.45/0.59 [181]P4(a5,a92)
% 0.45/0.59 [182]P4(a13,a2)
% 0.45/0.59 [183]P4(a13,a3)
% 0.45/0.59 [184]P4(a13,a4)
% 0.45/0.59 [186]P4(a13,a22)
% 0.45/0.59 [187]P4(a13,a81)
% 0.45/0.59 [189]P4(a13,a92)
% 0.45/0.59 [190]P4(a14,a2)
% 0.45/0.59 [191]P4(a14,a3)
% 0.45/0.59 [192]P4(a14,a4)
% 0.45/0.59 [194]P4(a14,a22)
% 0.45/0.59 [195]P4(a14,a81)
% 0.45/0.59 [197]P4(a14,a92)
% 0.45/0.59 [198]P4(a8,a2)
% 0.45/0.59 [200]P4(a8,a3)
% 0.45/0.59 [201]P4(a8,a4)
% 0.45/0.59 [203]P4(a8,a22)
% 0.45/0.59 [205]P4(a8,a81)
% 0.45/0.59 [207]P4(a8,a92)
% 0.45/0.59 [209]P4(a15,a2)
% 0.45/0.59 [211]P4(a15,a3)
% 0.45/0.59 [212]P4(a15,a4)
% 0.45/0.59 [214]P4(a15,a22)
% 0.45/0.59 [216]P4(a16,a2)
% 0.45/0.59 [217]P4(a16,a3)
% 0.45/0.59 [219]P4(a16,a4)
% 0.45/0.59 [221]P4(a16,a22)
% 0.45/0.59 [223]P4(a16,a81)
% 0.45/0.59 [225]P4(a16,a92)
% 0.45/0.59 [226]P4(a19,a2)
% 0.45/0.59 [228]P4(a19,a3)
% 0.45/0.59 [229]P4(a19,a4)
% 0.45/0.59 [231]P4(a19,a22)
% 0.45/0.59 [232]P4(a19,a81)
% 0.45/0.59 [234]P4(a19,a92)
% 0.45/0.59 [236]P4(a20,a2)
% 0.45/0.59 [238]P4(a20,a3)
% 0.45/0.59 [239]P4(a20,a4)
% 0.45/0.59 [241]P4(a20,a22)
% 0.45/0.59 [243]P4(a20,a81)
% 0.45/0.59 [245]P4(a20,a92)
% 0.45/0.59 [246]P4(a17,a2)
% 0.45/0.59 [247]P4(a17,a3)
% 0.45/0.59 [248]P4(a17,a4)
% 0.45/0.59 [249]P4(a17,a22)
% 0.45/0.59 [250]P4(a17,a81)
% 0.45/0.59 [252]P4(a17,a92)
% 0.45/0.59 [253]P4(a18,a2)
% 0.45/0.59 [255]P4(a18,a3)
% 0.45/0.59 [256]P4(a18,a4)
% 0.45/0.59 [258]P4(a18,a22)
% 0.45/0.59 [260]P4(a18,a81)
% 0.45/0.59 [262]P4(a18,a92)
% 0.45/0.59 [263]P4(a11,a2)
% 0.45/0.59 [264]P4(a11,a3)
% 0.45/0.59 [265]P4(a11,a4)
% 0.45/0.59 [267]P4(a11,a22)
% 0.45/0.59 [268]P4(a11,a81)
% 0.45/0.59 [270]P4(a11,a92)
% 0.45/0.59 [271]P4(a279,a2)
% 0.45/0.59 [272]P4(a279,a3)
% 0.45/0.59 [273]P4(a279,a4)
% 0.45/0.59 [275]P4(a279,a22)
% 0.45/0.59 [277]P4(a279,a81)
% 0.45/0.59 [279]P4(a279,a92)
% 0.45/0.59 [321]P13(a5,a8,a6)
% 0.45/0.59 [322]P13(a5,a16,a7)
% 0.45/0.59 [323]P13(a13,a8,a6)
% 0.45/0.59 [324]P13(a13,a16,a7)
% 0.45/0.60 [325]P13(a14,a8,a6)
% 0.45/0.60 [326]P13(a14,a16,a7)
% 0.45/0.60 [327]P13(a8,a5,a284)
% 0.45/0.60 [328]P13(a8,a13,a278)
% 0.45/0.60 [329]P13(a8,a279,a278)
% 0.45/0.60 [330]P13(a15,a5,a284)
% 0.45/0.60 [331]P13(a15,a13,a278)
% 0.45/0.60 [332]P13(a15,a279,a278)
% 0.45/0.60 [333]P13(a16,a5,a284)
% 0.45/0.60 [334]P13(a16,a13,a278)
% 0.45/0.60 [335]P13(a16,a279,a278)
% 0.45/0.60 [336]P13(a19,a5,a284)
% 0.45/0.60 [337]P13(a20,a5,a284)
% 0.45/0.60 [338]P13(a20,a13,a278)
% 0.45/0.60 [339]P13(a20,a279,a278)
% 0.45/0.60 [340]P13(a17,a16,a7)
% 0.45/0.60 [341]P13(a18,a5,a284)
% 0.45/0.60 [342]P13(a18,a13,a278)
% 0.45/0.60 [343]P13(a18,a279,a278)
% 0.45/0.60 [344]P13(a11,a8,a6)
% 0.45/0.60 [345]P13(a11,a16,a7)
% 0.45/0.60 [346]P13(a279,a8,a6)
% 0.45/0.60 [347]P13(a279,a16,a7)
% 0.45/0.60 [348]P5(a5,a8,a6)
% 0.45/0.60 [349]P5(a5,a16,a7)
% 0.45/0.60 [350]P5(a13,a8,a6)
% 0.45/0.60 [351]P5(a13,a16,a7)
% 0.45/0.60 [352]P5(a14,a8,a6)
% 0.45/0.60 [353]P5(a14,a16,a7)
% 0.45/0.60 [354]P5(a8,a5,a284)
% 0.45/0.60 [355]P5(a8,a13,a278)
% 0.45/0.60 [356]P5(a8,a279,a278)
% 0.45/0.60 [357]P5(a15,a5,a284)
% 0.45/0.60 [358]P5(a15,a13,a278)
% 0.45/0.60 [359]P5(a15,a279,a278)
% 0.45/0.60 [360]P5(a16,a5,a284)
% 0.45/0.60 [361]P5(a16,a13,a278)
% 0.45/0.60 [362]P5(a16,a279,a278)
% 0.45/0.60 [363]P5(a19,a5,a284)
% 0.45/0.60 [364]P5(a19,a13,a278)
% 0.45/0.60 [365]P5(a19,a279,a278)
% 0.45/0.60 [366]P5(a20,a5,a284)
% 0.45/0.60 [367]P5(a20,a13,a278)
% 0.45/0.60 [368]P5(a20,a279,a278)
% 0.45/0.60 [369]P5(a17,a8,a6)
% 0.45/0.60 [370]P5(a17,a16,a7)
% 0.45/0.60 [371]P5(a18,a5,a284)
% 0.45/0.60 [372]P5(a18,a13,a278)
% 0.45/0.60 [373]P5(a18,a279,a278)
% 0.45/0.60 [374]P5(a11,a8,a6)
% 0.45/0.60 [375]P5(a11,a16,a7)
% 0.45/0.60 [376]P5(a279,a8,a6)
% 0.45/0.60 [377]P5(a279,a16,a7)
% 0.45/0.60 [378]P15(a19,a13,a278)
% 0.45/0.60 [379]P15(a19,a279,a278)
% 0.45/0.60 [380]P15(a17,a8,a6)
% 0.45/0.60 [618]P6(a5,a13,a6,a92)
% 0.45/0.60 [619]P6(a5,a13,a278,a92)
% 0.45/0.60 [620]P6(a5,a13,a7,a92)
% 0.45/0.60 [621]P6(a5,a14,a6,a92)
% 0.45/0.60 [622]P6(a5,a279,a278,a81)
% 0.45/0.60 [623]P6(a5,a279,a278,a92)
% 0.45/0.60 [624]P6(a13,a5,a6,a81)
% 0.45/0.60 [625]P6(a13,a5,a6,a92)
% 0.45/0.60 [626]P6(a13,a5,a7,a92)
% 0.45/0.60 [627]P6(a13,a5,a284,a92)
% 0.45/0.60 [628]P6(a13,a14,a6,a92)
% 0.45/0.60 [629]P6(a13,a279,a278,a81)
% 0.45/0.60 [630]P6(a13,a279,a278,a92)
% 0.45/0.60 [631]P6(a14,a5,a6,a81)
% 0.45/0.60 [632]P6(a14,a5,a6,a92)
% 0.45/0.60 [633]P6(a14,a5,a7,a92)
% 0.45/0.60 [634]P6(a14,a5,a284,a92)
% 0.45/0.60 [635]P6(a14,a13,a6,a92)
% 0.45/0.60 [636]P6(a14,a13,a278,a92)
% 0.45/0.60 [637]P6(a14,a13,a7,a92)
% 0.45/0.60 [638]P6(a14,a279,a278,a81)
% 0.45/0.60 [639]P6(a14,a279,a278,a92)
% 0.45/0.60 [640]P6(a8,a15,a278,a2)
% 0.45/0.60 [641]P6(a8,a15,a284,a2)
% 0.45/0.60 [642]P6(a8,a16,a278,a92)
% 0.45/0.60 [643]P6(a8,a16,a7,a2)
% 0.45/0.60 [644]P6(a8,a16,a7,a81)
% 0.45/0.60 [645]P6(a8,a16,a7,a92)
% 0.45/0.60 [646]P6(a8,a16,a284,a92)
% 0.45/0.60 [647]P6(a8,a19,a284,a92)
% 0.45/0.60 [648]P6(a8,a20,a278,a2)
% 0.45/0.60 [649]P6(a8,a20,a278,a81)
% 0.45/0.60 [650]P6(a8,a20,a278,a92)
% 0.45/0.60 [651]P6(a8,a20,a284,a92)
% 0.45/0.60 [652]P6(a8,a18,a278,a92)
% 0.45/0.60 [653]P6(a8,a18,a284,a92)
% 0.45/0.60 [654]P6(a15,a16,a7,a22)
% 0.45/0.60 [655]P6(a15,a20,a278,a2)
% 0.45/0.60 [656]P6(a16,a8,a6,a81)
% 0.45/0.60 [657]P6(a16,a8,a6,a92)
% 0.45/0.60 [658]P6(a16,a8,a278,a3)
% 0.45/0.60 [659]P6(a16,a8,a278,a92)
% 0.45/0.60 [660]P6(a16,a8,a284,a92)
% 0.45/0.60 [661]P6(a16,a15,a278,a3)
% 0.45/0.60 [662]P6(a16,a19,a284,a92)
% 0.45/0.60 [663]P6(a16,a20,a278,a3)
% 0.45/0.60 [664]P6(a16,a20,a278,a92)
% 0.45/0.60 [665]P6(a16,a20,a284,a92)
% 0.45/0.60 [666]P6(a16,a18,a278,a3)
% 0.45/0.60 [667]P6(a16,a18,a278,a92)
% 0.45/0.60 [668]P6(a16,a18,a284,a22)
% 0.45/0.60 [669]P6(a16,a18,a284,a92)
% 0.45/0.60 [670]P6(a19,a8,a6,a81)
% 0.45/0.60 [671]P6(a19,a8,a6,a92)
% 0.45/0.60 [672]P6(a19,a8,a284,a92)
% 0.45/0.60 [673]P6(a19,a15,a284,a2)
% 0.45/0.60 [674]P6(a19,a16,a7,a2)
% 0.45/0.60 [675]P6(a19,a16,a7,a81)
% 0.45/0.60 [676]P6(a19,a16,a7,a92)
% 0.45/0.60 [677]P6(a19,a16,a284,a92)
% 0.45/0.60 [678]P6(a19,a20,a284,a92)
% 0.45/0.60 [679]P6(a19,a18,a284,a92)
% 0.45/0.60 [680]P6(a20,a8,a6,a81)
% 0.45/0.60 [681]P6(a20,a8,a6,a92)
% 0.45/0.60 [682]P6(a20,a8,a278,a92)
% 0.45/0.60 [683]P6(a20,a8,a284,a92)
% 0.45/0.60 [684]P6(a20,a15,a278,a2)
% 0.45/0.60 [685]P6(a20,a15,a284,a2)
% 0.45/0.60 [686]P6(a20,a16,a278,a92)
% 0.45/0.60 [687]P6(a20,a16,a7,a81)
% 0.45/0.60 [688]P6(a20,a16,a7,a92)
% 0.45/0.60 [689]P6(a20,a16,a284,a92)
% 0.45/0.60 [690]P6(a20,a19,a284,a92)
% 0.45/0.60 [691]P6(a20,a18,a278,a92)
% 0.45/0.60 [692]P6(a20,a18,a284,a92)
% 0.45/0.60 [693]P6(a17,a5,a7,a92)
% 0.45/0.60 [694]P6(a17,a5,a284,a92)
% 0.45/0.60 [695]P6(a17,a13,a278,a92)
% 0.45/0.60 [696]P6(a17,a13,a7,a92)
% 0.45/0.60 [697]P6(a17,a279,a278,a81)
% 0.45/0.60 [698]P6(a17,a279,a278,a92)
% 0.45/0.60 [699]P6(a18,a8,a6,a81)
% 0.45/0.60 [700]P6(a18,a8,a6,a92)
% 0.45/0.60 [701]P6(a18,a8,a278,a92)
% 0.45/0.60 [702]P6(a18,a8,a284,a92)
% 0.45/0.60 [703]P6(a18,a15,a278,a2)
% 0.45/0.60 [704]P6(a18,a16,a278,a92)
% 0.45/0.60 [705]P6(a18,a16,a7,a2)
% 0.45/0.60 [706]P6(a18,a16,a7,a81)
% 0.45/0.60 [707]P6(a18,a16,a7,a92)
% 0.45/0.60 [708]P6(a18,a16,a284,a92)
% 0.45/0.60 [709]P6(a18,a19,a284,a92)
% 0.45/0.60 [710]P6(a18,a20,a278,a2)
% 0.45/0.60 [711]P6(a18,a20,a278,a81)
% 0.45/0.60 [712]P6(a18,a20,a278,a92)
% 0.45/0.60 [713]P6(a18,a20,a284,a92)
% 0.45/0.60 [714]P6(a11,a5,a6,a81)
% 0.45/0.60 [715]P6(a11,a5,a6,a92)
% 0.45/0.60 [716]P6(a11,a5,a7,a92)
% 0.45/0.60 [717]P6(a11,a5,a284,a92)
% 0.45/0.60 [718]P6(a11,a13,a6,a92)
% 0.45/0.60 [719]P6(a11,a13,a278,a92)
% 0.45/0.60 [720]P6(a11,a13,a7,a92)
% 0.45/0.60 [721]P6(a11,a14,a6,a92)
% 0.45/0.60 [722]P6(a279,a5,a6,a81)
% 0.45/0.60 [723]P6(a279,a5,a6,a92)
% 0.45/0.60 [724]P6(a279,a5,a7,a92)
% 0.45/0.60 [725]P6(a279,a5,a284,a92)
% 0.45/0.60 [726]P6(a279,a13,a6,a92)
% 0.45/0.60 [727]P6(a279,a13,a278,a92)
% 0.45/0.60 [728]P6(a279,a13,a7,a92)
% 0.45/0.60 [729]P6(a279,a14,a6,a92)
% 0.45/0.60 [730]~P2(a19,a278)
% 0.45/0.60 [731]~P2(a17,a6)
% 0.45/0.60 [732]~P3(a11,a279)
% 0.45/0.60 [733]~P4(a15,a81)
% 0.45/0.60 [734]~P4(a15,a92)
% 0.45/0.60 [735]~P6(a15,a8,a6,a81)
% 0.45/0.60 [736]~P6(a15,a8,a6,a92)
% 0.45/0.60 [737]~P6(a15,a8,a278,a92)
% 0.45/0.60 [738]~P6(a15,a8,a284,a92)
% 0.45/0.60 [739]~P6(a15,a16,a278,a92)
% 0.45/0.60 [740]~P6(a15,a16,a7,a81)
% 0.45/0.60 [741]~P6(a15,a16,a7,a92)
% 0.45/0.60 [742]~P6(a15,a16,a284,a92)
% 0.45/0.60 [743]~P6(a15,a19,a284,a92)
% 0.45/0.60 [744]~P6(a15,a20,a278,a81)
% 0.45/0.60 [745]~P6(a15,a20,a278,a92)
% 0.45/0.60 [746]~P6(a15,a20,a284,a92)
% 0.45/0.60 [747]~P6(a15,a18,a278,a92)
% 0.45/0.60 [748]~P6(a15,a18,a284,a92)
% 0.45/0.60 [749]~P6(a19,a8,a278,a3)
% 0.45/0.60 [750]~P6(a19,a8,a278,a22)
% 0.45/0.60 [751]~P6(a19,a8,a278,a92)
% 0.45/0.60 [752]~P6(a19,a15,a278,a2)
% 0.45/0.60 [753]~P6(a19,a15,a278,a3)
% 0.45/0.60 [754]~P6(a19,a15,a278,a22)
% 0.45/0.60 [755]~P6(a19,a16,a278,a22)
% 0.45/0.60 [756]~P6(a19,a16,a278,a92)
% 0.45/0.60 [757]~P6(a19,a20,a278,a2)
% 0.45/0.60 [758]~P6(a19,a20,a278,a3)
% 0.45/0.60 [759]~P6(a19,a20,a278,a22)
% 0.45/0.60 [760]~P6(a19,a20,a278,a81)
% 0.45/0.60 [761]~P6(a19,a20,a278,a92)
% 0.45/0.60 [762]~P6(a19,a18,a278,a3)
% 0.45/0.60 [763]~P6(a19,a18,a278,a22)
% 0.45/0.60 [764]~P6(a19,a18,a278,a92)
% 0.45/0.60 [765]~P6(a17,a5,a6,a22)
% 0.45/0.60 [766]~P6(a17,a5,a6,a92)
% 0.45/0.60 [767]~P6(a17,a13,a6,a22)
% 0.45/0.60 [768]~P6(a17,a13,a6,a92)
% 0.45/0.60 [769]~P6(a17,a14,a6,a22)
% 0.45/0.60 [770]~P6(a17,a14,a6,a92)
% 0.45/0.60 [771]~P6(a17,a11,a6,a22)
% 0.45/0.60 [772]~P6(a17,a279,a6,a22)
% 0.45/0.60 [773]~P6(a11,a279,a278,a22)
% 0.45/0.60 [774]~P6(a11,a279,a278,a92)
% 0.45/0.60 [43]P1(f113(a1))
% 0.45/0.60 [44]P1(f113(a2))
% 0.45/0.60 [45]P1(f113(a3))
% 0.45/0.60 [46]P1(f113(a4))
% 0.45/0.60 [47]P1(f113(a114))
% 0.45/0.60 [48]P1(f113(a115))
% 0.45/0.60 [49]P1(f113(a22))
% 0.45/0.60 [50]P1(f113(a81))
% 0.45/0.60 [51]P1(f113(a92))
% 0.45/0.60 [293]P11(f113(a1),f113(a115))
% 0.45/0.60 [294]P11(f113(a2),f113(a81))
% 0.45/0.60 [295]P11(f113(a3),f113(a2))
% 0.45/0.60 [296]P11(f113(a4),f113(a22))
% 0.45/0.60 [297]P11(f113(a115),f113(a114))
% 0.45/0.60 [298]P11(f113(a21),f113(a4))
% 0.45/0.60 [299]P11(f113(a22),f113(a3))
% 0.45/0.60 [300]P11(f113(a81),f113(a92))
% 0.45/0.60 [301]P11(f113(a92),f113(a1))
% 0.45/0.60 [302]P12(a1,f275(f113(a1)))
% 0.45/0.60 [303]P12(a2,f275(f113(a2)))
% 0.45/0.60 [304]P12(a3,f275(f113(a3)))
% 0.45/0.60 [305]P12(a4,f275(f113(a4)))
% 0.45/0.60 [306]P12(a114,f275(f113(a114)))
% 0.45/0.60 [307]P12(a115,f275(f113(a115)))
% 0.45/0.60 [308]P12(a21,f275(f113(a21)))
% 0.45/0.60 [309]P12(a22,f275(f113(a22)))
% 0.45/0.60 [310]P12(a81,f275(f113(a81)))
% 0.45/0.60 [311]P12(a92,f275(f113(a92)))
% 0.45/0.60 [312]P12(a137,f276(f113(a4)))
% 0.45/0.60 [313]P12(a148,f276(f113(a22)))
% 0.45/0.60 [314]P12(a188,f276(f113(a3)))
% 0.45/0.60 [315]P12(a199,f276(f113(a2)))
% 0.45/0.60 [316]P12(a210,f276(f113(a81)))
% 0.45/0.60 [317]P12(a221,f276(f113(a92)))
% 0.45/0.60 [318]P12(a232,f276(f113(a1)))
% 0.45/0.60 [319]P12(a243,f276(f113(a115)))
% 0.45/0.60 [320]P12(a254,f276(f113(a114)))
% 0.45/0.60 [381]P12(a103,f275(f277(f113(a81),f113(a92))))
% 0.45/0.60 [382]P12(a61,f275(f277(f113(a21),f113(a22))))
% 0.45/0.60 [383]P12(a93,f275(f277(f113(a2),f113(a81))))
% 0.45/0.60 [384]P12(a62,f275(f277(f113(a3),f113(a22))))
% 0.45/0.60 [385]P12(a71,f275(f277(f113(a21),f113(a3))))
% 0.45/0.60 [386]P12(a104,f275(f277(f113(a21),f113(a92))))
% 0.45/0.60 [387]P12(a116,f275(f277(f113(a21),f113(a1))))
% 0.45/0.60 [388]P12(a23,f275(f277(f113(a81),f113(a4))))
% 0.45/0.60 [389]P12(a24,f275(f277(f113(a21),f113(a4))))
% 0.45/0.60 [390]P12(a109,f275(f277(f113(a115),f113(a92))))
% 0.45/0.60 [391]P12(a57,f275(f277(f113(a92),f113(a4))))
% 0.45/0.60 [392]P12(a25,f275(f277(f113(a4),f113(a4))))
% 0.45/0.60 [393]P12(a36,f275(f277(f113(a3),f113(a4))))
% 0.45/0.60 [394]P12(a37,f275(f277(f113(a22),f113(a4))))
% 0.45/0.60 [395]P12(a126,f275(f277(f113(a81),f113(a115))))
% 0.45/0.60 [396]P12(a117,f275(f277(f113(a81),f113(a1))))
% 0.45/0.60 [397]P12(a65,f275(f277(f113(a2),f113(a22))))
% 0.45/0.60 [398]P12(a66,f275(f277(f113(a81),f113(a22))))
% 0.45/0.60 [399]P12(a122,f275(f277(f113(a115),f113(a1))))
% 0.45/0.60 [400]P12(a56,f275(f277(f113(a2),f113(a4))))
% 0.45/0.60 [401]P12(a58,f275(f277(f113(a1),f113(a4))))
% 0.45/0.60 [402]P12(a59,f275(f277(f113(a115),f113(a4))))
% 0.45/0.60 [403]P12(a60,f275(f277(f113(a114),f113(a4))))
% 0.45/0.60 [404]P12(a63,f275(f277(f113(a4),f113(a22))))
% 0.45/0.60 [405]P12(a64,f275(f277(f113(a22),f113(a22))))
% 0.45/0.60 [406]P12(a67,f275(f277(f113(a92),f113(a22))))
% 0.45/0.60 [407]P12(a68,f275(f277(f113(a1),f113(a22))))
% 0.45/0.60 [408]P12(a69,f275(f277(f113(a115),f113(a22))))
% 0.45/0.60 [409]P12(a70,f275(f277(f113(a114),f113(a22))))
% 0.45/0.60 [410]P12(a72,f275(f277(f113(a4),f113(a3))))
% 0.45/0.60 [411]P12(a73,f275(f277(f113(a22),f113(a3))))
% 0.45/0.60 [412]P12(a74,f275(f277(f113(a3),f113(a3))))
% 0.45/0.60 [413]P12(a75,f275(f277(f113(a2),f113(a3))))
% 0.45/0.60 [414]P12(a76,f275(f277(f113(a81),f113(a3))))
% 0.45/0.60 [415]P12(a77,f275(f277(f113(a92),f113(a3))))
% 0.45/0.60 [416]P12(a78,f275(f277(f113(a1),f113(a3))))
% 0.45/0.60 [417]P12(a79,f275(f277(f113(a115),f113(a3))))
% 0.45/0.60 [418]P12(a80,f275(f277(f113(a114),f113(a3))))
% 0.45/0.60 [419]P12(a82,f275(f277(f113(a21),f113(a2))))
% 0.45/0.60 [420]P12(a83,f275(f277(f113(a4),f113(a2))))
% 0.45/0.60 [421]P12(a84,f275(f277(f113(a22),f113(a2))))
% 0.45/0.60 [422]P12(a85,f275(f277(f113(a3),f113(a2))))
% 0.45/0.60 [423]P12(a86,f275(f277(f113(a2),f113(a2))))
% 0.45/0.60 [424]P12(a87,f275(f277(f113(a81),f113(a2))))
% 0.45/0.60 [425]P12(a88,f275(f277(f113(a92),f113(a2))))
% 0.45/0.60 [426]P12(a89,f275(f277(f113(a1),f113(a2))))
% 0.45/0.60 [427]P12(a90,f275(f277(f113(a115),f113(a2))))
% 0.45/0.60 [428]P12(a91,f275(f277(f113(a114),f113(a2))))
% 0.45/0.60 [429]P12(a94,f275(f277(f113(a21),f113(a81))))
% 0.45/0.60 [430]P12(a95,f275(f277(f113(a4),f113(a81))))
% 0.45/0.60 [431]P12(a96,f275(f277(f113(a22),f113(a81))))
% 0.45/0.60 [432]P12(a97,f275(f277(f113(a3),f113(a81))))
% 0.45/0.60 [433]P12(a98,f275(f277(f113(a81),f113(a81))))
% 0.45/0.60 [434]P12(a99,f275(f277(f113(a92),f113(a81))))
% 0.45/0.60 [435]P12(a100,f275(f277(f113(a1),f113(a81))))
% 0.45/0.60 [436]P12(a101,f275(f277(f113(a115),f113(a81))))
% 0.45/0.60 [437]P12(a102,f275(f277(f113(a114),f113(a81))))
% 0.45/0.60 [438]P12(a105,f275(f277(f113(a4),f113(a92))))
% 0.45/0.60 [439]P12(a106,f275(f277(f113(a22),f113(a92))))
% 0.45/0.60 [440]P12(a107,f275(f277(f113(a3),f113(a92))))
% 0.45/0.60 [441]P12(a108,f275(f277(f113(a2),f113(a92))))
% 0.45/0.60 [442]P12(a110,f275(f277(f113(a92),f113(a92))))
% 0.45/0.60 [443]P12(a111,f275(f277(f113(a1),f113(a92))))
% 0.45/0.60 [444]P12(a112,f275(f277(f113(a114),f113(a92))))
% 0.45/0.60 [445]P12(a118,f275(f277(f113(a4),f113(a1))))
% 0.45/0.60 [446]P12(a119,f275(f277(f113(a22),f113(a1))))
% 0.45/0.60 [447]P12(a120,f275(f277(f113(a3),f113(a1))))
% 0.45/0.60 [448]P12(a121,f275(f277(f113(a2),f113(a1))))
% 0.45/0.60 [449]P12(a123,f275(f277(f113(a92),f113(a1))))
% 0.45/0.60 [450]P12(a124,f275(f277(f113(a1),f113(a1))))
% 0.45/0.60 [451]P12(a125,f275(f277(f113(a114),f113(a1))))
% 0.45/0.60 [452]P12(a127,f275(f277(f113(a21),f113(a115))))
% 0.45/0.60 [453]P12(a128,f275(f277(f113(a4),f113(a115))))
% 0.45/0.60 [454]P12(a129,f275(f277(f113(a22),f113(a115))))
% 0.45/0.60 [455]P12(a130,f275(f277(f113(a3),f113(a115))))
% 0.45/0.60 [456]P12(a131,f275(f277(f113(a2),f113(a115))))
% 0.45/0.60 [457]P12(a132,f275(f277(f113(a92),f113(a115))))
% 0.45/0.60 [458]P12(a133,f275(f277(f113(a1),f113(a115))))
% 0.45/0.60 [459]P12(a134,f275(f277(f113(a115),f113(a115))))
% 0.45/0.60 [460]P12(a135,f275(f277(f113(a114),f113(a115))))
% 0.45/0.60 [461]P12(a138,f275(f277(f113(a21),f113(a114))))
% 0.45/0.60 [462]P12(a139,f275(f277(f113(a4),f113(a114))))
% 0.45/0.60 [463]P12(a140,f275(f277(f113(a22),f113(a114))))
% 0.45/0.60 [464]P12(a141,f275(f277(f113(a3),f113(a114))))
% 0.45/0.60 [465]P12(a142,f275(f277(f113(a2),f113(a114))))
% 0.45/0.60 [466]P12(a143,f275(f277(f113(a81),f113(a114))))
% 0.45/0.60 [467]P12(a144,f275(f277(f113(a92),f113(a114))))
% 0.45/0.60 [468]P12(a145,f275(f277(f113(a1),f113(a114))))
% 0.45/0.60 [469]P12(a146,f275(f277(f113(a115),f113(a114))))
% 0.45/0.60 [470]P12(a147,f275(f277(f113(a114),f113(a114))))
% 0.45/0.60 [471]P12(a149,f276(f277(f113(a21),f113(a4))))
% 0.45/0.60 [472]P12(a150,f276(f277(f113(a4),f113(a4))))
% 0.45/0.60 [473]P12(a161,f276(f277(f113(a22),f113(a4))))
% 0.45/0.60 [474]P12(a172,f276(f277(f113(a3),f113(a4))))
% 0.45/0.60 [475]P12(a182,f276(f277(f113(a2),f113(a4))))
% 0.45/0.60 [476]P12(a183,f276(f277(f113(a81),f113(a4))))
% 0.45/0.60 [477]P12(a184,f276(f277(f113(a92),f113(a4))))
% 0.45/0.60 [478]P12(a185,f276(f277(f113(a1),f113(a4))))
% 0.45/0.60 [479]P12(a186,f276(f277(f113(a115),f113(a4))))
% 0.45/0.60 [480]P12(a187,f276(f277(f113(a114),f113(a4))))
% 0.45/0.60 [481]P12(a189,f276(f277(f113(a21),f113(a22))))
% 0.45/0.60 [482]P12(a190,f276(f277(f113(a4),f113(a22))))
% 0.45/0.60 [483]P12(a191,f276(f277(f113(a22),f113(a22))))
% 0.45/0.60 [484]P12(a192,f276(f277(f113(a3),f113(a22))))
% 0.45/0.60 [485]P12(a193,f276(f277(f113(a2),f113(a22))))
% 0.45/0.60 [486]P12(a194,f276(f277(f113(a81),f113(a22))))
% 0.45/0.60 [487]P12(a195,f276(f277(f113(a92),f113(a22))))
% 0.45/0.60 [488]P12(a196,f276(f277(f113(a1),f113(a22))))
% 0.45/0.60 [489]P12(a197,f276(f277(f113(a115),f113(a22))))
% 0.45/0.60 [490]P12(a198,f276(f277(f113(a114),f113(a22))))
% 0.45/0.60 [491]P12(a200,f276(f277(f113(a21),f113(a3))))
% 0.45/0.60 [492]P12(a201,f276(f277(f113(a4),f113(a3))))
% 0.45/0.60 [493]P12(a202,f276(f277(f113(a22),f113(a3))))
% 0.45/0.60 [494]P12(a203,f276(f277(f113(a3),f113(a3))))
% 0.45/0.60 [495]P12(a204,f276(f277(f113(a2),f113(a3))))
% 0.45/0.60 [496]P12(a205,f276(f277(f113(a81),f113(a3))))
% 0.45/0.60 [497]P12(a206,f276(f277(f113(a92),f113(a3))))
% 0.45/0.60 [498]P12(a207,f276(f277(f113(a1),f113(a3))))
% 0.45/0.60 [499]P12(a208,f276(f277(f113(a115),f113(a3))))
% 0.45/0.60 [500]P12(a209,f276(f277(f113(a114),f113(a3))))
% 0.45/0.60 [501]P12(a211,f276(f277(f113(a21),f113(a2))))
% 0.45/0.60 [502]P12(a212,f276(f277(f113(a4),f113(a2))))
% 0.45/0.60 [503]P12(a213,f276(f277(f113(a22),f113(a2))))
% 0.45/0.60 [504]P12(a214,f276(f277(f113(a3),f113(a2))))
% 0.45/0.60 [505]P12(a215,f276(f277(f113(a2),f113(a2))))
% 0.45/0.60 [506]P12(a216,f276(f277(f113(a81),f113(a2))))
% 0.45/0.60 [507]P12(a217,f276(f277(f113(a92),f113(a2))))
% 0.45/0.60 [508]P12(a218,f276(f277(f113(a1),f113(a2))))
% 0.45/0.60 [509]P12(a219,f276(f277(f113(a115),f113(a2))))
% 0.45/0.60 [510]P12(a220,f276(f277(f113(a114),f113(a2))))
% 0.45/0.60 [511]P12(a222,f276(f277(f113(a21),f113(a81))))
% 0.45/0.60 [512]P12(a223,f276(f277(f113(a4),f113(a81))))
% 0.45/0.60 [513]P12(a224,f276(f277(f113(a22),f113(a81))))
% 0.45/0.60 [514]P12(a225,f276(f277(f113(a3),f113(a81))))
% 0.45/0.60 [515]P12(a226,f276(f277(f113(a2),f113(a81))))
% 0.45/0.60 [516]P12(a227,f276(f277(f113(a81),f113(a81))))
% 0.45/0.60 [517]P12(a228,f276(f277(f113(a92),f113(a81))))
% 0.45/0.60 [518]P12(a229,f276(f277(f113(a1),f113(a81))))
% 0.45/0.60 [519]P12(a230,f276(f277(f113(a115),f113(a81))))
% 0.45/0.60 [520]P12(a231,f276(f277(f113(a114),f113(a81))))
% 0.45/0.60 [521]P12(a233,f276(f277(f113(a21),f113(a92))))
% 0.45/0.60 [522]P12(a234,f276(f277(f113(a4),f113(a92))))
% 0.45/0.60 [523]P12(a235,f276(f277(f113(a22),f113(a92))))
% 0.45/0.60 [524]P12(a236,f276(f277(f113(a3),f113(a92))))
% 0.45/0.60 [525]P12(a237,f276(f277(f113(a2),f113(a92))))
% 0.45/0.60 [526]P12(a238,f276(f277(f113(a81),f113(a92))))
% 0.45/0.60 [527]P12(a239,f276(f277(f113(a92),f113(a92))))
% 0.45/0.60 [528]P12(a240,f276(f277(f113(a1),f113(a92))))
% 0.45/0.60 [529]P12(a241,f276(f277(f113(a115),f113(a92))))
% 0.45/0.60 [530]P12(a242,f276(f277(f113(a114),f113(a92))))
% 0.45/0.60 [531]P12(a244,f276(f277(f113(a21),f113(a1))))
% 0.45/0.60 [532]P12(a245,f276(f277(f113(a4),f113(a1))))
% 0.45/0.60 [533]P12(a246,f276(f277(f113(a22),f113(a1))))
% 0.45/0.60 [534]P12(a247,f276(f277(f113(a3),f113(a1))))
% 0.45/0.60 [535]P12(a248,f276(f277(f113(a2),f113(a1))))
% 0.45/0.60 [536]P12(a249,f276(f277(f113(a81),f113(a1))))
% 0.45/0.60 [537]P12(a250,f276(f277(f113(a92),f113(a1))))
% 0.45/0.60 [538]P12(a251,f276(f277(f113(a1),f113(a1))))
% 0.45/0.60 [539]P12(a252,f276(f277(f113(a115),f113(a1))))
% 0.45/0.60 [540]P12(a253,f276(f277(f113(a114),f113(a1))))
% 0.45/0.60 [541]P12(a255,f276(f277(f113(a21),f113(a115))))
% 0.45/0.60 [542]P12(a256,f276(f277(f113(a4),f113(a115))))
% 0.45/0.60 [543]P12(a257,f276(f277(f113(a22),f113(a115))))
% 0.45/0.60 [544]P12(a258,f276(f277(f113(a3),f113(a115))))
% 0.45/0.60 [545]P12(a259,f276(f277(f113(a2),f113(a115))))
% 0.45/0.60 [546]P12(a260,f276(f277(f113(a81),f113(a115))))
% 0.45/0.60 [547]P12(a261,f276(f277(f113(a92),f113(a115))))
% 0.45/0.60 [548]P12(a262,f276(f277(f113(a1),f113(a115))))
% 0.45/0.60 [549]P12(a263,f276(f277(f113(a115),f113(a115))))
% 0.45/0.60 [550]P12(a264,f276(f277(f113(a114),f113(a115))))
% 0.45/0.60 [551]P12(a265,f276(f277(f113(a21),f113(a114))))
% 0.45/0.60 [552]P12(a266,f276(f277(f113(a4),f113(a114))))
% 0.45/0.60 [553]P12(a267,f276(f277(f113(a22),f113(a114))))
% 0.45/0.60 [554]P12(a268,f276(f277(f113(a3),f113(a114))))
% 0.45/0.60 [555]P12(a269,f276(f277(f113(a2),f113(a114))))
% 0.45/0.60 [556]P12(a270,f276(f277(f113(a81),f113(a114))))
% 0.45/0.60 [557]P12(a271,f276(f277(f113(a92),f113(a114))))
% 0.45/0.60 [558]P12(a272,f276(f277(f113(a1),f113(a114))))
% 0.45/0.60 [559]P12(a273,f276(f277(f113(a115),f113(a114))))
% 0.45/0.60 [560]P12(a274,f276(f277(f113(a114),f113(a114))))
% 0.45/0.60 [561]P12(a26,f275(f277(f113(a21),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [562]P12(a27,f275(f277(f113(a4),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [563]P12(a28,f275(f277(f113(a22),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [564]P12(a29,f275(f277(f113(a3),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [565]P12(a30,f275(f277(f113(a2),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [566]P12(a31,f275(f277(f113(a81),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [567]P12(a32,f275(f277(f113(a92),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [568]P12(a33,f275(f277(f113(a1),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [569]P12(a34,f275(f277(f113(a115),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [570]P12(a35,f275(f277(f113(a114),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [571]P12(a38,f275(f277(f113(a21),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [572]P12(a39,f275(f277(f113(a4),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [573]P12(a40,f275(f277(f113(a22),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [574]P12(a41,f275(f277(f113(a3),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [575]P12(a42,f275(f277(f113(a2),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [576]P12(a43,f275(f277(f113(a81),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [577]P12(a44,f275(f277(f113(a92),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [578]P12(a45,f275(f277(f113(a1),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [579]P12(a46,f275(f277(f113(a115),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [580]P12(a47,f275(f277(f113(a114),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [581]P12(a48,f275(f277(f113(a21),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [582]P12(a49,f275(f277(f113(a4),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [583]P12(a50,f275(f277(f113(a22),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [584]P12(a51,f275(f277(f113(a3),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [585]P12(a52,f275(f277(f113(a2),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [586]P12(a53,f275(f277(f113(a81),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [587]P12(a54,f275(f277(f113(a92),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [588]P12(a55,f275(f277(f113(a1),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [589]P12(a151,f276(f277(f113(a21),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [590]P12(a152,f276(f277(f113(a4),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [591]P12(a153,f276(f277(f113(a22),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [592]P12(a154,f276(f277(f113(a3),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [593]P12(a155,f276(f277(f113(a2),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [594]P12(a156,f276(f277(f113(a81),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [595]P12(a157,f276(f277(f113(a92),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [596]P12(a158,f276(f277(f113(a1),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [597]P12(a159,f276(f277(f113(a115),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [598]P12(a160,f276(f277(f113(a114),f277(f113(a21),f113(a4)))))
% 0.45/0.60 [599]P12(a162,f276(f277(f113(a21),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [600]P12(a163,f276(f277(f113(a4),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [601]P12(a164,f276(f277(f113(a22),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [602]P12(a165,f276(f277(f113(a3),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [603]P12(a166,f276(f277(f113(a2),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [604]P12(a167,f276(f277(f113(a81),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [605]P12(a168,f276(f277(f113(a92),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [606]P12(a169,f276(f277(f113(a1),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [607]P12(a170,f276(f277(f113(a115),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [608]P12(a171,f276(f277(f113(a114),f277(f113(a4),f113(a4)))))
% 0.45/0.60 [609]P12(a173,f276(f277(f113(a21),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [610]P12(a174,f276(f277(f113(a4),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [611]P12(a175,f276(f277(f113(a22),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [612]P12(a176,f276(f277(f113(a3),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [613]P12(a177,f276(f277(f113(a2),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [614]P12(a178,f276(f277(f113(a81),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [615]P12(a179,f276(f277(f113(a92),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [616]P12(a180,f276(f277(f113(a1),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [617]P12(a181,f276(f277(f113(a115),f277(f113(a22),f113(a4)))))
% 0.45/0.60 [280]P2(x2801,a281)
% 0.45/0.60 [281]P2(x2811,a9)
% 0.45/0.60 [282]P2(x2821,a282)
% 0.45/0.60 [283]P2(x2831,a10)
% 0.45/0.60 [284]P2(x2841,a280)
% 0.45/0.60 [285]P2(x2851,a136)
% 0.45/0.60 [286]P2(x2861,a6)
% 0.45/0.60 [287]P2(x2871,a283)
% 0.45/0.60 [288]P2(x2881,a278)
% 0.45/0.60 [289]P2(x2891,a12)
% 0.45/0.60 [290]P2(x2901,a285)
% 0.45/0.60 [291]P2(x2911,a7)
% 0.45/0.60 [292]P2(x2921,a284)
% 0.45/0.60 [777]P9(f113(x7771))+~P1(f113(x7771))
% 0.45/0.60 [775]~E(x7751,x7752)+P7(x7751,x7752)
% 0.45/0.60 [776]~P8(x7762,x7761)+~E(x7761,x7762)
% 0.45/0.60 [779]~P10(x7791,x7792)+P4(x7791,x7792)
% 0.45/0.60 [780]~P8(x7801,x7802)+P7(x7801,x7802)
% 0.45/0.60 [782]~P8(x7822,x7821)+~P8(x7821,x7822)
% 0.45/0.60 [783]~P9(x7832)+P9(f277(f113(x7831),x7832))
% 0.45/0.60 [787]P2(x7871,x7872)+~P13(x7871,x7873,x7872)
% 0.45/0.60 [788]P3(x7881,x7882)+~P13(x7881,x7882,x7883)
% 0.45/0.60 [789]P3(x7891,x7892)+~P5(x7891,x7892,x7893)
% 0.45/0.60 [785]~P9(x7853)+P11(f113(x7851),f277(f113(x7852),x7853))
% 0.45/0.60 [798]P2(x7981,x7982)+~P6(x7981,x7983,x7982,x7984)
% 0.45/0.60 [799]P3(x7991,x7992)+~P6(x7991,x7992,x7993,x7994)
% 0.45/0.60 [800]P4(x8001,x8002)+~P6(x8001,x8003,x8004,x8002)
% 0.45/0.60 [793]~P11(x7932,x7934)+P11(f277(f113(x7931),x7932),f277(f113(x7933),x7934))
% 0.45/0.60 [778]P8(x7782,x7781)+P8(x7781,x7782)+E(x7781,x7782)
% 0.45/0.60 [781]P8(x7811,x7812)+~P7(x7811,x7812)+E(x7811,x7812)
% 0.45/0.60 [784]~P8(x7842,x7843)+P4(x7841,x7842)+~P4(x7841,x7843)
% 0.45/0.60 [794]P7(x7941,x7942)+~P8(x7941,x7943)+~P14(x7942,a4,x7943)
% 0.45/0.60 [795]~P15(x7951,x7953,x7952)+~P2(x7951,x7952)+~P3(x7951,x7953)
% 0.45/0.60 [792]P11(f113(x7921),f113(x7922))+~P11(f113(x7923),f113(x7922))+~P11(f113(x7921),f113(x7923))
% 0.45/0.60 [796]~P9(x7962)+~P11(f113(x7961),f113(x7963))+P11(f277(f113(x7961),x7962),f277(f113(x7963),x7962))
% 0.45/0.60 [786]P8(x7861,x7862)+~P12(x7862,f275(x7863))+~P12(x7861,f276(x7864))
% 0.45/0.60 [797]~P2(x7971,x7973)+~P3(x7971,x7972)+~P4(x7971,x7974)+P6(x7971,x7972,x7973,x7974)
% 0.45/0.60 [790]P8(x7901,x7902)+~P11(x7903,x7904)+~P12(x7902,f276(x7903))+~P12(x7901,f276(x7904))
% 0.45/0.60 [791]P8(x7911,x7912)+~P11(x7913,x7914)+~P12(x7912,f275(x7914))+~P12(x7911,f275(x7913))
% 0.45/0.60 %EqnAxiom
% 0.45/0.60 [1]E(x11,x11)
% 0.45/0.60 [2]E(x22,x21)+~E(x21,x22)
% 0.45/0.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.45/0.60 [4]~E(x41,x42)+E(f113(x41),f113(x42))
% 0.45/0.60 [5]~E(x51,x52)+E(f277(x51,x53),f277(x52,x53))
% 0.45/0.60 [6]~E(x61,x62)+E(f277(x63,x61),f277(x63,x62))
% 0.45/0.60 [7]~E(x71,x72)+E(f276(x71),f276(x72))
% 0.45/0.60 [8]~E(x81,x82)+E(f275(x81),f275(x82))
% 0.45/0.60 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 0.45/0.60 [10]P6(x102,x103,x104,x105)+~E(x101,x102)+~P6(x101,x103,x104,x105)
% 0.45/0.60 [11]P6(x113,x112,x114,x115)+~E(x111,x112)+~P6(x113,x111,x114,x115)
% 0.45/0.60 [12]P6(x123,x124,x122,x125)+~E(x121,x122)+~P6(x123,x124,x121,x125)
% 0.45/0.60 [13]P6(x133,x134,x135,x132)+~E(x131,x132)+~P6(x133,x134,x135,x131)
% 0.45/0.60 [14]P4(x142,x143)+~E(x141,x142)+~P4(x141,x143)
% 0.45/0.60 [15]P4(x153,x152)+~E(x151,x152)+~P4(x153,x151)
% 0.45/0.60 [16]P11(x162,x163)+~E(x161,x162)+~P11(x161,x163)
% 0.45/0.60 [17]P11(x173,x172)+~E(x171,x172)+~P11(x173,x171)
% 0.45/0.60 [18]P3(x182,x183)+~E(x181,x182)+~P3(x181,x183)
% 0.45/0.60 [19]P3(x193,x192)+~E(x191,x192)+~P3(x193,x191)
% 0.45/0.61 [20]~P9(x201)+P9(x202)+~E(x201,x202)
% 0.45/0.61 [21]P2(x212,x213)+~E(x211,x212)+~P2(x211,x213)
% 0.45/0.61 [22]P2(x223,x222)+~E(x221,x222)+~P2(x223,x221)
% 0.45/0.61 [23]P12(x232,x233)+~E(x231,x232)+~P12(x231,x233)
% 0.45/0.61 [24]P12(x243,x242)+~E(x241,x242)+~P12(x243,x241)
% 0.45/0.61 [25]P15(x252,x253,x254)+~E(x251,x252)+~P15(x251,x253,x254)
% 0.45/0.61 [26]P15(x263,x262,x264)+~E(x261,x262)+~P15(x263,x261,x264)
% 0.45/0.61 [27]P15(x273,x274,x272)+~E(x271,x272)+~P15(x273,x274,x271)
% 0.45/0.61 [28]P7(x282,x283)+~E(x281,x282)+~P7(x281,x283)
% 0.45/0.61 [29]P7(x293,x292)+~E(x291,x292)+~P7(x293,x291)
% 0.45/0.61 [30]P8(x302,x303)+~E(x301,x302)+~P8(x301,x303)
% 0.45/0.61 [31]P8(x313,x312)+~E(x311,x312)+~P8(x313,x311)
% 0.45/0.61 [32]P5(x322,x323,x324)+~E(x321,x322)+~P5(x321,x323,x324)
% 0.45/0.61 [33]P5(x333,x332,x334)+~E(x331,x332)+~P5(x333,x331,x334)
% 0.45/0.61 [34]P5(x343,x344,x342)+~E(x341,x342)+~P5(x343,x344,x341)
% 0.45/0.61 [35]P13(x352,x353,x354)+~E(x351,x352)+~P13(x351,x353,x354)
% 0.45/0.61 [36]P13(x363,x362,x364)+~E(x361,x362)+~P13(x363,x361,x364)
% 0.45/0.61 [37]P13(x373,x374,x372)+~E(x371,x372)+~P13(x373,x374,x371)
% 0.45/0.61 [38]P10(x382,x383)+~E(x381,x382)+~P10(x381,x383)
% 0.45/0.61 [39]P10(x393,x392)+~E(x391,x392)+~P10(x393,x391)
% 0.45/0.61 [40]P14(x402,x403,x404)+~E(x401,x402)+~P14(x401,x403,x404)
% 0.45/0.61 [41]P14(x413,x412,x414)+~E(x411,x412)+~P14(x413,x411,x414)
% 0.45/0.61 [42]P14(x423,x424,x422)+~E(x421,x422)+~P14(x423,x424,x421)
% 0.45/0.61
% 0.45/0.61 %-------------------------------------------
% 0.45/0.61 cnf(803,plain,
% 0.45/0.61 ($false),
% 0.45/0.61 inference(scs_inference,[],[286,731]),
% 0.45/0.61 ['proof']).
% 0.45/0.61 % SZS output end Proof
% 0.45/0.61 % Total time :0.010000s
%------------------------------------------------------------------------------