%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM343+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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 12:23:55 EDT 2024
% Result : Theorem 0.56s 0.74s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : NUM343+1 : TPTP v8.2.0. Released v3.1.0.
% 0.11/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.34 % Computer : n020.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Sat Jun 22 22:35:54 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 0.56/0.73 %-------------------------------------------
% 0.56/0.73 % File :CSE---1.7
% 0.56/0.73 % Problem :theBenchmark
% 0.56/0.73 % Transform :cnf
% 0.56/0.73 % Format :tptp:raw
% 0.56/0.73 % Command :java -jar mcs_scs.jar %d %s
% 0.56/0.73
% 0.56/0.73 % Result :Theorem 0.020000s
% 0.56/0.73 % Output :CNFRefutation 0.020000s
% 0.56/0.73 %-------------------------------------------
% 0.56/0.73 %------------------------------------------------------------------------------
% 0.56/0.73 % File : NUM343+1 : TPTP v8.2.0. Released v3.1.0.
% 0.56/0.73 % Domain : Number Theory (RDN arithmetic)
% 0.56/0.73 % Problem : -1 < ? & ? < 1 => 21 + ? = 21
% 0.56/0.73 % Version : Especial.
% 0.56/0.73 % English :
% 0.56/0.73
% 0.56/0.73 % Refs :
% 0.56/0.73 % Source : [TPTP]
% 0.56/0.73 % Names :
% 0.56/0.73
% 0.56/0.73 % Status : Theorem
% 0.56/0.74 % Rating : 0.14 v8.2.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.17 v7.1.0, 0.13 v6.4.0, 0.12 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.23 v6.0.0, 0.30 v5.5.0, 0.22 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.15 v5.1.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0, 0.14 v3.2.0, 0.27 v3.1.0
% 0.56/0.74 % Syntax : Number of formulae : 402 ( 374 unt; 0 def)
% 0.56/0.74 % Number of atoms : 475 ( 5 equ)
% 0.56/0.74 % Maximal formula atoms : 8 ( 1 avg)
% 0.56/0.74 % Number of connectives : 75 ( 2 ~; 1 |; 44 &)
% 0.56/0.74 % ( 3 <=>; 25 =>; 0 <=; 0 <~>)
% 0.56/0.74 % Maximal formula depth : 19 ( 1 avg)
% 0.56/0.74 % Maximal term depth : 5 ( 2 avg)
% 0.56/0.74 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 0.56/0.74 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 0.56/0.74 % Number of variables : 122 ( 121 !; 1 ?)
% 0.56/0.74 % SPC : FOF_THM_RFO_SEQ
% 0.56/0.74
% 0.56/0.74 % Comments :
% 0.56/0.74 %------------------------------------------------------------------------------
% 0.56/0.74 %----Include axioms for RDN arithmetic
% 0.56/0.74 include('Axioms/NUM005+0.ax').
% 0.56/0.74 include('Axioms/NUM005+1.ax').
% 0.56/0.74 include('Axioms/NUM005+2.ax').
% 0.56/0.74 %------------------------------------------------------------------------------
% 0.56/0.74 fof(sum_something_n0_samething,conjecture,
% 0.56/0.74 ? [X] :
% 0.56/0.74 ( ( less(nn1,X)
% 0.56/0.74 & less(X,n1) )
% 0.56/0.74 => sum(n21,X,n21) ) ).
% 0.56/0.74
% 0.56/0.74 %------------------------------------------------------------------------------
% 0.56/0.74 %-------------------------------------------
% 0.56/0.74 % Proof found
% 0.56/0.74 % SZS status Theorem for theBenchmark
% 0.56/0.74 % SZS output start Proof
% 0.56/0.74 %ClaNum:441(EqnAxiom:32)
% 0.56/0.74 %VarNum:274(SingletonVarNum:135)
% 0.56/0.74 %MaxLitNum:8
% 0.56/0.74 %MaxfuncDepth:4
% 0.56/0.74 %SharedTerms:951
% 0.56/0.74 %goalClause: 42 43 409
% 0.56/0.74 %singleGoalClaCount:3
% 0.56/0.74 [33]P1(f3(a1))
% 0.56/0.74 [34]P1(f3(a4))
% 0.56/0.74 [35]P1(f3(a43))
% 0.56/0.74 [36]P1(f3(a54))
% 0.56/0.74 [37]P1(f3(a65))
% 0.56/0.74 [38]P1(f3(a76))
% 0.56/0.74 [39]P1(f3(a87))
% 0.56/0.74 [40]P1(f3(a98))
% 0.56/0.74 [41]P1(f3(a109))
% 0.56/0.74 [44]P8(f3(a2),f3(a1))
% 0.56/0.74 [45]P8(f3(a1),f3(a4))
% 0.56/0.74 [46]P8(f3(a4),f3(a43))
% 0.56/0.74 [47]P8(f3(a43),f3(a54))
% 0.56/0.74 [48]P8(f3(a54),f3(a65))
% 0.56/0.74 [49]P8(f3(a65),f3(a76))
% 0.56/0.74 [50]P8(f3(a76),f3(a87))
% 0.56/0.74 [51]P8(f3(a87),f3(a98))
% 0.56/0.74 [52]P8(f3(a98),f3(a109))
% 0.56/0.74 [309]P4(f3(a2),f3(a2),f3(a2),f3(a2))
% 0.56/0.74 [310]P4(f3(a2),f3(a1),f3(a1),f3(a2))
% 0.56/0.74 [311]P4(f3(a2),f3(a4),f3(a4),f3(a2))
% 0.56/0.74 [312]P4(f3(a2),f3(a43),f3(a43),f3(a2))
% 0.56/0.74 [313]P4(f3(a2),f3(a54),f3(a54),f3(a2))
% 0.56/0.74 [314]P4(f3(a2),f3(a65),f3(a65),f3(a2))
% 0.56/0.74 [315]P4(f3(a2),f3(a76),f3(a76),f3(a2))
% 0.56/0.74 [316]P4(f3(a2),f3(a87),f3(a87),f3(a2))
% 0.56/0.74 [317]P4(f3(a2),f3(a98),f3(a98),f3(a2))
% 0.56/0.74 [318]P4(f3(a2),f3(a109),f3(a109),f3(a2))
% 0.56/0.74 [319]P4(f3(a1),f3(a2),f3(a1),f3(a2))
% 0.56/0.74 [320]P4(f3(a1),f3(a1),f3(a4),f3(a2))
% 0.56/0.74 [321]P4(f3(a1),f3(a4),f3(a43),f3(a2))
% 0.56/0.74 [322]P4(f3(a1),f3(a43),f3(a54),f3(a2))
% 0.56/0.74 [323]P4(f3(a1),f3(a54),f3(a65),f3(a2))
% 0.56/0.74 [324]P4(f3(a1),f3(a65),f3(a76),f3(a2))
% 0.56/0.74 [325]P4(f3(a1),f3(a76),f3(a87),f3(a2))
% 0.56/0.74 [326]P4(f3(a1),f3(a87),f3(a98),f3(a2))
% 0.56/0.74 [327]P4(f3(a1),f3(a98),f3(a109),f3(a2))
% 0.56/0.74 [328]P4(f3(a1),f3(a109),f3(a2),f3(a1))
% 0.56/0.74 [329]P4(f3(a4),f3(a2),f3(a4),f3(a2))
% 0.56/0.74 [330]P4(f3(a4),f3(a1),f3(a43),f3(a2))
% 0.56/0.74 [331]P4(f3(a4),f3(a4),f3(a54),f3(a2))
% 0.56/0.74 [332]P4(f3(a4),f3(a43),f3(a65),f3(a2))
% 0.56/0.74 [333]P4(f3(a4),f3(a54),f3(a76),f3(a2))
% 0.56/0.74 [334]P4(f3(a4),f3(a65),f3(a87),f3(a2))
% 0.56/0.74 [335]P4(f3(a4),f3(a76),f3(a98),f3(a2))
% 0.56/0.74 [336]P4(f3(a4),f3(a87),f3(a109),f3(a2))
% 0.56/0.74 [337]P4(f3(a4),f3(a98),f3(a2),f3(a1))
% 0.56/0.74 [338]P4(f3(a4),f3(a109),f3(a1),f3(a1))
% 0.56/0.74 [339]P4(f3(a43),f3(a2),f3(a43),f3(a2))
% 0.56/0.74 [340]P4(f3(a43),f3(a1),f3(a54),f3(a2))
% 0.56/0.74 [341]P4(f3(a43),f3(a4),f3(a65),f3(a2))
% 0.56/0.74 [342]P4(f3(a43),f3(a43),f3(a76),f3(a2))
% 0.56/0.74 [343]P4(f3(a43),f3(a54),f3(a87),f3(a2))
% 0.56/0.74 [344]P4(f3(a43),f3(a65),f3(a98),f3(a2))
% 0.56/0.74 [345]P4(f3(a43),f3(a76),f3(a109),f3(a2))
% 0.56/0.74 [346]P4(f3(a43),f3(a87),f3(a2),f3(a1))
% 0.56/0.74 [347]P4(f3(a43),f3(a98),f3(a1),f3(a1))
% 0.56/0.74 [348]P4(f3(a43),f3(a109),f3(a4),f3(a1))
% 0.56/0.74 [349]P4(f3(a54),f3(a2),f3(a54),f3(a2))
% 0.56/0.74 [350]P4(f3(a54),f3(a1),f3(a65),f3(a2))
% 0.56/0.74 [351]P4(f3(a54),f3(a4),f3(a76),f3(a2))
% 0.56/0.74 [352]P4(f3(a54),f3(a43),f3(a87),f3(a2))
% 0.56/0.74 [353]P4(f3(a54),f3(a54),f3(a98),f3(a2))
% 0.56/0.74 [354]P4(f3(a54),f3(a65),f3(a109),f3(a2))
% 0.56/0.74 [355]P4(f3(a54),f3(a76),f3(a2),f3(a1))
% 0.56/0.74 [356]P4(f3(a54),f3(a87),f3(a1),f3(a1))
% 0.56/0.74 [357]P4(f3(a54),f3(a98),f3(a4),f3(a1))
% 0.56/0.74 [358]P4(f3(a54),f3(a109),f3(a43),f3(a1))
% 0.56/0.74 [359]P4(f3(a65),f3(a2),f3(a65),f3(a2))
% 0.56/0.74 [360]P4(f3(a65),f3(a1),f3(a76),f3(a2))
% 0.56/0.74 [361]P4(f3(a65),f3(a4),f3(a87),f3(a2))
% 0.56/0.74 [362]P4(f3(a65),f3(a43),f3(a98),f3(a2))
% 0.56/0.74 [363]P4(f3(a65),f3(a54),f3(a109),f3(a2))
% 0.56/0.74 [364]P4(f3(a65),f3(a65),f3(a2),f3(a1))
% 0.56/0.74 [365]P4(f3(a65),f3(a76),f3(a1),f3(a1))
% 0.56/0.74 [366]P4(f3(a65),f3(a87),f3(a4),f3(a1))
% 0.56/0.74 [367]P4(f3(a65),f3(a98),f3(a43),f3(a1))
% 0.56/0.74 [368]P4(f3(a65),f3(a109),f3(a54),f3(a1))
% 0.56/0.74 [369]P4(f3(a76),f3(a2),f3(a76),f3(a2))
% 0.56/0.74 [370]P4(f3(a76),f3(a1),f3(a87),f3(a2))
% 0.56/0.74 [371]P4(f3(a76),f3(a4),f3(a98),f3(a2))
% 0.56/0.74 [372]P4(f3(a76),f3(a43),f3(a109),f3(a2))
% 0.56/0.74 [373]P4(f3(a76),f3(a54),f3(a2),f3(a1))
% 0.56/0.74 [374]P4(f3(a76),f3(a65),f3(a1),f3(a1))
% 0.56/0.74 [375]P4(f3(a76),f3(a76),f3(a4),f3(a1))
% 0.56/0.74 [376]P4(f3(a76),f3(a87),f3(a43),f3(a1))
% 0.56/0.74 [377]P4(f3(a76),f3(a98),f3(a54),f3(a1))
% 0.56/0.74 [378]P4(f3(a76),f3(a109),f3(a65),f3(a1))
% 0.56/0.74 [379]P4(f3(a87),f3(a2),f3(a87),f3(a2))
% 0.56/0.74 [380]P4(f3(a87),f3(a1),f3(a98),f3(a2))
% 0.56/0.74 [381]P4(f3(a87),f3(a4),f3(a109),f3(a2))
% 0.56/0.74 [382]P4(f3(a87),f3(a43),f3(a2),f3(a1))
% 0.56/0.74 [383]P4(f3(a87),f3(a54),f3(a1),f3(a1))
% 0.56/0.74 [384]P4(f3(a87),f3(a65),f3(a4),f3(a1))
% 0.56/0.74 [385]P4(f3(a87),f3(a76),f3(a43),f3(a1))
% 0.56/0.74 [386]P4(f3(a87),f3(a87),f3(a54),f3(a1))
% 0.56/0.74 [387]P4(f3(a87),f3(a98),f3(a65),f3(a1))
% 0.56/0.74 [388]P4(f3(a87),f3(a109),f3(a76),f3(a1))
% 0.56/0.74 [389]P4(f3(a98),f3(a2),f3(a98),f3(a2))
% 0.56/0.74 [390]P4(f3(a98),f3(a1),f3(a109),f3(a2))
% 0.56/0.74 [391]P4(f3(a98),f3(a4),f3(a2),f3(a1))
% 0.56/0.74 [392]P4(f3(a98),f3(a43),f3(a1),f3(a1))
% 0.56/0.74 [393]P4(f3(a98),f3(a54),f3(a4),f3(a1))
% 0.56/0.74 [394]P4(f3(a98),f3(a65),f3(a43),f3(a1))
% 0.56/0.74 [395]P4(f3(a98),f3(a76),f3(a54),f3(a1))
% 0.56/0.74 [396]P4(f3(a98),f3(a87),f3(a65),f3(a1))
% 0.56/0.74 [397]P4(f3(a98),f3(a98),f3(a76),f3(a1))
% 0.56/0.74 [398]P4(f3(a98),f3(a109),f3(a87),f3(a1))
% 0.56/0.74 [399]P4(f3(a109),f3(a2),f3(a109),f3(a2))
% 0.56/0.74 [400]P4(f3(a109),f3(a1),f3(a2),f3(a1))
% 0.56/0.74 [401]P4(f3(a109),f3(a4),f3(a1),f3(a1))
% 0.56/0.74 [402]P4(f3(a109),f3(a43),f3(a4),f3(a1))
% 0.56/0.74 [403]P4(f3(a109),f3(a54),f3(a43),f3(a1))
% 0.56/0.74 [404]P4(f3(a109),f3(a65),f3(a54),f3(a1))
% 0.56/0.74 [405]P4(f3(a109),f3(a76),f3(a65),f3(a1))
% 0.56/0.74 [406]P4(f3(a109),f3(a87),f3(a76),f3(a1))
% 0.56/0.74 [407]P4(f3(a109),f3(a98),f3(a87),f3(a1))
% 0.56/0.74 [408]P4(f3(a109),f3(a109),f3(a98),f3(a1))
% 0.56/0.74 [53]P9(a2,f131(f3(a2)))
% 0.56/0.74 [54]P9(a1,f131(f3(a1)))
% 0.56/0.74 [55]P9(a4,f131(f3(a4)))
% 0.56/0.74 [56]P9(a43,f131(f3(a43)))
% 0.56/0.74 [57]P9(a54,f131(f3(a54)))
% 0.56/0.74 [58]P9(a65,f131(f3(a65)))
% 0.56/0.74 [59]P9(a76,f131(f3(a76)))
% 0.56/0.74 [60]P9(a87,f131(f3(a87)))
% 0.56/0.74 [61]P9(a98,f131(f3(a98)))
% 0.56/0.74 [62]P9(a109,f131(f3(a109)))
% 0.56/0.74 [63]P9(a120,f132(f3(a1)))
% 0.56/0.74 [64]P9(a133,f132(f3(a4)))
% 0.56/0.75 [65]P9(a173,f132(f3(a43)))
% 0.56/0.75 [66]P9(a184,f132(f3(a54)))
% 0.56/0.75 [67]P9(a195,f132(f3(a65)))
% 0.56/0.75 [68]P9(a206,f132(f3(a76)))
% 0.56/0.75 [69]P9(a217,f132(f3(a87)))
% 0.56/0.75 [70]P9(a228,f132(f3(a98)))
% 0.56/0.75 [71]P9(a239,f132(f3(a109)))
% 0.56/0.75 [72]P9(a5,f131(f250(f3(a2),f3(a1))))
% 0.56/0.75 [73]P9(a6,f131(f250(f3(a1),f3(a1))))
% 0.56/0.75 [74]P9(a17,f131(f250(f3(a4),f3(a1))))
% 0.56/0.75 [75]P9(a28,f131(f250(f3(a43),f3(a1))))
% 0.56/0.75 [76]P9(a37,f131(f250(f3(a54),f3(a1))))
% 0.56/0.75 [77]P9(a38,f131(f250(f3(a65),f3(a1))))
% 0.56/0.75 [78]P9(a39,f131(f250(f3(a76),f3(a1))))
% 0.56/0.75 [79]P9(a40,f131(f250(f3(a87),f3(a1))))
% 0.56/0.75 [80]P9(a41,f131(f250(f3(a98),f3(a1))))
% 0.56/0.75 [81]P9(a42,f131(f250(f3(a109),f3(a1))))
% 0.56/0.75 [82]P9(a44,f131(f250(f3(a2),f3(a4))))
% 0.56/0.75 [83]P9(a45,f131(f250(f3(a1),f3(a4))))
% 0.56/0.75 [84]P9(a46,f131(f250(f3(a4),f3(a4))))
% 0.56/0.75 [85]P9(a47,f131(f250(f3(a43),f3(a4))))
% 0.56/0.75 [86]P9(a48,f131(f250(f3(a54),f3(a4))))
% 0.56/0.75 [87]P9(a49,f131(f250(f3(a65),f3(a4))))
% 0.56/0.75 [88]P9(a50,f131(f250(f3(a76),f3(a4))))
% 0.56/0.75 [89]P9(a51,f131(f250(f3(a87),f3(a4))))
% 0.56/0.75 [90]P9(a52,f131(f250(f3(a98),f3(a4))))
% 0.56/0.75 [91]P9(a53,f131(f250(f3(a109),f3(a4))))
% 0.56/0.75 [92]P9(a55,f131(f250(f3(a2),f3(a43))))
% 0.56/0.75 [93]P9(a56,f131(f250(f3(a1),f3(a43))))
% 0.56/0.75 [94]P9(a57,f131(f250(f3(a4),f3(a43))))
% 0.56/0.75 [95]P9(a58,f131(f250(f3(a43),f3(a43))))
% 0.56/0.75 [96]P9(a59,f131(f250(f3(a54),f3(a43))))
% 0.56/0.75 [97]P9(a60,f131(f250(f3(a65),f3(a43))))
% 0.56/0.75 [98]P9(a61,f131(f250(f3(a76),f3(a43))))
% 0.56/0.75 [99]P9(a62,f131(f250(f3(a87),f3(a43))))
% 0.56/0.75 [100]P9(a63,f131(f250(f3(a98),f3(a43))))
% 0.56/0.75 [101]P9(a64,f131(f250(f3(a109),f3(a43))))
% 0.56/0.75 [102]P9(a66,f131(f250(f3(a2),f3(a54))))
% 0.56/0.75 [103]P9(a67,f131(f250(f3(a1),f3(a54))))
% 0.56/0.75 [104]P9(a68,f131(f250(f3(a4),f3(a54))))
% 0.56/0.75 [105]P9(a69,f131(f250(f3(a43),f3(a54))))
% 0.56/0.75 [106]P9(a70,f131(f250(f3(a54),f3(a54))))
% 0.56/0.75 [107]P9(a71,f131(f250(f3(a65),f3(a54))))
% 0.56/0.75 [108]P9(a72,f131(f250(f3(a76),f3(a54))))
% 0.56/0.75 [109]P9(a73,f131(f250(f3(a87),f3(a54))))
% 0.56/0.75 [110]P9(a74,f131(f250(f3(a98),f3(a54))))
% 0.56/0.75 [111]P9(a75,f131(f250(f3(a109),f3(a54))))
% 0.56/0.75 [112]P9(a77,f131(f250(f3(a2),f3(a65))))
% 0.56/0.75 [113]P9(a78,f131(f250(f3(a1),f3(a65))))
% 0.56/0.75 [114]P9(a79,f131(f250(f3(a4),f3(a65))))
% 0.56/0.75 [115]P9(a80,f131(f250(f3(a43),f3(a65))))
% 0.56/0.75 [116]P9(a81,f131(f250(f3(a54),f3(a65))))
% 0.56/0.75 [117]P9(a82,f131(f250(f3(a65),f3(a65))))
% 0.56/0.75 [118]P9(a83,f131(f250(f3(a76),f3(a65))))
% 0.56/0.75 [119]P9(a84,f131(f250(f3(a87),f3(a65))))
% 0.56/0.75 [120]P9(a85,f131(f250(f3(a98),f3(a65))))
% 0.56/0.75 [121]P9(a86,f131(f250(f3(a109),f3(a65))))
% 0.56/0.75 [122]P9(a88,f131(f250(f3(a2),f3(a76))))
% 0.56/0.75 [123]P9(a89,f131(f250(f3(a1),f3(a76))))
% 0.56/0.75 [124]P9(a90,f131(f250(f3(a4),f3(a76))))
% 0.56/0.75 [125]P9(a91,f131(f250(f3(a43),f3(a76))))
% 0.56/0.75 [126]P9(a92,f131(f250(f3(a54),f3(a76))))
% 0.56/0.75 [127]P9(a93,f131(f250(f3(a65),f3(a76))))
% 0.56/0.75 [128]P9(a94,f131(f250(f3(a76),f3(a76))))
% 0.56/0.75 [129]P9(a95,f131(f250(f3(a87),f3(a76))))
% 0.56/0.75 [130]P9(a96,f131(f250(f3(a98),f3(a76))))
% 0.56/0.75 [131]P9(a97,f131(f250(f3(a109),f3(a76))))
% 0.56/0.75 [132]P9(a99,f131(f250(f3(a2),f3(a87))))
% 0.56/0.75 [133]P9(a100,f131(f250(f3(a1),f3(a87))))
% 0.56/0.75 [134]P9(a101,f131(f250(f3(a4),f3(a87))))
% 0.56/0.75 [135]P9(a102,f131(f250(f3(a43),f3(a87))))
% 0.56/0.75 [136]P9(a103,f131(f250(f3(a54),f3(a87))))
% 0.56/0.75 [137]P9(a104,f131(f250(f3(a65),f3(a87))))
% 0.56/0.75 [138]P9(a105,f131(f250(f3(a76),f3(a87))))
% 0.56/0.75 [139]P9(a106,f131(f250(f3(a87),f3(a87))))
% 0.56/0.75 [140]P9(a107,f131(f250(f3(a98),f3(a87))))
% 0.56/0.75 [141]P9(a108,f131(f250(f3(a109),f3(a87))))
% 0.56/0.75 [142]P9(a110,f131(f250(f3(a2),f3(a98))))
% 0.56/0.75 [143]P9(a111,f131(f250(f3(a1),f3(a98))))
% 0.56/0.75 [144]P9(a112,f131(f250(f3(a4),f3(a98))))
% 0.56/0.75 [145]P9(a113,f131(f250(f3(a43),f3(a98))))
% 0.56/0.75 [146]P9(a114,f131(f250(f3(a54),f3(a98))))
% 0.56/0.75 [147]P9(a115,f131(f250(f3(a65),f3(a98))))
% 0.56/0.75 [148]P9(a116,f131(f250(f3(a76),f3(a98))))
% 0.56/0.75 [149]P9(a117,f131(f250(f3(a87),f3(a98))))
% 0.56/0.75 [150]P9(a118,f131(f250(f3(a98),f3(a98))))
% 0.56/0.75 [151]P9(a119,f131(f250(f3(a109),f3(a98))))
% 0.56/0.75 [152]P9(a121,f131(f250(f3(a2),f3(a109))))
% 0.56/0.75 [153]P9(a122,f131(f250(f3(a1),f3(a109))))
% 0.56/0.75 [154]P9(a123,f131(f250(f3(a4),f3(a109))))
% 0.56/0.75 [155]P9(a124,f131(f250(f3(a43),f3(a109))))
% 0.56/0.75 [156]P9(a125,f131(f250(f3(a54),f3(a109))))
% 0.56/0.75 [157]P9(a126,f131(f250(f3(a65),f3(a109))))
% 0.56/0.75 [158]P9(a127,f131(f250(f3(a76),f3(a109))))
% 0.56/0.75 [159]P9(a128,f131(f250(f3(a87),f3(a109))))
% 0.56/0.75 [160]P9(a129,f131(f250(f3(a98),f3(a109))))
% 0.56/0.75 [161]P9(a130,f131(f250(f3(a109),f3(a109))))
% 0.56/0.75 [162]P9(a134,f132(f250(f3(a2),f3(a1))))
% 0.56/0.75 [163]P9(a135,f132(f250(f3(a1),f3(a1))))
% 0.56/0.75 [164]P9(a146,f132(f250(f3(a4),f3(a1))))
% 0.56/0.75 [165]P9(a157,f132(f250(f3(a43),f3(a1))))
% 0.56/0.75 [166]P9(a167,f132(f250(f3(a54),f3(a1))))
% 0.56/0.75 [167]P9(a168,f132(f250(f3(a65),f3(a1))))
% 0.56/0.75 [168]P9(a169,f132(f250(f3(a76),f3(a1))))
% 0.56/0.75 [169]P9(a170,f132(f250(f3(a87),f3(a1))))
% 0.56/0.75 [170]P9(a171,f132(f250(f3(a98),f3(a1))))
% 0.56/0.75 [171]P9(a172,f132(f250(f3(a109),f3(a1))))
% 0.56/0.75 [172]P9(a174,f132(f250(f3(a2),f3(a4))))
% 0.56/0.75 [173]P9(a175,f132(f250(f3(a1),f3(a4))))
% 0.56/0.75 [174]P9(a176,f132(f250(f3(a4),f3(a4))))
% 0.56/0.75 [175]P9(a177,f132(f250(f3(a43),f3(a4))))
% 0.56/0.75 [176]P9(a178,f132(f250(f3(a54),f3(a4))))
% 0.56/0.75 [177]P9(a179,f132(f250(f3(a65),f3(a4))))
% 0.56/0.75 [178]P9(a180,f132(f250(f3(a76),f3(a4))))
% 0.56/0.75 [179]P9(a181,f132(f250(f3(a87),f3(a4))))
% 0.56/0.75 [180]P9(a182,f132(f250(f3(a98),f3(a4))))
% 0.56/0.75 [181]P9(a183,f132(f250(f3(a109),f3(a4))))
% 0.56/0.75 [182]P9(a185,f132(f250(f3(a2),f3(a43))))
% 0.56/0.75 [183]P9(a186,f132(f250(f3(a1),f3(a43))))
% 0.56/0.75 [184]P9(a187,f132(f250(f3(a4),f3(a43))))
% 0.56/0.75 [185]P9(a188,f132(f250(f3(a43),f3(a43))))
% 0.56/0.75 [186]P9(a189,f132(f250(f3(a54),f3(a43))))
% 0.56/0.75 [187]P9(a190,f132(f250(f3(a65),f3(a43))))
% 0.56/0.75 [188]P9(a191,f132(f250(f3(a76),f3(a43))))
% 0.56/0.75 [189]P9(a192,f132(f250(f3(a87),f3(a43))))
% 0.56/0.75 [190]P9(a193,f132(f250(f3(a98),f3(a43))))
% 0.56/0.75 [191]P9(a194,f132(f250(f3(a109),f3(a43))))
% 0.56/0.75 [192]P9(a196,f132(f250(f3(a2),f3(a54))))
% 0.56/0.75 [193]P9(a197,f132(f250(f3(a1),f3(a54))))
% 0.56/0.75 [194]P9(a198,f132(f250(f3(a4),f3(a54))))
% 0.56/0.75 [195]P9(a199,f132(f250(f3(a43),f3(a54))))
% 0.56/0.75 [196]P9(a200,f132(f250(f3(a54),f3(a54))))
% 0.56/0.75 [197]P9(a201,f132(f250(f3(a65),f3(a54))))
% 0.56/0.75 [198]P9(a202,f132(f250(f3(a76),f3(a54))))
% 0.56/0.75 [199]P9(a203,f132(f250(f3(a87),f3(a54))))
% 0.56/0.75 [200]P9(a204,f132(f250(f3(a98),f3(a54))))
% 0.56/0.75 [201]P9(a205,f132(f250(f3(a109),f3(a54))))
% 0.56/0.75 [202]P9(a207,f132(f250(f3(a2),f3(a65))))
% 0.56/0.75 [203]P9(a208,f132(f250(f3(a1),f3(a65))))
% 0.56/0.75 [204]P9(a209,f132(f250(f3(a4),f3(a65))))
% 0.56/0.75 [205]P9(a210,f132(f250(f3(a43),f3(a65))))
% 0.56/0.75 [206]P9(a211,f132(f250(f3(a54),f3(a65))))
% 0.56/0.75 [207]P9(a212,f132(f250(f3(a65),f3(a65))))
% 0.56/0.75 [208]P9(a213,f132(f250(f3(a76),f3(a65))))
% 0.56/0.75 [209]P9(a214,f132(f250(f3(a87),f3(a65))))
% 0.56/0.75 [210]P9(a215,f132(f250(f3(a98),f3(a65))))
% 0.56/0.75 [211]P9(a216,f132(f250(f3(a109),f3(a65))))
% 0.56/0.75 [212]P9(a218,f132(f250(f3(a2),f3(a76))))
% 0.56/0.75 [213]P9(a219,f132(f250(f3(a1),f3(a76))))
% 0.56/0.75 [214]P9(a220,f132(f250(f3(a4),f3(a76))))
% 0.56/0.75 [215]P9(a221,f132(f250(f3(a43),f3(a76))))
% 0.56/0.75 [216]P9(a222,f132(f250(f3(a54),f3(a76))))
% 0.56/0.75 [217]P9(a223,f132(f250(f3(a65),f3(a76))))
% 0.56/0.75 [218]P9(a224,f132(f250(f3(a76),f3(a76))))
% 0.56/0.75 [219]P9(a225,f132(f250(f3(a87),f3(a76))))
% 0.56/0.75 [220]P9(a226,f132(f250(f3(a98),f3(a76))))
% 0.56/0.75 [221]P9(a227,f132(f250(f3(a109),f3(a76))))
% 0.56/0.75 [222]P9(a229,f132(f250(f3(a2),f3(a87))))
% 0.56/0.75 [223]P9(a230,f132(f250(f3(a1),f3(a87))))
% 0.56/0.75 [224]P9(a231,f132(f250(f3(a4),f3(a87))))
% 0.56/0.75 [225]P9(a232,f132(f250(f3(a43),f3(a87))))
% 0.56/0.75 [226]P9(a233,f132(f250(f3(a54),f3(a87))))
% 0.56/0.75 [227]P9(a234,f132(f250(f3(a65),f3(a87))))
% 0.56/0.75 [228]P9(a235,f132(f250(f3(a76),f3(a87))))
% 0.56/0.75 [229]P9(a236,f132(f250(f3(a87),f3(a87))))
% 0.56/0.75 [230]P9(a237,f132(f250(f3(a98),f3(a87))))
% 0.56/0.75 [231]P9(a238,f132(f250(f3(a109),f3(a87))))
% 0.56/0.75 [232]P9(a240,f132(f250(f3(a2),f3(a98))))
% 0.56/0.75 [233]P9(a241,f132(f250(f3(a1),f3(a98))))
% 0.56/0.75 [234]P9(a242,f132(f250(f3(a4),f3(a98))))
% 0.56/0.75 [235]P9(a243,f132(f250(f3(a43),f3(a98))))
% 0.56/0.75 [236]P9(a244,f132(f250(f3(a54),f3(a98))))
% 0.56/0.75 [237]P9(a245,f132(f250(f3(a65),f3(a98))))
% 0.56/0.75 [238]P9(a246,f132(f250(f3(a76),f3(a98))))
% 0.56/0.75 [239]P9(a247,f132(f250(f3(a87),f3(a98))))
% 0.56/0.75 [240]P9(a248,f132(f250(f3(a98),f3(a98))))
% 0.56/0.75 [241]P9(a249,f132(f250(f3(a109),f3(a98))))
% 0.56/0.75 [242]P9(a251,f132(f250(f3(a2),f3(a109))))
% 0.56/0.75 [243]P9(a252,f132(f250(f3(a1),f3(a109))))
% 0.56/0.75 [244]P9(a253,f132(f250(f3(a4),f3(a109))))
% 0.56/0.75 [245]P9(a254,f132(f250(f3(a43),f3(a109))))
% 0.56/0.75 [246]P9(a255,f132(f250(f3(a54),f3(a109))))
% 0.56/0.75 [247]P9(a256,f132(f250(f3(a65),f3(a109))))
% 0.56/0.75 [248]P9(a257,f132(f250(f3(a76),f3(a109))))
% 0.56/0.75 [249]P9(a258,f132(f250(f3(a87),f3(a109))))
% 0.56/0.75 [250]P9(a259,f132(f250(f3(a98),f3(a109))))
% 0.56/0.75 [251]P9(a260,f132(f250(f3(a109),f3(a109))))
% 0.56/0.75 [252]P9(a7,f131(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [253]P9(a8,f131(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [254]P9(a9,f131(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [255]P9(a10,f131(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [256]P9(a11,f131(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [257]P9(a12,f131(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [258]P9(a13,f131(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [259]P9(a14,f131(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [260]P9(a15,f131(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [261]P9(a16,f131(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [262]P9(a18,f131(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [263]P9(a19,f131(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [264]P9(a20,f131(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [265]P9(a21,f131(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [266]P9(a22,f131(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [267]P9(a23,f131(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [268]P9(a24,f131(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [269]P9(a25,f131(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [270]P9(a26,f131(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [271]P9(a27,f131(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [272]P9(a29,f131(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [273]P9(a30,f131(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [274]P9(a31,f131(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [275]P9(a32,f131(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [276]P9(a33,f131(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [277]P9(a34,f131(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [278]P9(a35,f131(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [279]P9(a36,f131(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [280]P9(a136,f132(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [281]P9(a137,f132(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [282]P9(a138,f132(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [283]P9(a139,f132(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [284]P9(a140,f132(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [285]P9(a141,f132(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [286]P9(a142,f132(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [287]P9(a143,f132(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [288]P9(a144,f132(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [289]P9(a145,f132(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 0.56/0.75 [290]P9(a147,f132(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [291]P9(a148,f132(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [292]P9(a149,f132(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [293]P9(a150,f132(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [294]P9(a151,f132(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [295]P9(a152,f132(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [296]P9(a153,f132(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [297]P9(a154,f132(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [298]P9(a155,f132(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [299]P9(a156,f132(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 0.56/0.75 [300]P9(a158,f132(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [301]P9(a159,f132(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [302]P9(a160,f132(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [303]P9(a161,f132(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [304]P9(a162,f132(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [305]P9(a163,f132(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [306]P9(a164,f132(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [307]P9(a165,f132(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [308]P9(a166,f132(f250(f3(a98),f250(f3(a4),f3(a1)))))
% 0.56/0.75 [42]P2(x421,a1)
% 0.56/0.75 [43]P2(a120,x431)
% 0.56/0.75 [409]~P10(a45,x4091,a45)
% 0.56/0.75 [412]P7(f3(x4121))+~P1(f3(x4121))
% 0.56/0.75 [410]~E(x4101,x4102)+P5(x4101,x4102)
% 0.56/0.75 [411]~P2(x4112,x4111)+~E(x4111,x4112)
% 0.56/0.75 [414]~P2(x4141,x4142)+P5(x4141,x4142)
% 0.56/0.75 [416]~P2(x4162,x4161)+~P2(x4161,x4162)
% 0.56/0.75 [417]~P7(x4172)+P7(f250(f3(x4171),x4172))
% 0.56/0.75 [427]~P3(x4273,x4271,x4272)+P10(x4271,x4272,x4273)
% 0.56/0.75 [428]~P10(x4282,x4283,x4281)+P3(x4281,x4282,x4283)
% 0.56/0.75 [418]~P7(x4183)+P8(f3(x4181),f250(f3(x4182),x4183))
% 0.56/0.75 [423]~P8(x4232,x4234)+P8(f250(f3(x4231),x4232),f250(f3(x4233),x4234))
% 0.56/0.75 [437]P6(f3(x4371),f250(f3(x4372),x4373),f3(x4374),f250(f3(x4375),x4376))+~P6(f3(x4371),f3(x4374),f250(f3(x4372),x4373),f250(f3(x4375),x4376))
% 0.56/0.75 [413]P2(x4132,x4131)+P2(x4131,x4132)+E(x4131,x4132)
% 0.56/0.75 [415]P2(x4151,x4152)+~P5(x4151,x4152)+E(x4151,x4152)
% 0.56/0.75 [425]P5(x4251,x4252)+~P2(x4251,x4253)+~P10(x4252,a1,x4253)
% 0.56/0.75 [422]P8(f3(x4221),f3(x4222))+~P8(f3(x4223),f3(x4222))+~P8(f3(x4221),f3(x4223))
% 0.56/0.75 [424]P10(x4241,x4242,a2)+~P9(x4241,f131(x4243))+~P9(x4242,f132(x4243))
% 0.56/0.75 [426]~P7(x4262)+~P8(f3(x4261),f3(x4263))+P8(f250(f3(x4261),x4262),f250(f3(x4263),x4262))
% 0.56/0.75 [429]~P10(x4293,x4294,x4291)+E(x4291,x4292)+~P10(x4293,x4294,x4292)
% 0.56/0.75 [430]~P10(x4303,x4301,x4304)+E(x4301,x4302)+~P10(x4303,x4302,x4304)
% 0.56/0.75 [431]~P10(x4311,x4313,x4314)+E(x4311,x4312)+~P10(x4312,x4313,x4314)
% 0.56/0.75 [419]P2(x4191,x4192)+~P9(x4192,f131(x4193))+~P9(x4191,f132(x4194))
% 0.56/0.75 [438]P6(f3(x4381),f3(x4382),f3(x4383),f3(x4384))+~P4(f3(x4385),f3(x4381),f3(x4384),f3(a2))+~P4(f3(x4382),f3(x4383),f3(x4385),f3(a2))
% 0.56/0.75 [420]P2(x4201,x4202)+~P8(x4203,x4204)+~P9(x4202,f132(x4203))+~P9(x4201,f132(x4204))
% 0.56/0.75 [421]P2(x4211,x4212)+~P8(x4213,x4214)+~P9(x4212,f131(x4214))+~P9(x4211,f131(x4213))
% 0.56/0.75 [432]~P10(x4322,x4321,x4323)+P10(x4321,x4322,x4323)+~P9(x4322,f131(x4324))+~P9(x4321,f132(x4325))
% 0.56/0.75 [439]~P4(f3(x4395),f3(x4391),f3(x4394),f3(x4396))+~P4(f3(x4392),f3(x4393),f3(x4395),f3(x4397))+~P4(f3(x4397),f3(x4396),f3(a1),f3(a2))+P6(f3(x4391),f3(x4392),f3(x4393),f250(f3(x4394),f3(a1)))
% 0.56/0.75 [433]P10(x4331,x4332,x4333)+~P6(f3(a2),x4336,x4335,x4334)+~P9(x4333,f131(x4334))+~P9(x4332,f131(x4335))+~P9(x4331,f131(x4336))
% 0.56/0.76 [434]P10(x4341,x4342,x4343)+~P6(f3(a2),x4346,x4345,x4344)+~P9(x4343,f132(x4344))+~P9(x4342,f132(x4345))+~P9(x4341,f132(x4346))
% 0.56/0.76 [435]P10(x4351,x4352,x4353)+~P8(x4354,x4355)+~P6(f3(a2),x4354,x4356,x4355)+~P9(x4352,f132(x4354))+~P9(x4351,f131(x4355))+~P9(x4353,f131(x4356))
% 0.56/0.76 [436]P10(x4361,x4362,x4363)+~P8(x4364,x4365)+~P6(f3(a2),x4364,x4366,x4365)+~P9(x4362,f132(x4365))+~P9(x4361,f131(x4364))+~P9(x4363,f132(x4366))
% 0.56/0.76 [440]~P7(x4406)+~P7(x4404)+~P4(f3(x4408),f3(x4401),f3(x4405),f3(x4409))+~P4(f3(x4402),f3(x4403),f3(x4408),f3(x44010))+~P6(f3(x4407),f3(a2),x4404,x4406)+~P4(f3(x44010),f3(x4409),f3(x4407),f3(a2))+P6(f3(x4401),f3(x4402),f250(f3(x4403),x4404),f250(f3(x4405),x4406))
% 0.56/0.76 [441]~P7(x4417)+~P7(x4415)+~P7(x4413)+~P6(f3(x4418),x4413,x4415,x4417)+~P4(f3(x4419),f3(x4411),f3(x4416),f3(x44110))+~P4(f3(x4412),f3(x4414),f3(x4419),f3(x44111))+~P4(f3(x44111),f3(x44110),f3(x4418),f3(a2))+P6(f3(x4411),f250(f3(x4412),x4413),f250(f3(x4414),x4415),f250(f3(x4416),x4417))
% 0.56/0.76 %EqnAxiom
% 0.56/0.76 [1]E(x11,x11)
% 0.56/0.76 [2]E(x22,x21)+~E(x21,x22)
% 0.56/0.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.56/0.76 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 0.56/0.76 [5]~E(x51,x52)+E(f250(x51,x53),f250(x52,x53))
% 0.56/0.76 [6]~E(x61,x62)+E(f250(x63,x61),f250(x63,x62))
% 0.56/0.76 [7]~E(x71,x72)+E(f132(x71),f132(x72))
% 0.56/0.76 [8]~E(x81,x82)+E(f131(x81),f131(x82))
% 0.56/0.76 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 0.56/0.76 [10]P4(x102,x103,x104,x105)+~E(x101,x102)+~P4(x101,x103,x104,x105)
% 0.56/0.76 [11]P4(x113,x112,x114,x115)+~E(x111,x112)+~P4(x113,x111,x114,x115)
% 0.56/0.76 [12]P4(x123,x124,x122,x125)+~E(x121,x122)+~P4(x123,x124,x121,x125)
% 0.56/0.76 [13]P4(x133,x134,x135,x132)+~E(x131,x132)+~P4(x133,x134,x135,x131)
% 0.56/0.76 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 0.56/0.76 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 0.56/0.76 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 0.56/0.76 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 0.56/0.76 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 0.56/0.76 [19]P10(x192,x193,x194)+~E(x191,x192)+~P10(x191,x193,x194)
% 0.56/0.76 [20]P10(x203,x202,x204)+~E(x201,x202)+~P10(x203,x201,x204)
% 0.56/0.76 [21]P10(x213,x214,x212)+~E(x211,x212)+~P10(x213,x214,x211)
% 0.56/0.76 [22]P2(x222,x223)+~E(x221,x222)+~P2(x221,x223)
% 0.56/0.76 [23]P2(x233,x232)+~E(x231,x232)+~P2(x233,x231)
% 0.56/0.76 [24]P8(x242,x243)+~E(x241,x242)+~P8(x241,x243)
% 0.56/0.76 [25]P8(x253,x252)+~E(x251,x252)+~P8(x253,x251)
% 0.56/0.76 [26]P5(x262,x263)+~E(x261,x262)+~P5(x261,x263)
% 0.56/0.76 [27]P5(x273,x272)+~E(x271,x272)+~P5(x273,x271)
% 0.56/0.76 [28]P9(x282,x283)+~E(x281,x282)+~P9(x281,x283)
% 0.56/0.76 [29]P9(x293,x292)+~E(x291,x292)+~P9(x293,x291)
% 0.56/0.76 [30]P3(x302,x303,x304)+~E(x301,x302)+~P3(x301,x303,x304)
% 0.56/0.76 [31]P3(x313,x312,x314)+~E(x311,x312)+~P3(x313,x311,x314)
% 0.56/0.76 [32]P3(x323,x324,x322)+~E(x321,x322)+~P3(x323,x324,x321)
% 0.56/0.76
% 0.56/0.76 %-------------------------------------------
% 0.56/0.76 cnf(443,plain,
% 0.56/0.76 (~P2(x4431,x4431)),
% 0.56/0.76 inference(equality_inference,[],[411])).
% 0.56/0.76 cnf(444,plain,
% 0.56/0.76 ($false),
% 0.56/0.76 inference(scs_inference,[],[42,443]),
% 0.56/0.76 ['proof']).
% 0.56/0.76 % SZS output end Proof
% 0.56/0.76 % Total time :0.020000s
%------------------------------------------------------------------------------