%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM305+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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:47 EDT 2024
% Result : Theorem 60.70s 60.72s
% Output : CNFRefutation 60.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NUM305+1 : TPTP v8.2.0. Released v3.1.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/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 : Sun Jun 23 01:04:09 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 60.70/60.71 %-------------------------------------------
% 60.70/60.71 % File :CSE---1.7
% 60.70/60.71 % Problem :theBenchmark
% 60.70/60.71 % Transform :cnf
% 60.70/60.71 % Format :tptp:raw
% 60.70/60.71 % Command :java -jar mcs_scs.jar %d %s
% 60.70/60.71
% 60.70/60.71 % Result :Theorem 60.010000s
% 60.70/60.71 % Output :CNFRefutation 60.010000s
% 60.70/60.71 %-------------------------------------------
% 60.70/60.72 %------------------------------------------------------------------------------
% 60.70/60.72 % File : NUM305+1 : TPTP v8.2.0. Released v3.1.0.
% 60.70/60.72 % Domain : Number Theory (RDN arithmetic)
% 60.70/60.72 % Problem : 2 + 3 = 5
% 60.70/60.72 % Version : Especial.
% 60.70/60.72 % English :
% 60.70/60.72
% 60.70/60.72 % Refs :
% 60.70/60.72 % Source : [TPTP]
% 60.70/60.72 % Names :
% 60.70/60.72
% 60.70/60.72 % Status : Theorem
% 60.70/60.72 % Rating : 0.42 v7.5.0, 0.44 v7.4.0, 0.43 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.26 v7.0.0, 0.37 v6.4.0, 0.42 v6.3.0, 0.38 v6.2.0, 0.40 v6.1.0, 0.57 v6.0.0, 0.48 v5.5.0, 0.52 v5.4.0, 0.57 v5.3.0, 0.63 v5.2.0, 0.55 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.61 v4.0.0, 0.58 v3.7.0, 0.60 v3.5.0, 0.68 v3.3.0, 0.64 v3.2.0, 0.82 v3.1.0
% 60.70/60.72 % Syntax : Number of formulae : 402 ( 375 unt; 0 def)
% 60.70/60.72 % Number of atoms : 473 ( 5 equ)
% 60.70/60.72 % Maximal formula atoms : 8 ( 1 avg)
% 60.70/60.72 % Number of connectives : 73 ( 2 ~; 1 |; 43 &)
% 60.70/60.72 % ( 3 <=>; 24 =>; 0 <=; 0 <~>)
% 60.70/60.72 % Maximal formula depth : 19 ( 1 avg)
% 60.70/60.72 % Maximal term depth : 5 ( 2 avg)
% 60.70/60.72 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 60.70/60.72 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 60.70/60.72 % Number of variables : 121 ( 121 !; 0 ?)
% 60.70/60.72 % SPC : FOF_THM_RFO_SEQ
% 60.70/60.72
% 60.70/60.72 % Comments :
% 60.70/60.72 %------------------------------------------------------------------------------
% 60.70/60.72 %----Include axioms for RDN arithmetic
% 60.70/60.72 include('Axioms/NUM005+0.ax').
% 60.70/60.72 include('Axioms/NUM005+1.ax').
% 60.70/60.72 include('Axioms/NUM005+2.ax').
% 60.70/60.72 %------------------------------------------------------------------------------
% 60.70/60.72 fof(sum_n2_n3_n5,conjecture,
% 60.70/60.72 sum(n2,n3,n5) ).
% 60.70/60.72
% 60.70/60.72 %------------------------------------------------------------------------------
% 60.70/60.72 %-------------------------------------------
% 60.70/60.72 % Proof found
% 60.70/60.72 % SZS status Theorem for theBenchmark
% 60.70/60.72 % SZS output start Proof
% 60.70/60.72 %ClaNum:439(EqnAxiom:32)
% 60.70/60.72 %VarNum:271(SingletonVarNum:132)
% 60.70/60.72 %MaxLitNum:8
% 60.70/60.72 %MaxfuncDepth:4
% 60.70/60.72 %SharedTerms:967
% 60.70/60.72 %goalClause: 407
% 60.70/60.72 %singleGoalClaCount:1
% 60.70/60.72 [407]~P10(a4,a43,a65)
% 60.70/60.72 [33]P1(f3(a1))
% 60.70/60.72 [34]P1(f3(a4))
% 60.70/60.72 [35]P1(f3(a43))
% 60.70/60.72 [36]P1(f3(a54))
% 60.70/60.72 [37]P1(f3(a65))
% 60.70/60.72 [38]P1(f3(a76))
% 60.70/60.72 [39]P1(f3(a87))
% 60.70/60.72 [40]P1(f3(a98))
% 60.70/60.72 [41]P1(f3(a109))
% 60.70/60.72 [42]P8(f3(a2),f3(a1))
% 60.70/60.72 [43]P8(f3(a1),f3(a4))
% 60.70/60.72 [44]P8(f3(a4),f3(a43))
% 60.70/60.72 [45]P8(f3(a43),f3(a54))
% 60.70/60.72 [46]P8(f3(a54),f3(a65))
% 60.70/60.72 [47]P8(f3(a65),f3(a76))
% 60.70/60.72 [48]P8(f3(a76),f3(a87))
% 60.70/60.72 [49]P8(f3(a87),f3(a98))
% 60.70/60.72 [50]P8(f3(a98),f3(a109))
% 60.70/60.72 [307]P2(f3(a2),f3(a2),f3(a2),f3(a2))
% 60.70/60.72 [308]P2(f3(a2),f3(a1),f3(a1),f3(a2))
% 60.70/60.72 [309]P2(f3(a2),f3(a4),f3(a4),f3(a2))
% 60.70/60.72 [310]P2(f3(a2),f3(a43),f3(a43),f3(a2))
% 60.70/60.72 [311]P2(f3(a2),f3(a54),f3(a54),f3(a2))
% 60.70/60.72 [312]P2(f3(a2),f3(a65),f3(a65),f3(a2))
% 60.70/60.72 [313]P2(f3(a2),f3(a76),f3(a76),f3(a2))
% 60.70/60.72 [314]P2(f3(a2),f3(a87),f3(a87),f3(a2))
% 60.70/60.72 [315]P2(f3(a2),f3(a98),f3(a98),f3(a2))
% 60.70/60.72 [316]P2(f3(a2),f3(a109),f3(a109),f3(a2))
% 60.70/60.72 [317]P2(f3(a1),f3(a2),f3(a1),f3(a2))
% 60.70/60.72 [318]P2(f3(a1),f3(a1),f3(a4),f3(a2))
% 60.70/60.72 [319]P2(f3(a1),f3(a4),f3(a43),f3(a2))
% 60.70/60.72 [320]P2(f3(a1),f3(a43),f3(a54),f3(a2))
% 60.70/60.72 [321]P2(f3(a1),f3(a54),f3(a65),f3(a2))
% 60.70/60.72 [322]P2(f3(a1),f3(a65),f3(a76),f3(a2))
% 60.70/60.72 [323]P2(f3(a1),f3(a76),f3(a87),f3(a2))
% 60.70/60.72 [324]P2(f3(a1),f3(a87),f3(a98),f3(a2))
% 60.70/60.72 [325]P2(f3(a1),f3(a98),f3(a109),f3(a2))
% 60.70/60.72 [326]P2(f3(a1),f3(a109),f3(a2),f3(a1))
% 60.70/60.72 [327]P2(f3(a4),f3(a2),f3(a4),f3(a2))
% 60.70/60.72 [328]P2(f3(a4),f3(a1),f3(a43),f3(a2))
% 60.70/60.72 [329]P2(f3(a4),f3(a4),f3(a54),f3(a2))
% 60.70/60.72 [330]P2(f3(a4),f3(a43),f3(a65),f3(a2))
% 60.70/60.72 [331]P2(f3(a4),f3(a54),f3(a76),f3(a2))
% 60.70/60.72 [332]P2(f3(a4),f3(a65),f3(a87),f3(a2))
% 60.70/60.72 [333]P2(f3(a4),f3(a76),f3(a98),f3(a2))
% 60.70/60.72 [334]P2(f3(a4),f3(a87),f3(a109),f3(a2))
% 60.70/60.72 [335]P2(f3(a4),f3(a98),f3(a2),f3(a1))
% 60.70/60.72 [336]P2(f3(a4),f3(a109),f3(a1),f3(a1))
% 60.70/60.72 [337]P2(f3(a43),f3(a2),f3(a43),f3(a2))
% 60.70/60.72 [338]P2(f3(a43),f3(a1),f3(a54),f3(a2))
% 60.70/60.73 [339]P2(f3(a43),f3(a4),f3(a65),f3(a2))
% 60.70/60.73 [340]P2(f3(a43),f3(a43),f3(a76),f3(a2))
% 60.70/60.73 [341]P2(f3(a43),f3(a54),f3(a87),f3(a2))
% 60.70/60.73 [342]P2(f3(a43),f3(a65),f3(a98),f3(a2))
% 60.70/60.73 [343]P2(f3(a43),f3(a76),f3(a109),f3(a2))
% 60.70/60.73 [344]P2(f3(a43),f3(a87),f3(a2),f3(a1))
% 60.70/60.73 [345]P2(f3(a43),f3(a98),f3(a1),f3(a1))
% 60.70/60.73 [346]P2(f3(a43),f3(a109),f3(a4),f3(a1))
% 60.70/60.73 [347]P2(f3(a54),f3(a2),f3(a54),f3(a2))
% 60.70/60.73 [348]P2(f3(a54),f3(a1),f3(a65),f3(a2))
% 60.70/60.73 [349]P2(f3(a54),f3(a4),f3(a76),f3(a2))
% 60.70/60.73 [350]P2(f3(a54),f3(a43),f3(a87),f3(a2))
% 60.70/60.73 [351]P2(f3(a54),f3(a54),f3(a98),f3(a2))
% 60.70/60.73 [352]P2(f3(a54),f3(a65),f3(a109),f3(a2))
% 60.70/60.73 [353]P2(f3(a54),f3(a76),f3(a2),f3(a1))
% 60.70/60.73 [354]P2(f3(a54),f3(a87),f3(a1),f3(a1))
% 60.70/60.73 [355]P2(f3(a54),f3(a98),f3(a4),f3(a1))
% 60.70/60.73 [356]P2(f3(a54),f3(a109),f3(a43),f3(a1))
% 60.70/60.73 [357]P2(f3(a65),f3(a2),f3(a65),f3(a2))
% 60.70/60.73 [358]P2(f3(a65),f3(a1),f3(a76),f3(a2))
% 60.70/60.73 [359]P2(f3(a65),f3(a4),f3(a87),f3(a2))
% 60.70/60.73 [360]P2(f3(a65),f3(a43),f3(a98),f3(a2))
% 60.70/60.73 [361]P2(f3(a65),f3(a54),f3(a109),f3(a2))
% 60.70/60.73 [362]P2(f3(a65),f3(a65),f3(a2),f3(a1))
% 60.70/60.73 [363]P2(f3(a65),f3(a76),f3(a1),f3(a1))
% 60.70/60.73 [364]P2(f3(a65),f3(a87),f3(a4),f3(a1))
% 60.70/60.73 [365]P2(f3(a65),f3(a98),f3(a43),f3(a1))
% 60.70/60.73 [366]P2(f3(a65),f3(a109),f3(a54),f3(a1))
% 60.70/60.73 [367]P2(f3(a76),f3(a2),f3(a76),f3(a2))
% 60.70/60.73 [368]P2(f3(a76),f3(a1),f3(a87),f3(a2))
% 60.70/60.73 [369]P2(f3(a76),f3(a4),f3(a98),f3(a2))
% 60.70/60.73 [370]P2(f3(a76),f3(a43),f3(a109),f3(a2))
% 60.70/60.73 [371]P2(f3(a76),f3(a54),f3(a2),f3(a1))
% 60.70/60.73 [372]P2(f3(a76),f3(a65),f3(a1),f3(a1))
% 60.70/60.73 [373]P2(f3(a76),f3(a76),f3(a4),f3(a1))
% 60.70/60.73 [374]P2(f3(a76),f3(a87),f3(a43),f3(a1))
% 60.70/60.73 [375]P2(f3(a76),f3(a98),f3(a54),f3(a1))
% 60.70/60.73 [376]P2(f3(a76),f3(a109),f3(a65),f3(a1))
% 60.70/60.73 [377]P2(f3(a87),f3(a2),f3(a87),f3(a2))
% 60.70/60.73 [378]P2(f3(a87),f3(a1),f3(a98),f3(a2))
% 60.70/60.73 [379]P2(f3(a87),f3(a4),f3(a109),f3(a2))
% 60.70/60.73 [380]P2(f3(a87),f3(a43),f3(a2),f3(a1))
% 60.70/60.73 [381]P2(f3(a87),f3(a54),f3(a1),f3(a1))
% 60.70/60.73 [382]P2(f3(a87),f3(a65),f3(a4),f3(a1))
% 60.70/60.73 [383]P2(f3(a87),f3(a76),f3(a43),f3(a1))
% 60.70/60.73 [384]P2(f3(a87),f3(a87),f3(a54),f3(a1))
% 60.70/60.73 [385]P2(f3(a87),f3(a98),f3(a65),f3(a1))
% 60.70/60.73 [386]P2(f3(a87),f3(a109),f3(a76),f3(a1))
% 60.70/60.73 [387]P2(f3(a98),f3(a2),f3(a98),f3(a2))
% 60.70/60.73 [388]P2(f3(a98),f3(a1),f3(a109),f3(a2))
% 60.70/60.73 [389]P2(f3(a98),f3(a4),f3(a2),f3(a1))
% 60.70/60.73 [390]P2(f3(a98),f3(a43),f3(a1),f3(a1))
% 60.70/60.73 [391]P2(f3(a98),f3(a54),f3(a4),f3(a1))
% 60.70/60.73 [392]P2(f3(a98),f3(a65),f3(a43),f3(a1))
% 60.70/60.73 [393]P2(f3(a98),f3(a76),f3(a54),f3(a1))
% 60.70/60.73 [394]P2(f3(a98),f3(a87),f3(a65),f3(a1))
% 60.70/60.73 [395]P2(f3(a98),f3(a98),f3(a76),f3(a1))
% 60.70/60.73 [396]P2(f3(a98),f3(a109),f3(a87),f3(a1))
% 60.70/60.73 [397]P2(f3(a109),f3(a2),f3(a109),f3(a2))
% 60.70/60.73 [398]P2(f3(a109),f3(a1),f3(a2),f3(a1))
% 60.70/60.73 [399]P2(f3(a109),f3(a4),f3(a1),f3(a1))
% 60.70/60.73 [400]P2(f3(a109),f3(a43),f3(a4),f3(a1))
% 60.70/60.73 [401]P2(f3(a109),f3(a54),f3(a43),f3(a1))
% 60.70/60.73 [402]P2(f3(a109),f3(a65),f3(a54),f3(a1))
% 60.70/60.73 [403]P2(f3(a109),f3(a76),f3(a65),f3(a1))
% 60.70/60.73 [404]P2(f3(a109),f3(a87),f3(a76),f3(a1))
% 60.70/60.73 [405]P2(f3(a109),f3(a98),f3(a87),f3(a1))
% 60.70/60.73 [406]P2(f3(a109),f3(a109),f3(a98),f3(a1))
% 60.70/60.73 [51]P9(a2,f120(f3(a2)))
% 60.70/60.73 [52]P9(a1,f120(f3(a1)))
% 60.70/60.73 [53]P9(a4,f120(f3(a4)))
% 60.70/60.73 [54]P9(a43,f120(f3(a43)))
% 60.70/60.73 [55]P9(a54,f120(f3(a54)))
% 60.70/60.73 [56]P9(a65,f120(f3(a65)))
% 60.70/60.73 [57]P9(a76,f120(f3(a76)))
% 60.70/60.73 [58]P9(a87,f120(f3(a87)))
% 60.70/60.73 [59]P9(a98,f120(f3(a98)))
% 60.70/60.73 [60]P9(a109,f120(f3(a109)))
% 60.70/60.73 [61]P9(a121,f132(f3(a1)))
% 60.70/60.73 [62]P9(a133,f132(f3(a4)))
% 60.70/60.73 [63]P9(a173,f132(f3(a43)))
% 60.70/60.73 [64]P9(a184,f132(f3(a54)))
% 60.70/60.73 [65]P9(a195,f132(f3(a65)))
% 60.70/60.73 [66]P9(a206,f132(f3(a76)))
% 60.70/60.73 [67]P9(a217,f132(f3(a87)))
% 60.70/60.73 [68]P9(a228,f132(f3(a98)))
% 60.70/60.73 [69]P9(a239,f132(f3(a109)))
% 60.70/60.73 [70]P9(a5,f120(f250(f3(a2),f3(a1))))
% 60.70/60.73 [71]P9(a6,f120(f250(f3(a1),f3(a1))))
% 60.70/60.73 [72]P9(a17,f120(f250(f3(a4),f3(a1))))
% 60.70/60.73 [73]P9(a28,f120(f250(f3(a43),f3(a1))))
% 60.70/60.73 [74]P9(a37,f120(f250(f3(a54),f3(a1))))
% 60.70/60.73 [75]P9(a38,f120(f250(f3(a65),f3(a1))))
% 60.70/60.73 [76]P9(a39,f120(f250(f3(a76),f3(a1))))
% 60.70/60.73 [77]P9(a40,f120(f250(f3(a87),f3(a1))))
% 60.70/60.73 [78]P9(a41,f120(f250(f3(a98),f3(a1))))
% 60.70/60.73 [79]P9(a42,f120(f250(f3(a109),f3(a1))))
% 60.70/60.73 [80]P9(a44,f120(f250(f3(a2),f3(a4))))
% 60.70/60.73 [81]P9(a45,f120(f250(f3(a1),f3(a4))))
% 60.70/60.73 [82]P9(a46,f120(f250(f3(a4),f3(a4))))
% 60.70/60.73 [83]P9(a47,f120(f250(f3(a43),f3(a4))))
% 60.70/60.73 [84]P9(a48,f120(f250(f3(a54),f3(a4))))
% 60.70/60.73 [85]P9(a49,f120(f250(f3(a65),f3(a4))))
% 60.70/60.73 [86]P9(a50,f120(f250(f3(a76),f3(a4))))
% 60.70/60.73 [87]P9(a51,f120(f250(f3(a87),f3(a4))))
% 60.70/60.73 [88]P9(a52,f120(f250(f3(a98),f3(a4))))
% 60.70/60.73 [89]P9(a53,f120(f250(f3(a109),f3(a4))))
% 60.70/60.73 [90]P9(a55,f120(f250(f3(a2),f3(a43))))
% 60.70/60.73 [91]P9(a56,f120(f250(f3(a1),f3(a43))))
% 60.70/60.73 [92]P9(a57,f120(f250(f3(a4),f3(a43))))
% 60.70/60.73 [93]P9(a58,f120(f250(f3(a43),f3(a43))))
% 60.70/60.73 [94]P9(a59,f120(f250(f3(a54),f3(a43))))
% 60.70/60.73 [95]P9(a60,f120(f250(f3(a65),f3(a43))))
% 60.70/60.73 [96]P9(a61,f120(f250(f3(a76),f3(a43))))
% 60.70/60.73 [97]P9(a62,f120(f250(f3(a87),f3(a43))))
% 60.70/60.73 [98]P9(a63,f120(f250(f3(a98),f3(a43))))
% 60.70/60.73 [99]P9(a64,f120(f250(f3(a109),f3(a43))))
% 60.70/60.73 [100]P9(a66,f120(f250(f3(a2),f3(a54))))
% 60.70/60.73 [101]P9(a67,f120(f250(f3(a1),f3(a54))))
% 60.70/60.73 [102]P9(a68,f120(f250(f3(a4),f3(a54))))
% 60.70/60.73 [103]P9(a69,f120(f250(f3(a43),f3(a54))))
% 60.70/60.73 [104]P9(a70,f120(f250(f3(a54),f3(a54))))
% 60.70/60.73 [105]P9(a71,f120(f250(f3(a65),f3(a54))))
% 60.70/60.73 [106]P9(a72,f120(f250(f3(a76),f3(a54))))
% 60.70/60.73 [107]P9(a73,f120(f250(f3(a87),f3(a54))))
% 60.70/60.73 [108]P9(a74,f120(f250(f3(a98),f3(a54))))
% 60.70/60.73 [109]P9(a75,f120(f250(f3(a109),f3(a54))))
% 60.70/60.73 [110]P9(a77,f120(f250(f3(a2),f3(a65))))
% 60.70/60.73 [111]P9(a78,f120(f250(f3(a1),f3(a65))))
% 60.70/60.73 [112]P9(a79,f120(f250(f3(a4),f3(a65))))
% 60.70/60.73 [113]P9(a80,f120(f250(f3(a43),f3(a65))))
% 60.70/60.73 [114]P9(a81,f120(f250(f3(a54),f3(a65))))
% 60.70/60.73 [115]P9(a82,f120(f250(f3(a65),f3(a65))))
% 60.70/60.73 [116]P9(a83,f120(f250(f3(a76),f3(a65))))
% 60.70/60.73 [117]P9(a84,f120(f250(f3(a87),f3(a65))))
% 60.70/60.73 [118]P9(a85,f120(f250(f3(a98),f3(a65))))
% 60.70/60.73 [119]P9(a86,f120(f250(f3(a109),f3(a65))))
% 60.70/60.73 [120]P9(a88,f120(f250(f3(a2),f3(a76))))
% 60.70/60.73 [121]P9(a89,f120(f250(f3(a1),f3(a76))))
% 60.70/60.73 [122]P9(a90,f120(f250(f3(a4),f3(a76))))
% 60.70/60.73 [123]P9(a91,f120(f250(f3(a43),f3(a76))))
% 60.70/60.73 [124]P9(a92,f120(f250(f3(a54),f3(a76))))
% 60.70/60.73 [125]P9(a93,f120(f250(f3(a65),f3(a76))))
% 60.70/60.73 [126]P9(a94,f120(f250(f3(a76),f3(a76))))
% 60.70/60.73 [127]P9(a95,f120(f250(f3(a87),f3(a76))))
% 60.70/60.73 [128]P9(a96,f120(f250(f3(a98),f3(a76))))
% 60.70/60.73 [129]P9(a97,f120(f250(f3(a109),f3(a76))))
% 60.70/60.73 [130]P9(a99,f120(f250(f3(a2),f3(a87))))
% 60.70/60.73 [131]P9(a100,f120(f250(f3(a1),f3(a87))))
% 60.70/60.73 [132]P9(a101,f120(f250(f3(a4),f3(a87))))
% 60.70/60.73 [133]P9(a102,f120(f250(f3(a43),f3(a87))))
% 60.70/60.73 [134]P9(a103,f120(f250(f3(a54),f3(a87))))
% 60.70/60.73 [135]P9(a104,f120(f250(f3(a65),f3(a87))))
% 60.70/60.73 [136]P9(a105,f120(f250(f3(a76),f3(a87))))
% 60.70/60.73 [137]P9(a106,f120(f250(f3(a87),f3(a87))))
% 60.70/60.73 [138]P9(a107,f120(f250(f3(a98),f3(a87))))
% 60.70/60.73 [139]P9(a108,f120(f250(f3(a109),f3(a87))))
% 60.70/60.73 [140]P9(a110,f120(f250(f3(a2),f3(a98))))
% 60.70/60.73 [141]P9(a111,f120(f250(f3(a1),f3(a98))))
% 60.70/60.73 [142]P9(a112,f120(f250(f3(a4),f3(a98))))
% 60.70/60.73 [143]P9(a113,f120(f250(f3(a43),f3(a98))))
% 60.70/60.73 [144]P9(a114,f120(f250(f3(a54),f3(a98))))
% 60.70/60.73 [145]P9(a115,f120(f250(f3(a65),f3(a98))))
% 60.70/60.73 [146]P9(a116,f120(f250(f3(a76),f3(a98))))
% 60.70/60.73 [147]P9(a117,f120(f250(f3(a87),f3(a98))))
% 60.70/60.73 [148]P9(a118,f120(f250(f3(a98),f3(a98))))
% 60.70/60.73 [149]P9(a119,f120(f250(f3(a109),f3(a98))))
% 60.70/60.73 [150]P9(a122,f120(f250(f3(a2),f3(a109))))
% 60.70/60.73 [151]P9(a123,f120(f250(f3(a1),f3(a109))))
% 60.70/60.73 [152]P9(a124,f120(f250(f3(a4),f3(a109))))
% 60.70/60.73 [153]P9(a125,f120(f250(f3(a43),f3(a109))))
% 60.70/60.73 [154]P9(a126,f120(f250(f3(a54),f3(a109))))
% 60.70/60.73 [155]P9(a127,f120(f250(f3(a65),f3(a109))))
% 60.70/60.73 [156]P9(a128,f120(f250(f3(a76),f3(a109))))
% 60.70/60.73 [157]P9(a129,f120(f250(f3(a87),f3(a109))))
% 60.70/60.73 [158]P9(a130,f120(f250(f3(a98),f3(a109))))
% 60.70/60.73 [159]P9(a131,f120(f250(f3(a109),f3(a109))))
% 60.70/60.73 [160]P9(a134,f132(f250(f3(a2),f3(a1))))
% 60.70/60.73 [161]P9(a135,f132(f250(f3(a1),f3(a1))))
% 60.70/60.73 [162]P9(a146,f132(f250(f3(a4),f3(a1))))
% 60.70/60.73 [163]P9(a157,f132(f250(f3(a43),f3(a1))))
% 60.70/60.73 [164]P9(a167,f132(f250(f3(a54),f3(a1))))
% 60.70/60.73 [165]P9(a168,f132(f250(f3(a65),f3(a1))))
% 60.70/60.73 [166]P9(a169,f132(f250(f3(a76),f3(a1))))
% 60.70/60.73 [167]P9(a170,f132(f250(f3(a87),f3(a1))))
% 60.70/60.73 [168]P9(a171,f132(f250(f3(a98),f3(a1))))
% 60.70/60.73 [169]P9(a172,f132(f250(f3(a109),f3(a1))))
% 60.70/60.73 [170]P9(a174,f132(f250(f3(a2),f3(a4))))
% 60.70/60.73 [171]P9(a175,f132(f250(f3(a1),f3(a4))))
% 60.70/60.73 [172]P9(a176,f132(f250(f3(a4),f3(a4))))
% 60.70/60.73 [173]P9(a177,f132(f250(f3(a43),f3(a4))))
% 60.70/60.73 [174]P9(a178,f132(f250(f3(a54),f3(a4))))
% 60.70/60.73 [175]P9(a179,f132(f250(f3(a65),f3(a4))))
% 60.70/60.73 [176]P9(a180,f132(f250(f3(a76),f3(a4))))
% 60.70/60.73 [177]P9(a181,f132(f250(f3(a87),f3(a4))))
% 60.70/60.73 [178]P9(a182,f132(f250(f3(a98),f3(a4))))
% 60.70/60.73 [179]P9(a183,f132(f250(f3(a109),f3(a4))))
% 60.70/60.73 [180]P9(a185,f132(f250(f3(a2),f3(a43))))
% 60.70/60.73 [181]P9(a186,f132(f250(f3(a1),f3(a43))))
% 60.70/60.73 [182]P9(a187,f132(f250(f3(a4),f3(a43))))
% 60.70/60.73 [183]P9(a188,f132(f250(f3(a43),f3(a43))))
% 60.70/60.73 [184]P9(a189,f132(f250(f3(a54),f3(a43))))
% 60.70/60.73 [185]P9(a190,f132(f250(f3(a65),f3(a43))))
% 60.70/60.73 [186]P9(a191,f132(f250(f3(a76),f3(a43))))
% 60.70/60.73 [187]P9(a192,f132(f250(f3(a87),f3(a43))))
% 60.70/60.73 [188]P9(a193,f132(f250(f3(a98),f3(a43))))
% 60.70/60.73 [189]P9(a194,f132(f250(f3(a109),f3(a43))))
% 60.70/60.73 [190]P9(a196,f132(f250(f3(a2),f3(a54))))
% 60.70/60.73 [191]P9(a197,f132(f250(f3(a1),f3(a54))))
% 60.70/60.73 [192]P9(a198,f132(f250(f3(a4),f3(a54))))
% 60.70/60.73 [193]P9(a199,f132(f250(f3(a43),f3(a54))))
% 60.70/60.73 [194]P9(a200,f132(f250(f3(a54),f3(a54))))
% 60.70/60.73 [195]P9(a201,f132(f250(f3(a65),f3(a54))))
% 60.70/60.73 [196]P9(a202,f132(f250(f3(a76),f3(a54))))
% 60.70/60.73 [197]P9(a203,f132(f250(f3(a87),f3(a54))))
% 60.70/60.73 [198]P9(a204,f132(f250(f3(a98),f3(a54))))
% 60.70/60.73 [199]P9(a205,f132(f250(f3(a109),f3(a54))))
% 60.70/60.73 [200]P9(a207,f132(f250(f3(a2),f3(a65))))
% 60.70/60.73 [201]P9(a208,f132(f250(f3(a1),f3(a65))))
% 60.70/60.73 [202]P9(a209,f132(f250(f3(a4),f3(a65))))
% 60.70/60.73 [203]P9(a210,f132(f250(f3(a43),f3(a65))))
% 60.70/60.73 [204]P9(a211,f132(f250(f3(a54),f3(a65))))
% 60.70/60.73 [205]P9(a212,f132(f250(f3(a65),f3(a65))))
% 60.70/60.73 [206]P9(a213,f132(f250(f3(a76),f3(a65))))
% 60.70/60.73 [207]P9(a214,f132(f250(f3(a87),f3(a65))))
% 60.70/60.73 [208]P9(a215,f132(f250(f3(a98),f3(a65))))
% 60.70/60.73 [209]P9(a216,f132(f250(f3(a109),f3(a65))))
% 60.70/60.73 [210]P9(a218,f132(f250(f3(a2),f3(a76))))
% 60.70/60.73 [211]P9(a219,f132(f250(f3(a1),f3(a76))))
% 60.70/60.73 [212]P9(a220,f132(f250(f3(a4),f3(a76))))
% 60.70/60.73 [213]P9(a221,f132(f250(f3(a43),f3(a76))))
% 60.70/60.73 [214]P9(a222,f132(f250(f3(a54),f3(a76))))
% 60.70/60.73 [215]P9(a223,f132(f250(f3(a65),f3(a76))))
% 60.70/60.73 [216]P9(a224,f132(f250(f3(a76),f3(a76))))
% 60.70/60.73 [217]P9(a225,f132(f250(f3(a87),f3(a76))))
% 60.70/60.73 [218]P9(a226,f132(f250(f3(a98),f3(a76))))
% 60.70/60.73 [219]P9(a227,f132(f250(f3(a109),f3(a76))))
% 60.70/60.73 [220]P9(a229,f132(f250(f3(a2),f3(a87))))
% 60.70/60.73 [221]P9(a230,f132(f250(f3(a1),f3(a87))))
% 60.70/60.73 [222]P9(a231,f132(f250(f3(a4),f3(a87))))
% 60.70/60.73 [223]P9(a232,f132(f250(f3(a43),f3(a87))))
% 60.70/60.73 [224]P9(a233,f132(f250(f3(a54),f3(a87))))
% 60.70/60.73 [225]P9(a234,f132(f250(f3(a65),f3(a87))))
% 60.70/60.73 [226]P9(a235,f132(f250(f3(a76),f3(a87))))
% 60.70/60.73 [227]P9(a236,f132(f250(f3(a87),f3(a87))))
% 60.70/60.73 [228]P9(a237,f132(f250(f3(a98),f3(a87))))
% 60.70/60.73 [229]P9(a238,f132(f250(f3(a109),f3(a87))))
% 60.70/60.73 [230]P9(a240,f132(f250(f3(a2),f3(a98))))
% 60.70/60.73 [231]P9(a241,f132(f250(f3(a1),f3(a98))))
% 60.70/60.73 [232]P9(a242,f132(f250(f3(a4),f3(a98))))
% 60.70/60.73 [233]P9(a243,f132(f250(f3(a43),f3(a98))))
% 60.70/60.73 [234]P9(a244,f132(f250(f3(a54),f3(a98))))
% 60.70/60.74 [235]P9(a245,f132(f250(f3(a65),f3(a98))))
% 60.70/60.74 [236]P9(a246,f132(f250(f3(a76),f3(a98))))
% 60.70/60.74 [237]P9(a247,f132(f250(f3(a87),f3(a98))))
% 60.70/60.74 [238]P9(a248,f132(f250(f3(a98),f3(a98))))
% 60.70/60.74 [239]P9(a249,f132(f250(f3(a109),f3(a98))))
% 60.70/60.74 [240]P9(a251,f132(f250(f3(a2),f3(a109))))
% 60.70/60.74 [241]P9(a252,f132(f250(f3(a1),f3(a109))))
% 60.70/60.74 [242]P9(a253,f132(f250(f3(a4),f3(a109))))
% 60.70/60.74 [243]P9(a254,f132(f250(f3(a43),f3(a109))))
% 60.70/60.74 [244]P9(a255,f132(f250(f3(a54),f3(a109))))
% 60.70/60.74 [245]P9(a256,f132(f250(f3(a65),f3(a109))))
% 60.70/60.74 [246]P9(a257,f132(f250(f3(a76),f3(a109))))
% 60.70/60.74 [247]P9(a258,f132(f250(f3(a87),f3(a109))))
% 60.70/60.74 [248]P9(a259,f132(f250(f3(a98),f3(a109))))
% 60.70/60.74 [249]P9(a260,f132(f250(f3(a109),f3(a109))))
% 60.70/60.74 [250]P9(a7,f120(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [251]P9(a8,f120(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [252]P9(a9,f120(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [253]P9(a10,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [254]P9(a11,f120(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [255]P9(a12,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [256]P9(a13,f120(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [257]P9(a14,f120(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [258]P9(a15,f120(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [259]P9(a16,f120(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [260]P9(a18,f120(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [261]P9(a19,f120(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [262]P9(a20,f120(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [263]P9(a21,f120(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [264]P9(a22,f120(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [265]P9(a23,f120(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [266]P9(a24,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [267]P9(a25,f120(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [268]P9(a26,f120(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [269]P9(a27,f120(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [270]P9(a29,f120(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [271]P9(a30,f120(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [272]P9(a31,f120(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [273]P9(a32,f120(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [274]P9(a33,f120(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [275]P9(a34,f120(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [276]P9(a35,f120(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [277]P9(a36,f120(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [278]P9(a136,f132(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [279]P9(a137,f132(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [280]P9(a138,f132(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [281]P9(a139,f132(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [282]P9(a140,f132(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [283]P9(a141,f132(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [284]P9(a142,f132(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [285]P9(a143,f132(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [286]P9(a144,f132(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [287]P9(a145,f132(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 60.70/60.74 [288]P9(a147,f132(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [289]P9(a148,f132(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [290]P9(a149,f132(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [291]P9(a150,f132(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [292]P9(a151,f132(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [293]P9(a152,f132(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [294]P9(a153,f132(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [295]P9(a154,f132(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [296]P9(a155,f132(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [297]P9(a156,f132(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 60.70/60.74 [298]P9(a158,f132(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [299]P9(a159,f132(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [300]P9(a160,f132(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [301]P9(a161,f132(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [302]P9(a162,f132(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [303]P9(a163,f132(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [304]P9(a164,f132(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [305]P9(a165,f132(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [306]P9(a166,f132(f250(f3(a98),f250(f3(a4),f3(a1)))))
% 60.70/60.74 [410]P7(f3(x4101))+~P1(f3(x4101))
% 60.70/60.74 [408]~E(x4081,x4082)+P3(x4081,x4082)
% 60.70/60.74 [409]~P4(x4092,x4091)+~E(x4091,x4092)
% 60.70/60.74 [412]~P4(x4121,x4122)+P3(x4121,x4122)
% 60.70/60.74 [414]~P4(x4142,x4141)+~P4(x4141,x4142)
% 60.70/60.74 [415]~P7(x4152)+P7(f250(f3(x4151),x4152))
% 60.70/60.74 [425]~P5(x4253,x4251,x4252)+P10(x4251,x4252,x4253)
% 60.70/60.74 [426]~P10(x4262,x4263,x4261)+P5(x4261,x4262,x4263)
% 60.70/60.74 [416]~P7(x4163)+P8(f3(x4161),f250(f3(x4162),x4163))
% 60.70/60.74 [421]~P8(x4212,x4214)+P8(f250(f3(x4211),x4212),f250(f3(x4213),x4214))
% 60.70/60.74 [435]P6(f3(x4351),f250(f3(x4352),x4353),f3(x4354),f250(f3(x4355),x4356))+~P6(f3(x4351),f3(x4354),f250(f3(x4352),x4353),f250(f3(x4355),x4356))
% 60.70/60.74 [411]P4(x4112,x4111)+P4(x4111,x4112)+E(x4111,x4112)
% 60.70/60.74 [413]P4(x4131,x4132)+~P3(x4131,x4132)+E(x4131,x4132)
% 60.70/60.74 [423]P3(x4231,x4232)+~P4(x4231,x4233)+~P10(x4232,a1,x4233)
% 60.70/60.74 [420]P8(f3(x4201),f3(x4202))+~P8(f3(x4203),f3(x4202))+~P8(f3(x4201),f3(x4203))
% 60.70/60.74 [422]P10(x4221,x4222,a2)+~P9(x4221,f120(x4223))+~P9(x4222,f132(x4223))
% 60.70/60.74 [424]~P7(x4242)+~P8(f3(x4241),f3(x4243))+P8(f250(f3(x4241),x4242),f250(f3(x4243),x4242))
% 60.70/60.74 [427]~P10(x4273,x4274,x4271)+E(x4271,x4272)+~P10(x4273,x4274,x4272)
% 60.70/60.74 [428]~P10(x4283,x4281,x4284)+E(x4281,x4282)+~P10(x4283,x4282,x4284)
% 60.70/60.74 [429]~P10(x4291,x4293,x4294)+E(x4291,x4292)+~P10(x4292,x4293,x4294)
% 60.70/60.74 [417]P4(x4171,x4172)+~P9(x4172,f120(x4173))+~P9(x4171,f132(x4174))
% 60.70/60.74 [436]P6(f3(x4361),f3(x4362),f3(x4363),f3(x4364))+~P2(f3(x4365),f3(x4361),f3(x4364),f3(a2))+~P2(f3(x4362),f3(x4363),f3(x4365),f3(a2))
% 60.70/60.74 [418]P4(x4181,x4182)+~P8(x4183,x4184)+~P9(x4182,f132(x4183))+~P9(x4181,f132(x4184))
% 60.70/60.74 [419]P4(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f120(x4194))+~P9(x4191,f120(x4193))
% 60.70/60.74 [430]~P10(x4302,x4301,x4303)+P10(x4301,x4302,x4303)+~P9(x4302,f120(x4304))+~P9(x4301,f132(x4305))
% 60.70/60.74 [437]~P2(f3(x4375),f3(x4371),f3(x4374),f3(x4376))+~P2(f3(x4372),f3(x4373),f3(x4375),f3(x4377))+~P2(f3(x4377),f3(x4376),f3(a1),f3(a2))+P6(f3(x4371),f3(x4372),f3(x4373),f250(f3(x4374),f3(a1)))
% 60.70/60.74 [431]P10(x4311,x4312,x4313)+~P6(f3(a2),x4316,x4315,x4314)+~P9(x4313,f120(x4314))+~P9(x4312,f120(x4315))+~P9(x4311,f120(x4316))
% 60.70/60.74 [432]P10(x4321,x4322,x4323)+~P6(f3(a2),x4326,x4325,x4324)+~P9(x4323,f132(x4324))+~P9(x4322,f132(x4325))+~P9(x4321,f132(x4326))
% 60.70/60.74 [433]P10(x4331,x4332,x4333)+~P8(x4334,x4335)+~P6(f3(a2),x4334,x4336,x4335)+~P9(x4332,f132(x4334))+~P9(x4331,f120(x4335))+~P9(x4333,f120(x4336))
% 60.70/60.74 [434]P10(x4341,x4342,x4343)+~P8(x4344,x4345)+~P6(f3(a2),x4344,x4346,x4345)+~P9(x4342,f132(x4345))+~P9(x4341,f120(x4344))+~P9(x4343,f132(x4346))
% 60.70/60.74 [438]~P7(x4386)+~P7(x4384)+~P2(f3(x4388),f3(x4381),f3(x4385),f3(x4389))+~P2(f3(x4382),f3(x4383),f3(x4388),f3(x43810))+~P6(f3(x4387),f3(a2),x4384,x4386)+~P2(f3(x43810),f3(x4389),f3(x4387),f3(a2))+P6(f3(x4381),f3(x4382),f250(f3(x4383),x4384),f250(f3(x4385),x4386))
% 60.70/60.74 [439]~P7(x4397)+~P7(x4395)+~P7(x4393)+~P6(f3(x4398),x4393,x4395,x4397)+~P2(f3(x4399),f3(x4391),f3(x4396),f3(x43910))+~P2(f3(x4392),f3(x4394),f3(x4399),f3(x43911))+~P2(f3(x43911),f3(x43910),f3(x4398),f3(a2))+P6(f3(x4391),f250(f3(x4392),x4393),f250(f3(x4394),x4395),f250(f3(x4396),x4397))
% 60.70/60.74 %EqnAxiom
% 60.70/60.74 [1]E(x11,x11)
% 60.70/60.74 [2]E(x22,x21)+~E(x21,x22)
% 60.70/60.74 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.70/60.74 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 60.70/60.74 [5]~E(x51,x52)+E(f250(x51,x53),f250(x52,x53))
% 60.70/60.74 [6]~E(x61,x62)+E(f250(x63,x61),f250(x63,x62))
% 60.70/60.74 [7]~E(x71,x72)+E(f132(x71),f132(x72))
% 60.70/60.74 [8]~E(x81,x82)+E(f120(x81),f120(x82))
% 60.70/60.74 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 60.70/60.74 [10]P2(x102,x103,x104,x105)+~E(x101,x102)+~P2(x101,x103,x104,x105)
% 60.70/60.74 [11]P2(x113,x112,x114,x115)+~E(x111,x112)+~P2(x113,x111,x114,x115)
% 60.70/60.74 [12]P2(x123,x124,x122,x125)+~E(x121,x122)+~P2(x123,x124,x121,x125)
% 60.70/60.74 [13]P2(x133,x134,x135,x132)+~E(x131,x132)+~P2(x133,x134,x135,x131)
% 60.70/60.74 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 60.70/60.74 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 60.70/60.74 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 60.70/60.74 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 60.70/60.74 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 60.70/60.74 [19]P10(x192,x193,x194)+~E(x191,x192)+~P10(x191,x193,x194)
% 60.70/60.74 [20]P10(x203,x202,x204)+~E(x201,x202)+~P10(x203,x201,x204)
% 60.70/60.74 [21]P10(x213,x214,x212)+~E(x211,x212)+~P10(x213,x214,x211)
% 60.70/60.74 [22]P4(x222,x223)+~E(x221,x222)+~P4(x221,x223)
% 60.70/60.74 [23]P4(x233,x232)+~E(x231,x232)+~P4(x233,x231)
% 60.70/60.74 [24]P8(x242,x243)+~E(x241,x242)+~P8(x241,x243)
% 60.70/60.74 [25]P8(x253,x252)+~E(x251,x252)+~P8(x253,x251)
% 60.70/60.74 [26]P3(x262,x263)+~E(x261,x262)+~P3(x261,x263)
% 60.70/60.74 [27]P3(x273,x272)+~E(x271,x272)+~P3(x273,x271)
% 60.70/60.74 [28]P9(x282,x283)+~E(x281,x282)+~P9(x281,x283)
% 60.70/60.74 [29]P9(x293,x292)+~E(x291,x292)+~P9(x293,x291)
% 60.70/60.74 [30]P5(x302,x303,x304)+~E(x301,x302)+~P5(x301,x303,x304)
% 60.70/60.74 [31]P5(x313,x312,x314)+~E(x311,x312)+~P5(x313,x311,x314)
% 60.70/60.74 [32]P5(x323,x324,x322)+~E(x321,x322)+~P5(x323,x324,x321)
% 60.70/60.74
% 60.70/60.74 %-------------------------------------------
% 60.70/60.74 cnf(441,plain,
% 60.70/60.74 (~P4(x4411,x4411)),
% 60.70/60.74 inference(equality_inference,[],[409])).
% 60.70/60.74 cnf(444,plain,
% 60.70/60.74 (P10(a1,a121,a2)),
% 60.70/60.74 inference(scs_inference,[],[407,52,61,425,422])).
% 60.70/60.74 cnf(448,plain,
% 60.70/60.74 (P4(a121,a2)),
% 60.70/60.74 inference(scs_inference,[],[407,51,52,61,307,425,422,436,417])).
% 60.70/60.74 cnf(450,plain,
% 60.70/60.74 (~E(a121,a2)),
% 60.70/60.74 inference(scs_inference,[],[407,51,52,61,441,307,425,422,436,417,22])).
% 60.70/60.74 cnf(451,plain,
% 60.70/60.74 (~P4(x4511,x4511)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(453,plain,
% 60.70/60.74 (~P4(x4531,x4531)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(454,plain,
% 60.70/60.74 (P10(a121,a1,a2)),
% 60.70/60.74 inference(scs_inference,[],[407,51,52,61,441,451,307,425,422,436,417,22,23,430])).
% 60.70/60.74 cnf(456,plain,
% 60.70/60.74 (~P8(f3(a1),f3(a1))),
% 60.70/60.74 inference(scs_inference,[],[407,51,52,61,441,451,453,307,425,422,436,417,22,23,430,418])).
% 60.70/60.74 cnf(457,plain,
% 60.70/60.74 (~P4(x4571,x4571)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(459,plain,
% 60.70/60.74 (~P8(f3(a2),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[407,51,52,61,441,451,453,457,307,425,422,436,417,22,23,430,418,419])).
% 60.70/60.74 cnf(467,plain,
% 60.70/60.74 (~P8(f3(a1),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[407,42,51,52,61,441,451,453,457,307,425,422,436,417,22,23,430,418,419,431,414,19,420])).
% 60.70/60.74 cnf(482,plain,
% 60.70/60.74 (P10(a4,a133,a2)),
% 60.70/60.74 inference(scs_inference,[],[53,62,422])).
% 60.70/60.74 cnf(484,plain,
% 60.70/60.74 (~P8(f3(a4),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,422,420])).
% 60.70/60.74 cnf(487,plain,
% 60.70/60.74 (P4(a133,a4)),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,42,456,422,420,24,417])).
% 60.70/60.74 cnf(491,plain,
% 60.70/60.74 (~E(a4,a133)),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,42,456,441,308,307,422,420,24,417,436,23])).
% 60.70/60.74 cnf(492,plain,
% 60.70/60.74 (~P4(x4921,x4921)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(493,plain,
% 60.70/60.74 (~E(f3(a4),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,42,456,441,308,307,422,420,24,417,436,23,25])).
% 60.70/60.74 cnf(495,plain,
% 60.70/60.74 (~P4(x4951,x4951)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(496,plain,
% 60.70/60.74 (P10(a133,a4,a2)),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,42,456,441,492,308,307,422,420,24,417,436,23,25,22,430])).
% 60.70/60.74 cnf(498,plain,
% 60.70/60.74 (~P8(f3(a4),f3(a4))),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,42,456,441,492,495,308,307,422,420,24,417,436,23,25,22,430,419])).
% 60.70/60.74 cnf(499,plain,
% 60.70/60.74 (~P4(x4991,x4991)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(501,plain,
% 60.70/60.74 (~P8(f3(a43),f3(a43))),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,63,42,456,441,492,495,499,308,307,422,420,24,417,436,23,25,22,430,419,418])).
% 60.70/60.74 cnf(504,plain,
% 60.70/60.74 (~P4(a4,a133)),
% 60.70/60.74 inference(scs_inference,[],[467,43,53,62,63,42,456,441,492,495,499,308,307,422,420,24,417,436,23,25,22,430,419,418,414])).
% 60.70/60.74 cnf(519,plain,
% 60.70/60.74 (~E(a4,a2)),
% 60.70/60.74 inference(scs_inference,[],[493,4])).
% 60.70/60.74 cnf(520,plain,
% 60.70/60.74 (~P8(f3(a43),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[484,493,44,4,420])).
% 60.70/60.74 cnf(524,plain,
% 60.70/60.74 (P4(a184,a2)),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,4,420,422,417])).
% 60.70/60.74 cnf(528,plain,
% 60.70/60.74 (~E(a2,a184)),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,441,309,307,4,420,422,417,436,23])).
% 60.70/60.74 cnf(529,plain,
% 60.70/60.74 (~P4(x5291,x5291)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(530,plain,
% 60.70/60.74 (~E(f3(a4),f3(a43))),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,501,441,309,307,4,420,422,417,436,23,24])).
% 60.70/60.74 cnf(531,plain,
% 60.70/60.74 (~E(f3(a43),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,501,441,309,307,4,420,422,417,436,23,24,25])).
% 60.70/60.74 cnf(533,plain,
% 60.70/60.74 (~P4(x5331,x5331)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(534,plain,
% 60.70/60.74 (~P8(f3(a54),f3(a54))),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,501,441,529,533,309,307,4,420,422,417,436,23,24,25,22,419])).
% 60.70/60.74 cnf(535,plain,
% 60.70/60.74 (~P4(x5351,x5351)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(539,plain,
% 60.70/60.74 (~P8(f3(a65),f3(a65))),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,65,501,441,529,533,535,309,307,4,420,422,417,436,23,24,25,22,419,430,418])).
% 60.70/60.74 cnf(542,plain,
% 60.70/60.74 (~P4(a2,a184)),
% 60.70/60.74 inference(scs_inference,[],[51,484,493,44,55,64,65,501,441,529,533,535,309,307,4,420,422,417,436,23,24,25,22,419,430,418,414])).
% 60.70/60.74 cnf(550,plain,
% 60.70/60.74 (~E(a4,a43)),
% 60.70/60.74 inference(scs_inference,[],[530,4])).
% 60.70/60.74 cnf(553,plain,
% 60.70/60.74 (~P8(f3(a54),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,520,530,45,524,4,423,420])).
% 60.70/60.74 cnf(557,plain,
% 60.70/60.74 (P4(a206,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,520,530,45,57,66,524,4,423,420,422,417])).
% 60.70/60.74 cnf(562,plain,
% 60.70/60.74 (~P4(x5621,x5621)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(563,plain,
% 60.70/60.74 (~E(f3(a43),f3(a54))),
% 60.70/60.74 inference(scs_inference,[],[454,51,520,530,45,57,66,524,534,441,310,307,4,423,420,422,417,436,23,24])).
% 60.70/60.74 cnf(564,plain,
% 60.70/60.74 (~E(f3(a54),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,520,530,45,57,66,524,534,441,310,307,4,423,420,422,417,436,23,24,25])).
% 60.70/60.74 cnf(566,plain,
% 60.70/60.74 (~P4(x5661,x5661)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(567,plain,
% 60.70/60.74 (~P8(f3(a76),f3(a76))),
% 60.70/60.74 inference(scs_inference,[],[454,51,520,530,45,57,66,524,534,441,562,566,310,307,4,423,420,422,417,436,23,24,25,22,419])).
% 60.70/60.74 cnf(568,plain,
% 60.70/60.74 (~P4(x5681,x5681)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(572,plain,
% 60.70/60.74 (~P8(f3(a87),f3(a87))),
% 60.70/60.74 inference(scs_inference,[],[454,51,520,530,45,57,66,67,524,534,441,562,566,568,310,307,4,423,420,422,417,436,23,24,25,22,419,430,418])).
% 60.70/60.74 cnf(592,plain,
% 60.70/60.74 (~P8(f3(a65),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,531,553,46,557,4,423,420])).
% 60.70/60.74 cnf(594,plain,
% 60.70/60.74 (P10(a98,a228,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,531,553,46,59,68,557,4,423,420,422])).
% 60.70/60.74 cnf(598,plain,
% 60.70/60.74 (P4(a228,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,531,553,46,59,68,557,311,307,4,423,420,422,436,417])).
% 60.70/60.74 cnf(601,plain,
% 60.70/60.74 (~P4(x6011,x6011)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(603,plain,
% 60.70/60.74 (~P4(x6031,x6031)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(604,plain,
% 60.70/60.74 (~E(f3(a54),f3(a65))),
% 60.70/60.74 inference(scs_inference,[],[454,51,531,553,46,59,68,557,539,441,601,311,307,4,423,420,422,436,417,23,22,24])).
% 60.70/60.74 cnf(605,plain,
% 60.70/60.74 (~E(f3(a65),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,531,553,46,59,68,557,539,441,601,311,307,4,423,420,422,436,417,23,22,24,25])).
% 60.70/60.74 cnf(606,plain,
% 60.70/60.74 (~P8(f3(a98),f3(a98))),
% 60.70/60.74 inference(scs_inference,[],[454,51,531,553,46,59,68,557,539,441,601,603,311,307,4,423,420,422,436,417,23,22,24,25,419])).
% 60.70/60.74 cnf(607,plain,
% 60.70/60.74 (~P4(x6071,x6071)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(611,plain,
% 60.70/60.74 (~P8(f3(a109),f3(a109))),
% 60.70/60.74 inference(scs_inference,[],[454,51,531,553,46,59,68,69,557,539,441,601,603,607,311,307,4,423,420,422,436,417,23,22,24,25,419,430,418])).
% 60.70/60.74 cnf(629,plain,
% 60.70/60.74 (~E(a43,a54)),
% 60.70/60.74 inference(scs_inference,[],[563,4])).
% 60.70/60.74 cnf(632,plain,
% 60.70/60.74 (~P8(f3(a76),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,563,592,47,598,4,423,420])).
% 60.70/60.74 cnf(638,plain,
% 60.70/60.74 (P4(a134,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,563,592,47,160,70,598,312,307,4,423,420,422,436,417])).
% 60.70/60.74 cnf(641,plain,
% 60.70/60.74 (~P4(x6411,x6411)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(642,plain,
% 60.70/60.74 (~E(f3(a65),f3(a76))),
% 60.70/60.74 inference(scs_inference,[],[454,51,563,592,47,160,70,598,567,441,312,307,4,423,420,422,436,417,23,24])).
% 60.70/60.74 cnf(645,plain,
% 60.70/60.74 (~E(f3(a76),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,563,592,47,160,70,598,567,441,641,312,307,4,423,420,422,436,417,23,24,22,25])).
% 60.70/60.74 cnf(669,plain,
% 60.70/60.74 (P3(a134,a121)),
% 60.70/60.74 inference(scs_inference,[],[454,564,638,4,423])).
% 60.70/60.74 cnf(671,plain,
% 60.70/60.74 (~P8(f3(a87),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,564,632,48,638,4,423,420])).
% 60.70/60.74 cnf(677,plain,
% 60.70/60.74 (P4(a146,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,564,632,48,162,72,638,313,307,4,423,420,422,436,417])).
% 60.70/60.74 cnf(680,plain,
% 60.70/60.74 (~P4(x6801,x6801)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(682,plain,
% 60.70/60.74 (~P4(x6821,x6821)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(683,plain,
% 60.70/60.74 (~E(f3(a76),f3(a87))),
% 60.70/60.74 inference(scs_inference,[],[454,51,564,632,48,162,72,572,638,441,680,313,307,4,423,420,422,436,417,23,22,24])).
% 60.70/60.74 cnf(684,plain,
% 60.70/60.74 (~E(f3(a87),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,564,632,48,162,72,572,638,441,680,313,307,4,423,420,422,436,417,23,22,24,25])).
% 60.70/60.74 cnf(686,plain,
% 60.70/60.74 (~P4(x6861,x6861)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(696,plain,
% 60.70/60.74 (E(a1,a4)+~E(a133,a121)),
% 60.70/60.74 inference(scs_inference,[],[454,496,51,564,632,48,162,163,72,572,638,441,680,682,686,313,307,4,423,420,422,436,417,23,22,24,25,419,430,418,414,19,428])).
% 60.70/60.74 cnf(702,plain,
% 60.70/60.74 (~E(a54,a65)),
% 60.70/60.74 inference(scs_inference,[],[604,4])).
% 60.70/60.74 cnf(705,plain,
% 60.70/60.74 (~P8(f3(a98),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,604,671,49,677,4,423,420])).
% 60.70/60.74 cnf(711,plain,
% 60.70/60.74 (P4(a167,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,604,671,49,164,74,677,314,307,4,423,420,422,436,417])).
% 60.70/60.74 cnf(714,plain,
% 60.70/60.74 (~P4(x7141,x7141)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(715,plain,
% 60.70/60.74 (~E(f3(a87),f3(a98))),
% 60.70/60.74 inference(scs_inference,[],[454,51,604,671,49,164,74,677,606,441,314,307,4,423,420,422,436,417,23,24])).
% 60.70/60.74 cnf(718,plain,
% 60.70/60.74 (~E(f3(a98),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,604,671,49,164,74,677,606,441,714,314,307,4,423,420,422,436,417,23,24,22,25])).
% 60.70/60.74 cnf(742,plain,
% 60.70/60.74 (P4(a168,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,605,705,50,165,75,711,315,307,4,422,423,420,436,417])).
% 60.70/60.74 cnf(745,plain,
% 60.70/60.74 (~P4(x7451,x7451)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(748,plain,
% 60.70/60.74 (~E(f3(a98),f3(a109))),
% 60.70/60.74 inference(scs_inference,[],[454,51,605,705,50,165,75,611,711,441,745,315,307,4,422,423,420,436,417,23,22,24])).
% 60.70/60.74 cnf(749,plain,
% 60.70/60.74 (~E(f3(a109),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,605,705,50,165,75,611,711,441,745,315,307,4,422,423,420,436,417,23,22,24,25])).
% 60.70/60.74 cnf(750,plain,
% 60.70/60.74 (P10(a168,a38,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,605,705,50,165,75,611,711,441,745,315,307,4,422,423,420,436,417,23,22,24,25,430])).
% 60.70/60.74 cnf(765,plain,
% 60.70/60.74 (~P8(f3(a4),f3(a1))),
% 60.70/60.74 inference(scs_inference,[],[642,43,498,4,420])).
% 60.70/60.74 cnf(767,plain,
% 60.70/60.74 (P3(a168,a121)),
% 60.70/60.74 inference(scs_inference,[],[454,642,43,498,742,4,420,423])).
% 60.70/60.74 cnf(773,plain,
% 60.70/60.74 (P4(a170,a2)),
% 60.70/60.74 inference(scs_inference,[],[454,51,642,167,77,43,498,742,316,307,4,420,423,422,436,417])).
% 60.70/60.74 cnf(775,plain,
% 60.70/60.74 (~E(f3(a1),f3(a4))),
% 60.70/60.74 inference(scs_inference,[],[454,51,642,167,77,43,498,742,316,307,4,420,423,422,436,417,24])).
% 60.70/60.74 cnf(777,plain,
% 60.70/60.74 (~P4(x7771,x7771)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(779,plain,
% 60.70/60.74 (~P4(x7791,x7791)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(780,plain,
% 60.70/60.74 (~E(f3(a1),f3(a2))),
% 60.70/60.74 inference(scs_inference,[],[454,51,642,167,77,43,42,459,498,742,441,777,316,307,4,420,423,422,436,417,24,23,22,25])).
% 60.70/60.74 cnf(782,plain,
% 60.70/60.74 (~P4(x7821,x7821)),
% 60.70/60.74 inference(rename_variables,[],[441])).
% 60.70/60.74 cnf(791,plain,
% 60.70/60.74 (P9(x7911,f120(f3(a43)))+~E(a43,x7911)),
% 60.70/60.74 inference(scs_inference,[],[454,51,642,54,167,169,78,77,43,42,459,498,742,441,777,779,782,316,307,4,420,423,422,436,417,24,23,22,25,419,430,418,414,28])).
% 60.70/60.74 cnf(806,plain,
% 60.70/60.74 (P3(a170,a121)),
% 60.70/60.74 inference(scs_inference,[],[454,645,168,78,773,4,422,423])).
% 60.70/60.74 cnf(808,plain,
% 60.70/60.74 (~P8(f3(a43),f3(a4))),
% 60.70/60.74 inference(scs_inference,[],[454,645,168,78,44,773,501,4,422,423,420])).
% 60.70/60.74 cnf(812,plain,
% 60.70/60.74 (P4(a171,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,645,168,78,44,773,501,317,4,422,423,420,436,417])).
% 60.70/60.75 cnf(814,plain,
% 60.70/60.75 (~E(f3(a2),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,645,765,168,78,44,42,773,501,317,4,422,423,420,436,417,24])).
% 60.70/60.75 cnf(816,plain,
% 60.70/60.75 (~P4(x8161,x8161)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(819,plain,
% 60.70/60.75 (~E(f3(a43),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,645,765,168,78,44,42,773,501,441,816,317,4,422,423,420,436,417,24,22,23,25])).
% 60.70/60.75 cnf(843,plain,
% 60.70/60.75 (~P8(f3(a43),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[683,808,43,4,420])).
% 60.70/60.75 cnf(851,plain,
% 60.70/60.75 (P4(a175,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,683,808,171,81,43,812,318,317,4,420,423,422,436,417])).
% 60.70/60.75 cnf(854,plain,
% 60.70/60.75 (~P4(x8541,x8541)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(855,plain,
% 60.70/60.75 (~E(f3(a1),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,683,808,171,81,43,812,441,318,317,4,420,423,422,436,417,23,24])).
% 60.70/60.75 cnf(858,plain,
% 60.70/60.75 (~E(f3(a54),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,683,808,171,81,45,43,812,441,854,318,317,4,420,423,422,436,417,23,24,22,25])).
% 60.70/60.75 cnf(881,plain,
% 60.70/60.75 (~E(a87,a98)),
% 60.70/60.75 inference(scs_inference,[],[715,4])).
% 60.70/60.75 cnf(886,plain,
% 60.70/60.75 (~P8(f3(a65),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,715,173,83,46,851,539,4,422,423,420])).
% 60.70/60.75 cnf(888,plain,
% 60.70/60.75 (P6(f3(a4),f3(a2),f3(a1),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,715,173,83,46,851,539,319,308,4,422,423,420,436])).
% 60.70/60.75 cnf(890,plain,
% 60.70/60.75 (P4(a177,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,715,173,83,46,851,539,319,308,4,422,423,420,436,417])).
% 60.70/60.75 cnf(893,plain,
% 60.70/60.75 (~P4(x8931,x8931)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(896,plain,
% 60.70/60.75 (~E(f3(a2),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,715,843,173,83,46,42,851,539,441,893,319,308,4,422,423,420,436,417,23,22,24])).
% 60.70/60.75 cnf(897,plain,
% 60.70/60.75 (~E(f3(a54),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,715,843,173,83,46,45,42,851,539,441,893,319,308,4,422,423,420,436,417,23,22,24,25])).
% 60.70/60.75 cnf(923,plain,
% 60.70/60.75 (~P8(f3(a65),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[748,886,45,4,420])).
% 60.70/60.75 cnf(931,plain,
% 60.70/60.75 (P4(a178,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,748,886,174,84,45,890,320,317,4,420,422,423,436,417])).
% 60.70/60.75 cnf(933,plain,
% 60.70/60.75 (~E(f3(a43),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,748,886,174,84,45,890,320,317,4,420,422,423,436,417,24])).
% 60.70/60.75 cnf(935,plain,
% 60.70/60.75 (~P4(x9351,x9351)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(938,plain,
% 60.70/60.75 (~E(f3(a76),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,748,886,174,84,47,45,890,441,935,320,317,4,420,422,423,436,417,24,23,22,25])).
% 60.70/60.75 cnf(957,plain,
% 60.70/60.75 (~P8(f3(a65),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,684,923,44,931,4,423,420])).
% 60.70/60.75 cnf(963,plain,
% 60.70/60.75 (P4(a181,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,684,923,177,87,44,931,321,308,4,423,420,422,436,417])).
% 60.70/60.75 cnf(965,plain,
% 60.70/60.75 (~E(f3(a4),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,684,923,177,87,44,931,321,308,4,423,420,422,436,417,24])).
% 60.70/60.75 cnf(967,plain,
% 60.70/60.75 (~P4(x9671,x9671)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(970,plain,
% 60.70/60.75 (~E(f3(a76),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,684,923,177,87,47,44,931,441,967,321,308,4,423,420,422,436,417,24,22,23,25])).
% 60.70/60.75 cnf(994,plain,
% 60.70/60.75 (~P8(f3(a65),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[718,957,43,4,420])).
% 60.70/60.75 cnf(1002,plain,
% 60.70/60.75 (P4(a183,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,718,957,179,89,43,963,322,317,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1005,plain,
% 60.70/60.75 (~P4(x10051,x10051)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1006,plain,
% 60.70/60.75 (~E(f3(a1),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,718,957,179,89,43,963,441,322,317,4,420,423,422,436,417,22,24])).
% 60.70/60.75 cnf(1008,plain,
% 60.70/60.75 (~P4(x10081,x10081)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1009,plain,
% 60.70/60.75 (~E(f3(a76),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,718,957,179,89,47,43,963,441,1005,322,317,4,420,423,422,436,417,22,24,23,25])).
% 60.70/60.75 cnf(1011,plain,
% 60.70/60.75 (~P4(x10111,x10111)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1026,plain,
% 60.70/60.75 (P9(x10261,f120(f3(a87)))+~E(a87,x10261)),
% 60.70/60.75 inference(scs_inference,[],[454,750,51,718,888,957,767,58,179,180,91,89,47,43,963,441,1005,1008,1011,322,317,4,420,423,422,436,417,22,24,23,25,418,419,430,414,13,413,15,10,20,28])).
% 60.70/60.75 cnf(1032,plain,
% 60.70/60.75 (P7(f250(f3(x10321),f3(a1)))),
% 60.70/60.75 inference(scs_inference,[],[33,410,415])).
% 60.70/60.75 cnf(1036,plain,
% 60.70/60.75 (~P8(f3(a87),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,749,48,1002,572,4,423,420])).
% 60.70/60.75 cnf(1040,plain,
% 60.70/60.75 (P4(a186,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,749,181,91,48,1002,572,4,423,420,422,417])).
% 60.70/60.75 cnf(1044,plain,
% 60.70/60.75 (~E(f3(a2),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,749,994,181,91,48,42,1002,572,323,308,4,423,420,422,417,436,24])).
% 60.70/60.75 cnf(1046,plain,
% 60.70/60.75 (~P4(x10461,x10461)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1049,plain,
% 60.70/60.75 (~E(f3(a76),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,749,994,181,91,48,47,42,1002,572,441,1046,323,308,4,423,420,422,417,436,24,22,23,25])).
% 60.70/60.75 cnf(1074,plain,
% 60.70/60.75 (~E(a1,a4)),
% 60.70/60.75 inference(scs_inference,[],[775,4])).
% 60.70/60.75 cnf(1075,plain,
% 60.70/60.75 (~P8(f3(a87),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[775,1036,47,4,420])).
% 60.70/60.75 cnf(1083,plain,
% 60.70/60.75 (P4(a187,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,775,1036,182,92,47,1040,324,317,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1086,plain,
% 60.70/60.75 (~P4(x10861,x10861)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1088,plain,
% 60.70/60.75 (~P4(x10881,x10881)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1089,plain,
% 60.70/60.75 (~E(f3(a65),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,775,1036,182,92,47,1040,441,1086,324,317,4,420,423,422,436,417,22,23,24])).
% 60.70/60.75 cnf(1090,plain,
% 60.70/60.75 (~E(f3(a98),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,775,1036,182,92,49,47,1040,441,1086,324,317,4,420,423,422,436,417,22,23,24,25])).
% 60.70/60.75 cnf(1094,plain,
% 60.70/60.75 (~P4(x10941,x10941)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1099,plain,
% 60.70/60.75 (~E(a133,a121)),
% 60.70/60.75 inference(scs_inference,[],[454,51,775,1036,182,184,95,92,49,47,1040,441,1086,1088,1094,324,317,4,420,423,422,436,417,22,23,24,25,430,418,419,696])).
% 60.70/60.75 cnf(1110,plain,
% 60.70/60.75 (~P8(f3(a87),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,780,1075,46,1083,4,423,420])).
% 60.70/60.75 cnf(1114,plain,
% 60.70/60.75 (P4(a190,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,780,1075,185,95,46,1083,4,423,420,422,417])).
% 60.70/60.75 cnf(1119,plain,
% 60.70/60.75 (~P4(x11191,x11191)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1122,plain,
% 60.70/60.75 (~E(f3(a54),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,780,1075,185,95,46,1083,441,1119,325,308,4,423,420,422,417,436,23,22,24])).
% 60.70/60.75 cnf(1123,plain,
% 60.70/60.75 (~E(f3(a98),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,780,1075,185,95,46,49,1083,441,1119,325,308,4,423,420,422,417,436,23,22,24,25])).
% 60.70/60.75 cnf(1147,plain,
% 60.70/60.75 (~P8(f3(a87),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[933,1110,45,4,420])).
% 60.70/60.75 cnf(1155,plain,
% 60.70/60.75 (P4(a192,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,933,1110,187,97,45,1114,327,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1158,plain,
% 60.70/60.75 (~P4(x11581,x11581)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1159,plain,
% 60.70/60.75 (~E(f3(a43),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,933,1110,187,97,45,1114,441,327,4,420,423,422,436,417,22,24])).
% 60.70/60.75 cnf(1162,plain,
% 60.70/60.75 (~E(f3(a98),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,933,1110,187,97,49,45,1114,441,1158,327,4,420,423,422,436,417,22,24,23,25])).
% 60.70/60.75 cnf(1191,plain,
% 60.70/60.75 (~P8(f3(a87),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,965,1147,44,1155,4,423,420])).
% 60.70/60.75 cnf(1195,plain,
% 60.70/60.75 (P4(a193,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,965,1147,188,98,44,1155,4,423,420,422,417])).
% 60.70/60.75 cnf(1199,plain,
% 60.70/60.75 (~E(f3(a4),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,965,1147,188,98,44,1155,328,327,4,423,420,422,417,436,24])).
% 60.70/60.75 cnf(1201,plain,
% 60.70/60.75 (~P4(x12011,x12011)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1204,plain,
% 60.70/60.75 (~E(f3(a98),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,965,1147,188,98,49,44,1155,441,1201,328,327,4,423,420,422,417,436,24,23,22,25])).
% 60.70/60.75 cnf(1230,plain,
% 60.70/60.75 (~P8(f3(a87),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[1122,1191,43,4,420])).
% 60.70/60.75 cnf(1238,plain,
% 60.70/60.75 (P4(a197,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1122,1191,191,101,43,1195,329,318,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1241,plain,
% 60.70/60.75 (~P4(x12411,x12411)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1244,plain,
% 60.70/60.75 (~E(f3(a1),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,1122,1191,191,101,43,1195,441,1241,329,318,4,420,423,422,436,417,23,22,24])).
% 60.70/60.75 cnf(1245,plain,
% 60.70/60.75 (~E(f3(a98),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,1122,1191,191,101,49,43,1195,441,1241,329,318,4,420,423,422,436,417,23,22,24,25])).
% 60.70/60.75 cnf(1272,plain,
% 60.70/60.75 (~P8(f3(a54),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[896,45,534,4,420])).
% 60.70/60.75 cnf(1280,plain,
% 60.70/60.75 (P4(a199,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,896,193,103,45,1238,534,330,327,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1283,plain,
% 60.70/60.75 (~P4(x12831,x12831)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1286,plain,
% 60.70/60.75 (~E(f3(a2),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,896,1230,193,103,42,45,1238,534,441,1283,330,327,4,420,423,422,436,417,23,22,24])).
% 60.70/60.75 cnf(1287,plain,
% 60.70/60.75 (~E(f3(a98),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,896,1230,193,103,42,49,45,1238,534,441,1283,330,327,4,420,423,422,436,417,23,22,24,25])).
% 60.70/60.75 cnf(1313,plain,
% 60.70/60.75 (~P8(f3(a54),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[814,1272,44,4,420])).
% 60.70/60.75 cnf(1319,plain,
% 60.70/60.75 (P4(a201,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,814,1272,195,105,44,1280,4,420,423,422,417])).
% 60.70/60.75 cnf(1324,plain,
% 60.70/60.75 (~P4(x13241,x13241)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1327,plain,
% 60.70/60.75 (~E(f3(a4),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,814,1272,195,105,44,1280,441,1324,331,318,4,420,423,422,417,436,22,23,24])).
% 60.70/60.75 cnf(1328,plain,
% 60.70/60.75 (~E(f3(a65),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,814,1272,195,105,46,44,1280,441,1324,331,318,4,420,423,422,417,436,22,23,24,25])).
% 60.70/60.75 cnf(1352,plain,
% 60.70/60.75 (~P8(f3(a54),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[819,1313,43,4,420])).
% 60.70/60.75 cnf(1360,plain,
% 60.70/60.75 (P4(a203,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,819,1313,197,107,43,1319,332,309,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1363,plain,
% 60.70/60.75 (~P4(x13631,x13631)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1366,plain,
% 60.70/60.75 (~E(f3(a1),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,819,1313,197,107,43,1319,441,1363,332,309,4,420,423,422,436,417,23,22,24])).
% 60.70/60.75 cnf(1367,plain,
% 60.70/60.75 (~E(f3(a65),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,819,1313,197,107,46,43,1319,441,1363,332,309,4,420,423,422,436,417,23,22,24,25])).
% 60.70/60.75 cnf(1394,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[1089,50,611,4,420])).
% 60.70/60.75 cnf(1400,plain,
% 60.70/60.75 (P4(a205,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1089,199,109,50,1360,611,4,420,423,422,417])).
% 60.70/60.75 cnf(1405,plain,
% 60.70/60.75 (~P4(x14051,x14051)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1408,plain,
% 60.70/60.75 (~E(f3(a2),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,1089,1352,199,109,50,42,1360,611,441,1405,333,327,4,420,423,422,417,436,22,23,24])).
% 60.70/60.75 cnf(1409,plain,
% 60.70/60.75 (~E(f3(a65),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,1089,1352,199,109,50,46,42,1360,611,441,1405,333,327,4,420,423,422,417,436,22,23,24,25])).
% 60.70/60.75 cnf(1426,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[855,1394,49,4,420])).
% 60.70/60.75 cnf(1428,plain,
% 60.70/60.75 (P3(a205,a121)),
% 60.70/60.75 inference(scs_inference,[],[454,855,1394,49,1400,4,420,423])).
% 60.70/60.75 cnf(1434,plain,
% 60.70/60.75 (P4(a208,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,855,1394,201,111,49,1400,334,318,4,420,423,422,436,417])).
% 60.70/60.75 cnf(1437,plain,
% 60.70/60.75 (~P4(x14371,x14371)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1440,plain,
% 60.70/60.75 (~E(f3(a87),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,855,1394,201,111,49,1400,441,1437,334,318,4,420,423,422,436,417,23,22,24])).
% 60.70/60.75 cnf(1456,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[48,858,1426,4,420])).
% 60.70/60.75 cnf(1462,plain,
% 60.70/60.75 (P4(a210,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,858,1426,203,113,1434,4,420,423,422,417])).
% 60.70/60.75 cnf(1467,plain,
% 60.70/60.75 (~P4(x14671,x14671)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1470,plain,
% 60.70/60.75 (~E(f3(a76),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,858,1426,203,113,1434,441,1467,337,4,420,423,422,417,436,22,23,24])).
% 60.70/60.75 cnf(1494,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[47,897,1456,4,420])).
% 60.70/60.75 cnf(1500,plain,
% 60.70/60.75 (P4(a212,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,47,897,1456,205,115,1462,4,420,423,422,417])).
% 60.70/60.75 cnf(1505,plain,
% 60.70/60.75 (~P4(x15051,x15051)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1508,plain,
% 60.70/60.75 (~E(f3(a65),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,47,897,1456,205,115,1462,441,1505,338,319,4,420,423,422,417,436,23,22,24])).
% 60.70/60.75 cnf(1534,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[46,1470,1494,4,420])).
% 60.70/60.75 cnf(1540,plain,
% 60.70/60.75 (P4(a214,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,46,1470,1494,207,117,1500,4,420,423,422,417])).
% 60.70/60.75 cnf(1545,plain,
% 60.70/60.75 (~P4(x15451,x15451)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1548,plain,
% 60.70/60.75 (~E(f3(a54),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,46,1470,1494,207,117,1500,441,1545,339,337,4,420,423,422,417,436,22,23,24])).
% 60.70/60.75 cnf(1574,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[45,938,1534,4,420])).
% 60.70/60.75 cnf(1580,plain,
% 60.70/60.75 (P4(a216,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,45,938,1534,209,119,1540,4,420,423,422,417])).
% 60.70/60.75 cnf(1585,plain,
% 60.70/60.75 (~P4(x15851,x15851)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1588,plain,
% 60.70/60.75 (~E(f3(a43),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,45,938,1534,209,119,1540,441,1585,340,310,4,420,423,422,417,436,23,22,24])).
% 60.70/60.75 cnf(1615,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[44,970,1574,4,420])).
% 60.70/60.75 cnf(1621,plain,
% 60.70/60.75 (P4(a219,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,44,970,1574,211,121,1580,4,420,423,422,417])).
% 60.70/60.75 cnf(1626,plain,
% 60.70/60.75 (~P4(x16261,x16261)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1629,plain,
% 60.70/60.75 (~E(f3(a4),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,44,970,1574,211,121,1580,441,1626,341,319,4,420,423,422,417,436,22,23,24])).
% 60.70/60.75 cnf(1658,plain,
% 60.70/60.75 (~P8(f3(a109),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,43,1006,1615,1621,4,423,420])).
% 60.70/60.75 cnf(1662,plain,
% 60.70/60.75 (P4(a221,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,43,1006,1615,213,123,1621,4,423,420,422,417])).
% 60.70/60.75 cnf(1667,plain,
% 60.70/60.75 (~P4(x16671,x16671)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1670,plain,
% 60.70/60.75 (~E(f3(a1),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,43,1006,1615,213,123,1621,441,1667,342,337,4,423,420,422,417,436,23,22,24])).
% 60.70/60.75 cnf(1696,plain,
% 60.70/60.75 (~P8(f3(a76),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[47,1440,567,4,420])).
% 60.70/60.75 cnf(1702,plain,
% 60.70/60.75 (P4(a223,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,47,1440,215,125,1662,567,4,420,423,422,417])).
% 60.70/60.75 cnf(1707,plain,
% 60.70/60.75 (~P4(x17071,x17071)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1710,plain,
% 60.70/60.75 (~E(f3(a2),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[454,51,42,47,1440,1658,215,125,1662,567,441,1707,343,310,4,420,423,422,417,436,22,23,24])).
% 60.70/60.75 cnf(1736,plain,
% 60.70/60.75 (~P8(f3(a76),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[46,1508,1696,4,420])).
% 60.70/60.75 cnf(1742,plain,
% 60.70/60.75 (P4(a225,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,46,1508,1696,217,127,1702,4,420,423,422,417])).
% 60.70/60.75 cnf(1746,plain,
% 60.70/60.75 (~E(f3(a87),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,46,1508,1696,217,127,1702,347,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(1748,plain,
% 60.70/60.75 (~P4(x17481,x17481)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1751,plain,
% 60.70/60.75 (~E(f3(a54),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,46,1508,1696,217,127,1702,441,1748,347,4,420,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(1776,plain,
% 60.70/60.75 (~P8(f3(a76),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[45,1548,1736,4,420])).
% 60.70/60.75 cnf(1782,plain,
% 60.70/60.75 (P4(a227,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,45,1548,1736,219,129,1742,4,420,423,422,417])).
% 60.70/60.75 cnf(1786,plain,
% 60.70/60.75 (~E(f3(a87),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,45,1548,1736,219,129,1742,348,338,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(1788,plain,
% 60.70/60.75 (~P4(x17881,x17881)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1791,plain,
% 60.70/60.75 (~E(f3(a43),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,45,1548,1736,219,129,1742,441,1788,348,338,4,420,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(1818,plain,
% 60.70/60.75 (P3(a227,a121)),
% 60.70/60.75 inference(scs_inference,[],[454,1710,1782,4,423])).
% 60.70/60.75 cnf(1820,plain,
% 60.70/60.75 (~P8(f3(a76),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,44,1710,1776,1782,4,423,420])).
% 60.70/60.75 cnf(1824,plain,
% 60.70/60.75 (P4(a230,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,44,1710,1776,221,131,1782,4,423,420,422,417])).
% 60.70/60.75 cnf(1828,plain,
% 60.70/60.75 (~E(f3(a87),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,44,1710,1776,221,131,1782,349,347,4,423,420,422,417,436,25])).
% 60.70/60.75 cnf(1830,plain,
% 60.70/60.75 (~P4(x18301,x18301)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1833,plain,
% 60.70/60.75 (~E(f3(a4),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,44,1710,1776,221,131,1782,441,1830,349,347,4,423,420,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(1859,plain,
% 60.70/60.75 (~P8(f3(a76),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[43,1009,1820,4,420])).
% 60.70/60.75 cnf(1865,plain,
% 60.70/60.75 (P4(a231,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,43,1009,1820,222,132,1824,4,420,423,422,417])).
% 60.70/60.75 cnf(1869,plain,
% 60.70/60.75 (~E(f3(a87),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,43,1009,1820,222,132,1824,350,311,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(1871,plain,
% 60.70/60.75 (~P4(x18711,x18711)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1874,plain,
% 60.70/60.75 (~E(f3(a1),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,43,1009,1820,222,132,1824,441,1871,350,311,4,420,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(1902,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,49,1044,1865,606,4,423,420])).
% 60.70/60.75 cnf(1906,plain,
% 60.70/60.75 (P4(a234,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,49,1044,225,135,1865,606,4,423,420,422,417])).
% 60.70/60.75 cnf(1910,plain,
% 60.70/60.75 (~E(f3(a87),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,49,1044,1859,225,135,1865,606,351,329,4,423,420,422,417,436,25])).
% 60.70/60.75 cnf(1912,plain,
% 60.70/60.75 (~P4(x19121,x19121)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1915,plain,
% 60.70/60.75 (~E(f3(a2),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,42,49,1044,1859,225,135,1865,606,441,1912,351,329,4,423,420,422,417,436,25,23,22,24])).
% 60.70/60.75 cnf(1942,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[48,1049,1902,4,420])).
% 60.70/60.75 cnf(1948,plain,
% 60.70/60.75 (P4(a236,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,48,1049,1902,227,137,1906,4,420,423,422,417])).
% 60.70/60.75 cnf(1952,plain,
% 60.70/60.75 (~E(f3(a109),f3(a87))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,48,1049,1902,227,137,1906,352,320,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(1954,plain,
% 60.70/60.75 (~P4(x19541,x19541)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1957,plain,
% 60.70/60.75 (~E(f3(a76),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,48,1049,1902,227,137,1906,441,1954,352,320,4,420,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(1983,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,47,1090,1942,1948,4,423,420])).
% 60.70/60.75 cnf(1987,plain,
% 60.70/60.75 (P4(a238,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,47,1090,1942,229,139,1948,4,423,420,422,417])).
% 60.70/60.75 cnf(1991,plain,
% 60.70/60.75 (~E(f3(a109),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,47,1090,1942,229,139,1948,357,4,423,420,422,417,436,25])).
% 60.70/60.75 cnf(1993,plain,
% 60.70/60.75 (~P4(x19931,x19931)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(1996,plain,
% 60.70/60.75 (~E(f3(a65),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,47,1090,1942,229,139,1948,441,1993,357,4,423,420,422,417,436,25,23,22,24])).
% 60.70/60.75 cnf(2022,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[46,1123,1983,4,420])).
% 60.70/60.75 cnf(2028,plain,
% 60.70/60.75 (P4(a240,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,46,1123,1983,230,140,1987,4,420,423,422,417])).
% 60.70/60.75 cnf(2032,plain,
% 60.70/60.75 (~E(f3(a109),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,46,1123,1983,230,140,1987,358,330,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(2034,plain,
% 60.70/60.75 (~P4(x20341,x20341)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2037,plain,
% 60.70/60.75 (~E(f3(a54),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,46,1123,1983,230,140,1987,441,2034,358,330,4,420,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(2053,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[45,1159,2022,4,420])).
% 60.70/60.75 cnf(2059,plain,
% 60.70/60.75 (P4(a243,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,45,1159,2022,233,143,2028,4,420,423,422,417])).
% 60.70/60.75 cnf(2063,plain,
% 60.70/60.75 (~E(f3(a109),f3(a54))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,45,1159,2022,233,143,2028,359,348,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(2065,plain,
% 60.70/60.75 (~P4(x20651,x20651)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2068,plain,
% 60.70/60.75 (~E(f3(a43),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,45,1159,2022,233,143,2028,441,2065,359,348,4,420,423,422,417,436,25,23,22,24])).
% 60.70/60.75 cnf(2092,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[44,1162,2053,4,420])).
% 60.70/60.75 cnf(2098,plain,
% 60.70/60.75 (P4(a244,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,44,1162,2053,234,144,2059,4,420,423,422,417])).
% 60.70/60.75 cnf(2102,plain,
% 60.70/60.75 (~E(f3(a109),f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,44,1162,2053,234,144,2059,360,357,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(2104,plain,
% 60.70/60.75 (~P4(x21041,x21041)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2107,plain,
% 60.70/60.75 (~E(f3(a4),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,44,1162,2053,234,144,2059,441,2104,360,357,4,420,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(2127,plain,
% 60.70/60.75 (~P8(f3(a98),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[43,1199,2092,4,420])).
% 60.70/60.75 cnf(2133,plain,
% 60.70/60.75 (P4(a247,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,43,1199,2092,237,147,2098,4,420,423,422,417])).
% 60.70/60.75 cnf(2137,plain,
% 60.70/60.75 (~E(f3(a109),f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,43,1199,2092,237,147,2098,361,330,4,420,423,422,417,436,25])).
% 60.70/60.75 cnf(2139,plain,
% 60.70/60.75 (~P4(x21391,x21391)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2141,plain,
% 60.70/60.75 (~P4(x21411,x21411)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2142,plain,
% 60.70/60.75 (~E(f3(a1),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,43,1199,2092,237,147,2098,441,2139,361,330,4,420,423,422,417,436,25,23,22,24])).
% 60.70/60.75 cnf(2143,plain,
% 60.70/60.75 (~P8(f250(f3(a98),f3(a98)),f250(f3(a98),f3(a98)))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,43,1199,2092,237,148,147,2098,441,2139,2141,361,330,4,420,423,422,417,436,25,23,22,24,419])).
% 60.70/60.75 cnf(2170,plain,
% 60.70/60.75 (P4(a248,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1204,238,148,2133,4,423,422,417])).
% 60.70/60.75 cnf(2174,plain,
% 60.70/60.75 (~E(f3(a109),f3(a1))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,1204,2127,238,148,2133,367,4,423,422,417,436,25])).
% 60.70/60.75 cnf(2176,plain,
% 60.70/60.75 (~P4(x21761,x21761)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2179,plain,
% 60.70/60.75 (~E(f3(a2),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,50,42,1204,2127,238,148,2133,441,2176,367,4,423,422,417,436,25,22,23,24])).
% 60.70/60.75 cnf(2208,plain,
% 60.70/60.75 (P4(a252,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1244,241,151,2170,4,423,422,417])).
% 60.70/60.75 cnf(2243,plain,
% 60.70/60.75 (P4(a253,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1588,242,152,2208,4,423,422,417])).
% 60.70/60.75 cnf(2279,plain,
% 60.70/60.75 (P4(a255,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1629,244,154,2243,4,423,422,417])).
% 60.70/60.75 cnf(2310,plain,
% 60.70/60.75 (P4(a257,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1670,246,156,2279,4,423,422,417])).
% 60.70/60.75 cnf(2345,plain,
% 60.70/60.75 (P4(a259,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1245,248,158,2310,4,423,422,417])).
% 60.70/60.75 cnf(2380,plain,
% 60.70/60.75 (P4(a145,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1286,287,259,2345,4,423,422,417])).
% 60.70/60.75 cnf(2417,plain,
% 60.70/60.75 (P4(a144,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1287,286,258,2380,4,423,422,417])).
% 60.70/60.75 cnf(2452,plain,
% 60.70/60.75 (P4(a143,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1327,285,257,2417,4,423,422,417])).
% 60.70/60.75 cnf(2487,plain,
% 60.70/60.75 (P4(a165,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1328,305,277,2452,4,423,422,417])).
% 60.70/60.75 cnf(2524,plain,
% 60.70/60.75 (P4(a153,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1366,294,266,2487,4,423,422,417])).
% 60.70/60.75 cnf(2552,plain,
% 60.70/60.75 (P4(a141,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1367,283,255,2524,4,423,422,417])).
% 60.70/60.75 cnf(2587,plain,
% 60.70/60.75 (P4(a163,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1408,303,275,2552,4,423,422,417])).
% 60.70/60.75 cnf(2615,plain,
% 60.70/60.75 (P4(a151,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1409,292,264,2587,4,423,422,417])).
% 60.70/60.75 cnf(2650,plain,
% 60.70/60.75 (P4(a139,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1746,281,253,2615,4,423,422,417])).
% 60.70/60.75 cnf(2685,plain,
% 60.70/60.75 (P4(a161,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1751,301,273,2650,4,423,422,417])).
% 60.70/60.75 cnf(2721,plain,
% 60.70/60.75 (P4(a149,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1786,290,262,2685,4,423,422,417])).
% 60.70/60.75 cnf(2749,plain,
% 60.70/60.75 (P4(a137,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1791,279,251,2721,4,423,422,417])).
% 60.70/60.75 cnf(2784,plain,
% 60.70/60.75 (P4(a136,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1828,278,250,2749,4,423,422,417])).
% 60.70/60.75 cnf(2789,plain,
% 60.70/60.75 (~P4(x27891,x27891)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2791,plain,
% 60.70/60.75 (~P4(x27911,x27911)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2793,plain,
% 60.70/60.75 (~P4(x27931,x27931)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2798,plain,
% 60.70/60.75 (P10(a136,a7,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1828,278,298,260,250,2749,441,2789,2791,2793,323,317,4,423,422,417,436,23,22,419,418,430])).
% 60.70/60.75 cnf(2819,plain,
% 60.70/60.75 (P4(a147,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,1833,288,260,2784,4,423,422,417])).
% 60.70/60.75 cnf(2824,plain,
% 60.70/60.75 (~P4(x28241,x28241)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2826,plain,
% 60.70/60.75 (~P4(x28261,x28261)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2827,plain,
% 60.70/60.75 (~P8(f250(f3(a98),f250(f3(a4),f3(a1))),f250(f3(a98),f250(f3(a4),f3(a1))))),
% 60.70/60.75 inference(scs_inference,[],[454,51,1833,288,306,260,2784,441,2824,2826,333,309,4,423,422,417,436,23,22,418])).
% 60.70/60.75 cnf(2851,plain,
% 60.70/60.75 (P4(a173,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,54,1869,63,2819,4,423,422,417])).
% 60.70/60.75 cnf(2871,plain,
% 60.70/60.75 (P10(a65,a195,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,56,65,1874,2851,4,423,422])).
% 60.70/60.75 cnf(2873,plain,
% 60.70/60.75 (P4(a195,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,56,65,1874,2851,4,423,422,417])).
% 60.70/60.75 cnf(2900,plain,
% 60.70/60.75 (P10(a87,a217,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,58,67,1910,2873,4,423,422])).
% 60.70/60.75 cnf(2902,plain,
% 60.70/60.75 (P4(a217,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,58,67,1910,2873,4,423,422,417])).
% 60.70/60.75 cnf(2907,plain,
% 60.70/60.75 (~P4(x29071,x29071)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(2908,plain,
% 60.70/60.75 (~E(a217,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,58,67,1910,2873,441,2907,343,337,4,423,422,417,436,23,22])).
% 60.70/60.75 cnf(2912,plain,
% 60.70/60.75 (~P4(a2,a217)),
% 60.70/60.75 inference(scs_inference,[],[454,51,58,67,1910,2873,441,2907,343,337,4,423,422,417,436,23,22,430,414])).
% 60.70/60.75 cnf(2931,plain,
% 60.70/60.75 (P4(a239,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,60,69,1915,2902,4,422,423,417])).
% 60.70/60.75 cnf(2956,plain,
% 60.70/60.75 (P3(a239,a121)),
% 60.70/60.75 inference(scs_inference,[],[454,1952,2931,4,423])).
% 60.70/60.75 cnf(2960,plain,
% 60.70/60.75 (P4(a135,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,71,161,1952,2931,4,423,422,417])).
% 60.70/60.75 cnf(2991,plain,
% 60.70/60.75 (P4(a157,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,73,163,1957,2960,4,423,422,417])).
% 60.70/60.75 cnf(3016,plain,
% 60.70/60.75 (P3(a157,a121)),
% 60.70/60.75 inference(scs_inference,[],[454,1991,2991,4,423])).
% 60.70/60.75 cnf(3020,plain,
% 60.70/60.75 (P4(a169,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,76,166,1991,2991,4,423,422,417])).
% 60.70/60.75 cnf(3049,plain,
% 60.70/60.75 (P4(a172,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,79,169,1996,3020,4,423,422,417])).
% 60.70/60.75 cnf(3071,plain,
% 60.70/60.75 (P4(a174,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,80,170,2032,3049,4,423,422,417])).
% 60.70/60.75 cnf(3100,plain,
% 60.70/60.75 (P4(a176,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,82,172,2037,3071,4,423,422,417])).
% 60.70/60.75 cnf(3129,plain,
% 60.70/60.75 (P4(a179,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,85,175,2063,3100,4,423,422,417])).
% 60.70/60.75 cnf(3152,plain,
% 60.70/60.75 (P4(a180,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,86,176,2068,3129,4,423,422,417])).
% 60.70/60.75 cnf(3173,plain,
% 60.70/60.75 (P4(a182,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,88,178,2102,3152,4,423,422,417])).
% 60.70/60.75 cnf(3202,plain,
% 60.70/60.75 (P4(a185,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,90,180,2107,3173,4,423,422,417])).
% 60.70/60.75 cnf(3231,plain,
% 60.70/60.75 (P4(a188,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,93,183,2137,3202,4,423,422,417])).
% 60.70/60.75 cnf(3260,plain,
% 60.70/60.75 (P4(a189,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,94,184,2142,3231,4,423,422,417])).
% 60.70/60.75 cnf(3289,plain,
% 60.70/60.75 (P4(a191,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,96,186,2174,3260,4,423,422,417])).
% 60.70/60.75 cnf(3314,plain,
% 60.70/60.75 (~E(a2,a98)),
% 60.70/60.75 inference(scs_inference,[],[2179,4])).
% 60.70/60.75 cnf(3319,plain,
% 60.70/60.75 (P4(a194,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,99,189,2179,3289,4,423,422,417])).
% 60.70/60.75 cnf(3347,plain,
% 60.70/60.75 (P4(a196,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,100,190,3319,423,422,417])).
% 60.70/60.75 cnf(3375,plain,
% 60.70/60.75 (P4(a198,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,102,192,3347,423,422,417])).
% 60.70/60.75 cnf(3396,plain,
% 60.70/60.75 (P4(a200,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,104,194,3375,423,422,417])).
% 60.70/60.75 cnf(3417,plain,
% 60.70/60.75 (P4(a202,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,106,196,3396,422,423,417])).
% 60.70/60.75 cnf(3419,plain,
% 60.70/60.75 (P6(f3(a65),f3(a1),f3(a4),f3(a98))),
% 60.70/60.75 inference(scs_inference,[],[454,51,106,196,3396,342,319,422,423,417,436])).
% 60.70/60.75 cnf(3447,plain,
% 60.70/60.75 (P4(a204,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,108,198,3417,423,422,417])).
% 60.70/60.75 cnf(3475,plain,
% 60.70/60.75 (P4(a207,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,110,200,3447,423,422,417])).
% 60.70/60.75 cnf(3496,plain,
% 60.70/60.75 (P4(a209,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,112,202,3475,423,422,417])).
% 60.70/60.75 cnf(3526,plain,
% 60.70/60.75 (P4(a211,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,114,204,3496,423,422,417])).
% 60.70/60.75 cnf(3528,plain,
% 60.70/60.75 (P6(f3(a1),f3(a54),f3(a2),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[454,51,114,204,3496,347,348,423,422,417,436])).
% 60.70/60.75 cnf(3555,plain,
% 60.70/60.75 (P4(a213,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,116,206,3526,423,422,417])).
% 60.70/60.75 cnf(3585,plain,
% 60.70/60.75 (P4(a215,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,118,208,3555,423,422,417])).
% 60.70/60.75 cnf(3613,plain,
% 60.70/60.75 (P4(a218,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,120,210,3585,423,422,417])).
% 60.70/60.75 cnf(3641,plain,
% 60.70/60.75 (P4(a220,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,122,212,3613,423,422,417])).
% 60.70/60.75 cnf(3669,plain,
% 60.70/60.75 (P4(a222,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,124,214,3641,423,422,417])).
% 60.70/60.75 cnf(3699,plain,
% 60.70/60.75 (P4(a224,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,126,216,3669,422,423,417])).
% 60.70/60.75 cnf(3727,plain,
% 60.70/60.75 (P4(a226,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,128,218,3699,422,423,417])).
% 60.70/60.75 cnf(3755,plain,
% 60.70/60.75 (P4(a229,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,130,220,3727,423,422,417])).
% 60.70/60.75 cnf(3783,plain,
% 60.70/60.75 (P4(a232,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,133,223,3755,422,423,417])).
% 60.70/60.75 cnf(3811,plain,
% 60.70/60.75 (P4(a233,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,134,224,3783,422,423,417])).
% 60.70/60.75 cnf(3816,plain,
% 60.70/60.75 (~P4(x38161,x38161)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(3828,plain,
% 60.70/60.75 (P9(x38281,f120(f250(f3(a54),f3(a87))))+~E(a103,x38281)),
% 60.70/60.75 inference(scs_inference,[],[454,2798,51,669,134,224,3419,3783,441,3816,399,369,331,422,423,417,436,23,22,430,414,11,10,26,21,14,28])).
% 60.70/60.75 cnf(3839,plain,
% 60.70/60.75 (P4(a235,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,136,226,3811,422,423,417])).
% 60.70/60.75 cnf(3870,plain,
% 60.70/60.75 (P4(a237,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,138,228,3839,422,423,417])).
% 60.70/60.75 cnf(3898,plain,
% 60.70/60.75 (P4(a241,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,141,231,3870,422,423,417])).
% 60.70/60.75 cnf(3926,plain,
% 60.70/60.75 (P4(a242,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,142,232,3898,422,423,417])).
% 60.70/60.75 cnf(3946,plain,
% 60.70/60.75 (P4(a245,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,145,235,3926,423,422,417])).
% 60.70/60.75 cnf(3951,plain,
% 60.70/60.75 (~P4(x39511,x39511)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(3964,plain,
% 60.70/60.75 (P9(x39641,f120(f250(f3(a65),f3(a98))))+~E(a115,x39641)),
% 60.70/60.75 inference(scs_inference,[],[454,51,806,1428,145,235,3528,2956,3926,441,3951,346,350,347,423,422,417,436,23,22,430,414,15,27,413,13,26,28])).
% 60.70/60.75 cnf(3975,plain,
% 60.70/60.75 (P4(a246,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,146,236,3946,423,422,417])).
% 60.70/60.75 cnf(4003,plain,
% 60.70/60.75 (P4(a249,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,149,239,3975,423,422,417])).
% 60.70/60.75 cnf(4008,plain,
% 60.70/60.75 (~P4(x40081,x40081)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(4019,plain,
% 60.70/60.75 (P9(x40191,f120(f250(f3(a109),f3(a98))))+~E(a119,x40191)),
% 60.70/60.75 inference(scs_inference,[],[454,51,149,239,3016,3975,441,4008,354,361,348,423,422,417,436,23,22,430,414,10,12,413,28])).
% 60.70/60.75 cnf(4031,plain,
% 60.70/60.75 (P4(a251,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,150,240,4003,423,422,417])).
% 60.70/60.75 cnf(4051,plain,
% 60.70/60.75 (P4(a254,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,153,243,4031,423,422,417])).
% 60.70/60.75 cnf(4072,plain,
% 60.70/60.75 (P4(a256,a2)),
% 60.70/60.75 inference(scs_inference,[],[454,51,155,245,4051,423,422,417])).
% 60.70/60.75 cnf(4097,plain,
% 60.70/60.75 (~P4(x40971,x40971)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(4104,plain,
% 60.70/60.75 (P9(x41041,f120(f250(f3(a87),f3(a109))))+~E(a129,x41041)),
% 60.70/60.75 inference(scs_inference,[],[454,51,157,247,4072,441,4097,343,319,436,422,423,417,23,22,430,414,28])).
% 60.70/60.75 cnf(4202,plain,
% 60.70/60.75 (P6(f3(a54),f3(a4),f3(a2),f3(a76))),
% 60.70/60.75 inference(scs_inference,[],[331,327,436])).
% 60.70/60.75 cnf(4405,plain,
% 60.70/60.75 (P4(a138,a2)),
% 60.70/60.75 inference(scs_inference,[],[51,252,280,329,309,436,422,417])).
% 60.70/60.75 cnf(4430,plain,
% 60.70/60.75 (~P4(x44301,x44301)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(4437,plain,
% 60.70/60.75 (P9(x44371,f120(f250(f3(a4),f250(f3(a4),f3(a1)))))+~E(a31,x44371)),
% 60.70/60.75 inference(scs_inference,[],[454,51,272,300,4405,441,4430,351,320,436,422,417,423,23,22,430,414,28])).
% 60.70/60.75 cnf(4531,plain,
% 60.70/60.75 (P4(a166,a2)),
% 60.70/60.75 inference(scs_inference,[],[51,306,347,352,436,417])).
% 60.70/60.75 cnf(4555,plain,
% 60.70/60.75 (P4(a133,a2)),
% 60.70/60.75 inference(scs_inference,[],[51,62,329,327,436,417])).
% 60.70/60.75 cnf(4560,plain,
% 60.70/60.75 (~P4(x45601,x45601)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(4570,plain,
% 60.70/60.75 (P9(x45701,f120(f250(f3(a76),f3(a43))))+~E(a61,x45701)),
% 60.70/60.75 inference(scs_inference,[],[454,51,96,62,1818,4202,4531,441,4560,355,329,327,436,417,423,23,22,414,27,16,14,15,11,28])).
% 60.70/60.75 cnf(4579,plain,
% 60.70/60.75 (P4(a184,a4)),
% 60.70/60.75 inference(scs_inference,[],[64,53,328,318,436,417])).
% 60.70/60.75 cnf(4581,plain,
% 60.70/60.75 (P3(a133,a121)),
% 60.70/60.75 inference(scs_inference,[],[454,64,53,4555,328,318,436,417,423])).
% 60.70/60.75 cnf(4606,plain,
% 60.70/60.75 (P4(a228,a54)),
% 60.70/60.75 inference(scs_inference,[],[1099,68,55,4581,331,309,413,436,417])).
% 60.70/60.75 cnf(4609,plain,
% 60.70/60.75 (~P4(x46091,x46091)),
% 60.70/60.75 inference(rename_variables,[],[441])).
% 60.70/60.75 cnf(4612,plain,
% 60.70/60.75 (~P4(a121,a133)),
% 60.70/60.75 inference(scs_inference,[],[1099,68,55,4581,441,4609,331,309,413,436,417,23,22,414])).
% 60.70/60.75 cnf(4630,plain,
% 60.70/60.75 (P4(a134,a98)),
% 60.70/60.75 inference(scs_inference,[],[160,59,4606,310,339,414,436,417])).
% 60.70/60.75 cnf(4652,plain,
% 60.70/60.75 (P4(a146,a5)),
% 60.70/60.75 inference(scs_inference,[],[162,70,4630,319,317,414,436,417])).
% 60.70/60.75 cnf(4662,plain,
% 60.70/60.75 (~P4(a5,a146)),
% 60.70/60.75 inference(scs_inference,[],[4652,414])).
% 60.70/60.75 cnf(4666,plain,
% 60.70/60.75 (P4(a168,a17)),
% 60.70/60.75 inference(scs_inference,[],[165,72,4652,341,337,414,436,417])).
% 60.70/60.75 cnf(4668,plain,
% 60.70/60.75 (~E(a5,a146)),
% 60.70/60.75 inference(scs_inference,[],[165,72,4652,441,341,337,414,436,417,23])).
% 60.70/60.75 cnf(4692,plain,
% 60.70/60.75 (P7(f3(a4))),
% 60.70/60.75 inference(scs_inference,[],[487,444,34,1032,50,412,415,426,421,410])).
% 60.70/60.75 cnf(4703,plain,
% 60.70/60.75 (~P10(a4,a121,a2)),
% 60.70/60.75 inference(scs_inference,[],[487,550,1074,450,444,4666,34,1032,50,412,415,426,421,410,416,409,414,2,428,429])).
% 60.70/60.75 cnf(4709,plain,
% 60.70/60.75 (P8(f3(a87),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[487,550,1074,3314,450,444,4666,34,2827,2143,1032,50,49,412,415,426,421,410,416,409,414,2,428,429,25,24,427,420])).
% 60.70/60.75 cnf(4717,plain,
% 60.70/60.75 (~P3(a4,a133)),
% 60.70/60.75 inference(scs_inference,[],[487,550,1074,3314,450,491,444,4666,34,2827,504,2143,1032,52,50,49,51,412,415,426,421,410,416,409,414,2,428,429,25,24,427,420,424,422,29,413])).
% 60.70/60.75 cnf(4721,plain,
% 60.70/60.75 (~P9(a171,f120(x47211))),
% 60.70/60.75 inference(scs_inference,[],[487,550,1074,3314,450,491,444,4666,34,2827,504,2143,1032,316,397,52,168,50,49,441,51,412,415,426,421,410,416,409,414,2,428,429,25,24,427,420,424,422,29,413,436,417])).
% 60.70/60.75 cnf(4741,plain,
% 60.70/60.75 (~P9(a171,f120(x47411))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4743,plain,
% 60.70/60.75 (~P9(a171,f120(x47431))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4745,plain,
% 60.70/60.75 (~P9(a171,f120(x47451))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4747,plain,
% 60.70/60.75 (~P9(a171,f120(x47471))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4749,plain,
% 60.70/60.75 (~P9(a171,f120(x47491))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4751,plain,
% 60.70/60.75 (~P9(a171,f120(x47511))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4753,plain,
% 60.70/60.75 (~P9(a171,f120(x47531))),
% 60.70/60.75 inference(rename_variables,[],[4721])).
% 60.70/60.75 cnf(4762,plain,
% 60.70/60.75 (P7(f3(a43))),
% 60.70/60.75 inference(scs_inference,[],[2871,4579,4692,4709,4721,4741,4743,4745,4747,4749,4751,35,1026,3828,3964,4019,4104,4570,4437,415,421,412,426,410])).
% 60.70/60.75 cnf(4773,plain,
% 60.70/60.75 (P8(f3(a76),f3(a109))),
% 60.70/60.75 inference(scs_inference,[],[519,629,2871,482,4579,4692,4709,4721,4741,4743,4745,4747,4749,4751,35,496,48,1026,3828,3964,4019,4104,4570,4437,415,421,412,426,410,416,2,428,429,427,420])).
% 60.70/60.75 cnf(4783,plain,
% 60.70/60.75 (~P9(a133,f120(x47831))),
% 60.70/60.75 inference(scs_inference,[],[519,629,2871,482,4579,4662,4668,4703,4692,4709,4721,4741,4743,4745,4747,4749,4751,4753,35,4612,496,99,61,53,48,1026,3828,3964,4019,4104,4570,4437,415,421,412,426,410,416,2,428,429,427,420,424,422,28,413,417])).
% 60.70/60.75 cnf(4795,plain,
% 60.70/60.75 (~P6(f3(a2),f3(a4),f3(a43),f3(a65))),
% 60.70/60.75 inference(scs_inference,[],[407,519,629,2871,482,4579,4662,4668,4703,4717,4692,4709,4721,4741,4743,4745,4747,4749,4751,4753,35,4612,2912,496,398,99,325,58,54,61,67,56,53,308,48,441,1026,3828,3964,4019,4104,4570,4437,415,421,412,426,410,416,2,428,429,427,420,424,422,28,413,417,437,418,419,791,423,431])).
% 60.70/60.75 cnf(4800,plain,
% 60.70/60.75 (~P9(a133,f120(x48001))),
% 60.70/60.75 inference(rename_variables,[],[4783])).
% 60.70/60.75 cnf(4804,plain,
% 60.70/60.75 (~P9(a133,f120(x48041))),
% 60.70/60.75 inference(rename_variables,[],[4783])).
% 60.70/60.75 cnf(4806,plain,
% 60.70/60.75 (~P9(a133,f120(x48061))),
% 60.70/60.75 inference(rename_variables,[],[4783])).
% 60.70/60.75 cnf(4808,plain,
% 60.70/60.75 (~P9(a133,f120(x48081))),
% 60.70/60.75 inference(rename_variables,[],[4783])).
% 60.70/60.75 cnf(4812,plain,
% 60.70/60.75 (~P9(a133,f120(x48121))),
% 60.70/60.75 inference(rename_variables,[],[4783])).
% 60.70/60.75 cnf(4820,plain,
% 60.70/60.75 (~P9(a133,f120(x48201))),
% 60.70/60.75 inference(rename_variables,[],[4783])).
% 60.70/60.75 cnf(4841,plain,
% 60.70/60.75 ($false),
% 60.70/60.75 inference(scs_inference,[],[702,881,528,2908,2900,594,4762,4773,4783,4800,4804,4806,4808,4812,4820,4795,36,542,448,58,357,330,46,47,3828,421,4104,4019,4570,412,4437,415,426,410,1026,3964,416,2,429,428,427,420,424,20,422,413,436]),
% 60.70/60.75 ['proof']).
% 60.70/60.75 % SZS output end Proof
% 60.70/60.75 % Total time :60.010000s
%------------------------------------------------------------------------------