%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM310+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n022.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:48 EDT 2024
% Result : Theorem 61.15s 61.23s
% Output : CNFRefutation 61.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM310+1 : TPTP v8.2.0. Released v3.1.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sat Jun 22 22:22:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.53/0.56 start to proof:theBenchmark
% 61.15/61.22 %-------------------------------------------
% 61.15/61.22 % File :CSE---1.7
% 61.15/61.22 % Problem :theBenchmark
% 61.15/61.22 % Transform :cnf
% 61.15/61.22 % Format :tptp:raw
% 61.15/61.22 % Command :java -jar mcs_scs.jar %d %s
% 61.15/61.22
% 61.15/61.22 % Result :Theorem 60.550000s
% 61.15/61.22 % Output :CNFRefutation 60.550000s
% 61.15/61.22 %-------------------------------------------
% 61.15/61.22 %------------------------------------------------------------------------------
% 61.15/61.22 % File : NUM310+1 : TPTP v8.2.0. Released v3.1.0.
% 61.15/61.22 % Domain : Number Theory (RDN arithmetic)
% 61.15/61.22 % Problem : 2 + 3 != 6
% 61.15/61.22 % Version : Especial.
% 61.15/61.22 % English :
% 61.15/61.22
% 61.15/61.22 % Refs :
% 61.15/61.22 % Source : [TPTP]
% 61.15/61.22 % Names :
% 61.15/61.22
% 61.15/61.22 % Status : Theorem
% 61.15/61.22 % Rating : 0.61 v8.2.0, 0.58 v8.1.0, 0.61 v7.5.0, 0.62 v7.4.0, 0.60 v7.3.0, 0.66 v7.2.0, 0.59 v7.1.0, 0.48 v7.0.0, 0.50 v6.4.0, 0.62 v6.3.0, 0.58 v6.2.0, 0.56 v6.1.0, 0.70 v6.0.0, 0.57 v5.5.0, 0.63 v5.4.0, 0.64 v5.3.0, 0.70 v5.2.0, 0.65 v5.1.0, 0.62 v4.1.0, 0.65 v4.0.0, 0.62 v3.7.0, 0.65 v3.5.0, 0.74 v3.4.0, 0.79 v3.2.0, 0.82 v3.1.0
% 61.15/61.22 % Syntax : Number of formulae : 402 ( 375 unt; 0 def)
% 61.15/61.22 % Number of atoms : 473 ( 5 equ)
% 61.15/61.22 % Maximal formula atoms : 8 ( 1 avg)
% 61.15/61.22 % Number of connectives : 74 ( 3 ~; 1 |; 43 &)
% 61.15/61.22 % ( 3 <=>; 24 =>; 0 <=; 0 <~>)
% 61.15/61.22 % Maximal formula depth : 19 ( 1 avg)
% 61.15/61.22 % Maximal term depth : 5 ( 2 avg)
% 61.15/61.22 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 61.15/61.22 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 61.15/61.22 % Number of variables : 121 ( 121 !; 0 ?)
% 61.15/61.22 % SPC : FOF_THM_RFO_SEQ
% 61.15/61.22
% 61.15/61.22 % Comments :
% 61.15/61.23 %------------------------------------------------------------------------------
% 61.15/61.23 %----Include axioms for RDN arithmetic
% 61.15/61.23 include('Axioms/NUM005+0.ax').
% 61.15/61.23 include('Axioms/NUM005+1.ax').
% 61.15/61.23 include('Axioms/NUM005+2.ax').
% 61.15/61.23 %------------------------------------------------------------------------------
% 61.15/61.23 fof(sum_n2_n3_not_n6,conjecture,
% 61.15/61.23 ~ sum(n2,n3,n6) ).
% 61.15/61.23
% 61.15/61.23 %------------------------------------------------------------------------------
% 61.15/61.23 %-------------------------------------------
% 61.15/61.23 % Proof found
% 61.15/61.23 % SZS status Theorem for theBenchmark
% 61.15/61.23 % SZS output start Proof
% 61.15/61.23 %ClaNum:439(EqnAxiom:32)
% 61.15/61.23 %VarNum:271(SingletonVarNum:132)
% 61.15/61.23 %MaxLitNum:8
% 61.15/61.23 %MaxfuncDepth:4
% 61.15/61.23 %SharedTerms:967
% 61.15/61.23 %goalClause: 70
% 61.15/61.23 %singleGoalClaCount:1
% 61.15/61.23 [70]P10(a4,a43,a76)
% 61.15/61.23 [33]P1(f3(a1))
% 61.15/61.23 [34]P1(f3(a4))
% 61.15/61.23 [35]P1(f3(a43))
% 61.15/61.23 [36]P1(f3(a54))
% 61.15/61.23 [37]P1(f3(a65))
% 61.15/61.23 [38]P1(f3(a76))
% 61.15/61.23 [39]P1(f3(a87))
% 61.15/61.23 [40]P1(f3(a98))
% 61.15/61.23 [41]P1(f3(a109))
% 61.15/61.23 [42]P8(f3(a2),f3(a1))
% 61.15/61.23 [43]P8(f3(a1),f3(a4))
% 61.15/61.23 [44]P8(f3(a4),f3(a43))
% 61.15/61.23 [45]P8(f3(a43),f3(a54))
% 61.15/61.23 [46]P8(f3(a54),f3(a65))
% 61.15/61.23 [47]P8(f3(a65),f3(a76))
% 61.15/61.23 [48]P8(f3(a76),f3(a87))
% 61.22/61.23 [49]P8(f3(a87),f3(a98))
% 61.22/61.23 [50]P8(f3(a98),f3(a109))
% 61.22/61.23 [308]P2(f3(a2),f3(a2),f3(a2),f3(a2))
% 61.22/61.23 [309]P2(f3(a2),f3(a1),f3(a1),f3(a2))
% 61.22/61.23 [310]P2(f3(a2),f3(a4),f3(a4),f3(a2))
% 61.22/61.23 [311]P2(f3(a2),f3(a43),f3(a43),f3(a2))
% 61.22/61.23 [312]P2(f3(a2),f3(a54),f3(a54),f3(a2))
% 61.22/61.23 [313]P2(f3(a2),f3(a65),f3(a65),f3(a2))
% 61.22/61.23 [314]P2(f3(a2),f3(a76),f3(a76),f3(a2))
% 61.22/61.23 [315]P2(f3(a2),f3(a87),f3(a87),f3(a2))
% 61.22/61.23 [316]P2(f3(a2),f3(a98),f3(a98),f3(a2))
% 61.22/61.23 [317]P2(f3(a2),f3(a109),f3(a109),f3(a2))
% 61.22/61.23 [318]P2(f3(a1),f3(a2),f3(a1),f3(a2))
% 61.22/61.23 [319]P2(f3(a1),f3(a1),f3(a4),f3(a2))
% 61.22/61.23 [320]P2(f3(a1),f3(a4),f3(a43),f3(a2))
% 61.22/61.23 [321]P2(f3(a1),f3(a43),f3(a54),f3(a2))
% 61.22/61.23 [322]P2(f3(a1),f3(a54),f3(a65),f3(a2))
% 61.22/61.23 [323]P2(f3(a1),f3(a65),f3(a76),f3(a2))
% 61.22/61.23 [324]P2(f3(a1),f3(a76),f3(a87),f3(a2))
% 61.22/61.23 [325]P2(f3(a1),f3(a87),f3(a98),f3(a2))
% 61.22/61.23 [326]P2(f3(a1),f3(a98),f3(a109),f3(a2))
% 61.22/61.23 [327]P2(f3(a1),f3(a109),f3(a2),f3(a1))
% 61.22/61.23 [328]P2(f3(a4),f3(a2),f3(a4),f3(a2))
% 61.22/61.23 [329]P2(f3(a4),f3(a1),f3(a43),f3(a2))
% 61.22/61.23 [330]P2(f3(a4),f3(a4),f3(a54),f3(a2))
% 61.22/61.23 [331]P2(f3(a4),f3(a43),f3(a65),f3(a2))
% 61.22/61.23 [332]P2(f3(a4),f3(a54),f3(a76),f3(a2))
% 61.22/61.23 [333]P2(f3(a4),f3(a65),f3(a87),f3(a2))
% 61.22/61.23 [334]P2(f3(a4),f3(a76),f3(a98),f3(a2))
% 61.22/61.23 [335]P2(f3(a4),f3(a87),f3(a109),f3(a2))
% 61.22/61.23 [336]P2(f3(a4),f3(a98),f3(a2),f3(a1))
% 61.22/61.23 [337]P2(f3(a4),f3(a109),f3(a1),f3(a1))
% 61.22/61.23 [338]P2(f3(a43),f3(a2),f3(a43),f3(a2))
% 61.22/61.23 [339]P2(f3(a43),f3(a1),f3(a54),f3(a2))
% 61.22/61.23 [340]P2(f3(a43),f3(a4),f3(a65),f3(a2))
% 61.22/61.23 [341]P2(f3(a43),f3(a43),f3(a76),f3(a2))
% 61.22/61.23 [342]P2(f3(a43),f3(a54),f3(a87),f3(a2))
% 61.22/61.23 [343]P2(f3(a43),f3(a65),f3(a98),f3(a2))
% 61.22/61.23 [344]P2(f3(a43),f3(a76),f3(a109),f3(a2))
% 61.22/61.23 [345]P2(f3(a43),f3(a87),f3(a2),f3(a1))
% 61.22/61.23 [346]P2(f3(a43),f3(a98),f3(a1),f3(a1))
% 61.22/61.23 [347]P2(f3(a43),f3(a109),f3(a4),f3(a1))
% 61.22/61.23 [348]P2(f3(a54),f3(a2),f3(a54),f3(a2))
% 61.22/61.23 [349]P2(f3(a54),f3(a1),f3(a65),f3(a2))
% 61.22/61.23 [350]P2(f3(a54),f3(a4),f3(a76),f3(a2))
% 61.22/61.23 [351]P2(f3(a54),f3(a43),f3(a87),f3(a2))
% 61.22/61.23 [352]P2(f3(a54),f3(a54),f3(a98),f3(a2))
% 61.22/61.23 [353]P2(f3(a54),f3(a65),f3(a109),f3(a2))
% 61.22/61.23 [354]P2(f3(a54),f3(a76),f3(a2),f3(a1))
% 61.22/61.23 [355]P2(f3(a54),f3(a87),f3(a1),f3(a1))
% 61.22/61.23 [356]P2(f3(a54),f3(a98),f3(a4),f3(a1))
% 61.22/61.23 [357]P2(f3(a54),f3(a109),f3(a43),f3(a1))
% 61.22/61.23 [358]P2(f3(a65),f3(a2),f3(a65),f3(a2))
% 61.22/61.23 [359]P2(f3(a65),f3(a1),f3(a76),f3(a2))
% 61.22/61.23 [360]P2(f3(a65),f3(a4),f3(a87),f3(a2))
% 61.22/61.23 [361]P2(f3(a65),f3(a43),f3(a98),f3(a2))
% 61.22/61.23 [362]P2(f3(a65),f3(a54),f3(a109),f3(a2))
% 61.22/61.23 [363]P2(f3(a65),f3(a65),f3(a2),f3(a1))
% 61.22/61.23 [364]P2(f3(a65),f3(a76),f3(a1),f3(a1))
% 61.22/61.23 [365]P2(f3(a65),f3(a87),f3(a4),f3(a1))
% 61.22/61.23 [366]P2(f3(a65),f3(a98),f3(a43),f3(a1))
% 61.22/61.23 [367]P2(f3(a65),f3(a109),f3(a54),f3(a1))
% 61.22/61.23 [368]P2(f3(a76),f3(a2),f3(a76),f3(a2))
% 61.22/61.23 [369]P2(f3(a76),f3(a1),f3(a87),f3(a2))
% 61.22/61.23 [370]P2(f3(a76),f3(a4),f3(a98),f3(a2))
% 61.22/61.23 [371]P2(f3(a76),f3(a43),f3(a109),f3(a2))
% 61.22/61.23 [372]P2(f3(a76),f3(a54),f3(a2),f3(a1))
% 61.22/61.23 [373]P2(f3(a76),f3(a65),f3(a1),f3(a1))
% 61.22/61.23 [374]P2(f3(a76),f3(a76),f3(a4),f3(a1))
% 61.22/61.23 [375]P2(f3(a76),f3(a87),f3(a43),f3(a1))
% 61.22/61.23 [376]P2(f3(a76),f3(a98),f3(a54),f3(a1))
% 61.22/61.23 [377]P2(f3(a76),f3(a109),f3(a65),f3(a1))
% 61.22/61.23 [378]P2(f3(a87),f3(a2),f3(a87),f3(a2))
% 61.22/61.23 [379]P2(f3(a87),f3(a1),f3(a98),f3(a2))
% 61.22/61.23 [380]P2(f3(a87),f3(a4),f3(a109),f3(a2))
% 61.22/61.23 [381]P2(f3(a87),f3(a43),f3(a2),f3(a1))
% 61.22/61.23 [382]P2(f3(a87),f3(a54),f3(a1),f3(a1))
% 61.22/61.23 [383]P2(f3(a87),f3(a65),f3(a4),f3(a1))
% 61.22/61.23 [384]P2(f3(a87),f3(a76),f3(a43),f3(a1))
% 61.22/61.23 [385]P2(f3(a87),f3(a87),f3(a54),f3(a1))
% 61.22/61.23 [386]P2(f3(a87),f3(a98),f3(a65),f3(a1))
% 61.22/61.23 [387]P2(f3(a87),f3(a109),f3(a76),f3(a1))
% 61.22/61.23 [388]P2(f3(a98),f3(a2),f3(a98),f3(a2))
% 61.22/61.23 [389]P2(f3(a98),f3(a1),f3(a109),f3(a2))
% 61.22/61.23 [390]P2(f3(a98),f3(a4),f3(a2),f3(a1))
% 61.22/61.23 [391]P2(f3(a98),f3(a43),f3(a1),f3(a1))
% 61.22/61.23 [392]P2(f3(a98),f3(a54),f3(a4),f3(a1))
% 61.22/61.23 [393]P2(f3(a98),f3(a65),f3(a43),f3(a1))
% 61.22/61.23 [394]P2(f3(a98),f3(a76),f3(a54),f3(a1))
% 61.22/61.23 [395]P2(f3(a98),f3(a87),f3(a65),f3(a1))
% 61.22/61.23 [396]P2(f3(a98),f3(a98),f3(a76),f3(a1))
% 61.22/61.23 [397]P2(f3(a98),f3(a109),f3(a87),f3(a1))
% 61.22/61.23 [398]P2(f3(a109),f3(a2),f3(a109),f3(a2))
% 61.22/61.23 [399]P2(f3(a109),f3(a1),f3(a2),f3(a1))
% 61.22/61.23 [400]P2(f3(a109),f3(a4),f3(a1),f3(a1))
% 61.22/61.23 [401]P2(f3(a109),f3(a43),f3(a4),f3(a1))
% 61.22/61.23 [402]P2(f3(a109),f3(a54),f3(a43),f3(a1))
% 61.22/61.23 [403]P2(f3(a109),f3(a65),f3(a54),f3(a1))
% 61.22/61.23 [404]P2(f3(a109),f3(a76),f3(a65),f3(a1))
% 61.22/61.23 [405]P2(f3(a109),f3(a87),f3(a76),f3(a1))
% 61.22/61.23 [406]P2(f3(a109),f3(a98),f3(a87),f3(a1))
% 61.22/61.23 [407]P2(f3(a109),f3(a109),f3(a98),f3(a1))
% 61.22/61.23 [51]P9(a2,f120(f3(a2)))
% 61.22/61.23 [52]P9(a1,f120(f3(a1)))
% 61.22/61.23 [53]P9(a4,f120(f3(a4)))
% 61.22/61.23 [54]P9(a43,f120(f3(a43)))
% 61.22/61.23 [55]P9(a54,f120(f3(a54)))
% 61.22/61.23 [56]P9(a65,f120(f3(a65)))
% 61.22/61.23 [57]P9(a76,f120(f3(a76)))
% 61.22/61.23 [58]P9(a87,f120(f3(a87)))
% 61.22/61.23 [59]P9(a98,f120(f3(a98)))
% 61.22/61.23 [60]P9(a109,f120(f3(a109)))
% 61.22/61.23 [61]P9(a121,f132(f3(a1)))
% 61.22/61.23 [62]P9(a133,f132(f3(a4)))
% 61.22/61.23 [63]P9(a173,f132(f3(a43)))
% 61.22/61.23 [64]P9(a184,f132(f3(a54)))
% 61.22/61.23 [65]P9(a195,f132(f3(a65)))
% 61.22/61.23 [66]P9(a206,f132(f3(a76)))
% 61.22/61.23 [67]P9(a217,f132(f3(a87)))
% 61.22/61.23 [68]P9(a228,f132(f3(a98)))
% 61.22/61.23 [69]P9(a239,f132(f3(a109)))
% 61.22/61.23 [71]P9(a5,f120(f250(f3(a2),f3(a1))))
% 61.22/61.23 [72]P9(a6,f120(f250(f3(a1),f3(a1))))
% 61.22/61.23 [73]P9(a17,f120(f250(f3(a4),f3(a1))))
% 61.22/61.23 [74]P9(a28,f120(f250(f3(a43),f3(a1))))
% 61.22/61.23 [75]P9(a37,f120(f250(f3(a54),f3(a1))))
% 61.22/61.23 [76]P9(a38,f120(f250(f3(a65),f3(a1))))
% 61.22/61.23 [77]P9(a39,f120(f250(f3(a76),f3(a1))))
% 61.22/61.23 [78]P9(a40,f120(f250(f3(a87),f3(a1))))
% 61.22/61.23 [79]P9(a41,f120(f250(f3(a98),f3(a1))))
% 61.22/61.23 [80]P9(a42,f120(f250(f3(a109),f3(a1))))
% 61.22/61.23 [81]P9(a44,f120(f250(f3(a2),f3(a4))))
% 61.22/61.23 [82]P9(a45,f120(f250(f3(a1),f3(a4))))
% 61.22/61.24 [83]P9(a46,f120(f250(f3(a4),f3(a4))))
% 61.22/61.24 [84]P9(a47,f120(f250(f3(a43),f3(a4))))
% 61.22/61.24 [85]P9(a48,f120(f250(f3(a54),f3(a4))))
% 61.22/61.24 [86]P9(a49,f120(f250(f3(a65),f3(a4))))
% 61.22/61.24 [87]P9(a50,f120(f250(f3(a76),f3(a4))))
% 61.22/61.24 [88]P9(a51,f120(f250(f3(a87),f3(a4))))
% 61.22/61.24 [89]P9(a52,f120(f250(f3(a98),f3(a4))))
% 61.22/61.24 [90]P9(a53,f120(f250(f3(a109),f3(a4))))
% 61.22/61.24 [91]P9(a55,f120(f250(f3(a2),f3(a43))))
% 61.22/61.24 [92]P9(a56,f120(f250(f3(a1),f3(a43))))
% 61.22/61.24 [93]P9(a57,f120(f250(f3(a4),f3(a43))))
% 61.22/61.24 [94]P9(a58,f120(f250(f3(a43),f3(a43))))
% 61.22/61.24 [95]P9(a59,f120(f250(f3(a54),f3(a43))))
% 61.22/61.24 [96]P9(a60,f120(f250(f3(a65),f3(a43))))
% 61.22/61.24 [97]P9(a61,f120(f250(f3(a76),f3(a43))))
% 61.22/61.24 [98]P9(a62,f120(f250(f3(a87),f3(a43))))
% 61.22/61.24 [99]P9(a63,f120(f250(f3(a98),f3(a43))))
% 61.22/61.24 [100]P9(a64,f120(f250(f3(a109),f3(a43))))
% 61.22/61.24 [101]P9(a66,f120(f250(f3(a2),f3(a54))))
% 61.22/61.24 [102]P9(a67,f120(f250(f3(a1),f3(a54))))
% 61.22/61.24 [103]P9(a68,f120(f250(f3(a4),f3(a54))))
% 61.22/61.24 [104]P9(a69,f120(f250(f3(a43),f3(a54))))
% 61.22/61.24 [105]P9(a70,f120(f250(f3(a54),f3(a54))))
% 61.22/61.24 [106]P9(a71,f120(f250(f3(a65),f3(a54))))
% 61.22/61.24 [107]P9(a72,f120(f250(f3(a76),f3(a54))))
% 61.22/61.24 [108]P9(a73,f120(f250(f3(a87),f3(a54))))
% 61.22/61.24 [109]P9(a74,f120(f250(f3(a98),f3(a54))))
% 61.22/61.24 [110]P9(a75,f120(f250(f3(a109),f3(a54))))
% 61.22/61.24 [111]P9(a77,f120(f250(f3(a2),f3(a65))))
% 61.22/61.24 [112]P9(a78,f120(f250(f3(a1),f3(a65))))
% 61.22/61.24 [113]P9(a79,f120(f250(f3(a4),f3(a65))))
% 61.22/61.24 [114]P9(a80,f120(f250(f3(a43),f3(a65))))
% 61.22/61.24 [115]P9(a81,f120(f250(f3(a54),f3(a65))))
% 61.22/61.24 [116]P9(a82,f120(f250(f3(a65),f3(a65))))
% 61.22/61.24 [117]P9(a83,f120(f250(f3(a76),f3(a65))))
% 61.22/61.24 [118]P9(a84,f120(f250(f3(a87),f3(a65))))
% 61.22/61.24 [119]P9(a85,f120(f250(f3(a98),f3(a65))))
% 61.22/61.24 [120]P9(a86,f120(f250(f3(a109),f3(a65))))
% 61.22/61.24 [121]P9(a88,f120(f250(f3(a2),f3(a76))))
% 61.22/61.24 [122]P9(a89,f120(f250(f3(a1),f3(a76))))
% 61.22/61.24 [123]P9(a90,f120(f250(f3(a4),f3(a76))))
% 61.22/61.24 [124]P9(a91,f120(f250(f3(a43),f3(a76))))
% 61.22/61.24 [125]P9(a92,f120(f250(f3(a54),f3(a76))))
% 61.22/61.24 [126]P9(a93,f120(f250(f3(a65),f3(a76))))
% 61.22/61.24 [127]P9(a94,f120(f250(f3(a76),f3(a76))))
% 61.22/61.24 [128]P9(a95,f120(f250(f3(a87),f3(a76))))
% 61.22/61.24 [129]P9(a96,f120(f250(f3(a98),f3(a76))))
% 61.22/61.24 [130]P9(a97,f120(f250(f3(a109),f3(a76))))
% 61.22/61.24 [131]P9(a99,f120(f250(f3(a2),f3(a87))))
% 61.22/61.24 [132]P9(a100,f120(f250(f3(a1),f3(a87))))
% 61.22/61.24 [133]P9(a101,f120(f250(f3(a4),f3(a87))))
% 61.22/61.24 [134]P9(a102,f120(f250(f3(a43),f3(a87))))
% 61.22/61.24 [135]P9(a103,f120(f250(f3(a54),f3(a87))))
% 61.22/61.24 [136]P9(a104,f120(f250(f3(a65),f3(a87))))
% 61.22/61.24 [137]P9(a105,f120(f250(f3(a76),f3(a87))))
% 61.22/61.24 [138]P9(a106,f120(f250(f3(a87),f3(a87))))
% 61.22/61.24 [139]P9(a107,f120(f250(f3(a98),f3(a87))))
% 61.22/61.24 [140]P9(a108,f120(f250(f3(a109),f3(a87))))
% 61.22/61.24 [141]P9(a110,f120(f250(f3(a2),f3(a98))))
% 61.22/61.24 [142]P9(a111,f120(f250(f3(a1),f3(a98))))
% 61.22/61.24 [143]P9(a112,f120(f250(f3(a4),f3(a98))))
% 61.22/61.24 [144]P9(a113,f120(f250(f3(a43),f3(a98))))
% 61.22/61.24 [145]P9(a114,f120(f250(f3(a54),f3(a98))))
% 61.22/61.24 [146]P9(a115,f120(f250(f3(a65),f3(a98))))
% 61.22/61.24 [147]P9(a116,f120(f250(f3(a76),f3(a98))))
% 61.22/61.24 [148]P9(a117,f120(f250(f3(a87),f3(a98))))
% 61.22/61.24 [149]P9(a118,f120(f250(f3(a98),f3(a98))))
% 61.22/61.24 [150]P9(a119,f120(f250(f3(a109),f3(a98))))
% 61.22/61.24 [151]P9(a122,f120(f250(f3(a2),f3(a109))))
% 61.22/61.24 [152]P9(a123,f120(f250(f3(a1),f3(a109))))
% 61.22/61.24 [153]P9(a124,f120(f250(f3(a4),f3(a109))))
% 61.22/61.24 [154]P9(a125,f120(f250(f3(a43),f3(a109))))
% 61.22/61.24 [155]P9(a126,f120(f250(f3(a54),f3(a109))))
% 61.22/61.24 [156]P9(a127,f120(f250(f3(a65),f3(a109))))
% 61.22/61.24 [157]P9(a128,f120(f250(f3(a76),f3(a109))))
% 61.22/61.24 [158]P9(a129,f120(f250(f3(a87),f3(a109))))
% 61.22/61.24 [159]P9(a130,f120(f250(f3(a98),f3(a109))))
% 61.22/61.24 [160]P9(a131,f120(f250(f3(a109),f3(a109))))
% 61.22/61.24 [161]P9(a134,f132(f250(f3(a2),f3(a1))))
% 61.22/61.24 [162]P9(a135,f132(f250(f3(a1),f3(a1))))
% 61.22/61.24 [163]P9(a146,f132(f250(f3(a4),f3(a1))))
% 61.22/61.24 [164]P9(a157,f132(f250(f3(a43),f3(a1))))
% 61.22/61.24 [165]P9(a167,f132(f250(f3(a54),f3(a1))))
% 61.22/61.24 [166]P9(a168,f132(f250(f3(a65),f3(a1))))
% 61.22/61.24 [167]P9(a169,f132(f250(f3(a76),f3(a1))))
% 61.22/61.24 [168]P9(a170,f132(f250(f3(a87),f3(a1))))
% 61.22/61.24 [169]P9(a171,f132(f250(f3(a98),f3(a1))))
% 61.22/61.24 [170]P9(a172,f132(f250(f3(a109),f3(a1))))
% 61.22/61.24 [171]P9(a174,f132(f250(f3(a2),f3(a4))))
% 61.22/61.24 [172]P9(a175,f132(f250(f3(a1),f3(a4))))
% 61.22/61.24 [173]P9(a176,f132(f250(f3(a4),f3(a4))))
% 61.22/61.24 [174]P9(a177,f132(f250(f3(a43),f3(a4))))
% 61.22/61.24 [175]P9(a178,f132(f250(f3(a54),f3(a4))))
% 61.22/61.24 [176]P9(a179,f132(f250(f3(a65),f3(a4))))
% 61.22/61.24 [177]P9(a180,f132(f250(f3(a76),f3(a4))))
% 61.22/61.24 [178]P9(a181,f132(f250(f3(a87),f3(a4))))
% 61.22/61.24 [179]P9(a182,f132(f250(f3(a98),f3(a4))))
% 61.22/61.24 [180]P9(a183,f132(f250(f3(a109),f3(a4))))
% 61.22/61.24 [181]P9(a185,f132(f250(f3(a2),f3(a43))))
% 61.22/61.24 [182]P9(a186,f132(f250(f3(a1),f3(a43))))
% 61.22/61.24 [183]P9(a187,f132(f250(f3(a4),f3(a43))))
% 61.22/61.24 [184]P9(a188,f132(f250(f3(a43),f3(a43))))
% 61.22/61.24 [185]P9(a189,f132(f250(f3(a54),f3(a43))))
% 61.22/61.24 [186]P9(a190,f132(f250(f3(a65),f3(a43))))
% 61.22/61.24 [187]P9(a191,f132(f250(f3(a76),f3(a43))))
% 61.22/61.24 [188]P9(a192,f132(f250(f3(a87),f3(a43))))
% 61.22/61.24 [189]P9(a193,f132(f250(f3(a98),f3(a43))))
% 61.22/61.24 [190]P9(a194,f132(f250(f3(a109),f3(a43))))
% 61.22/61.24 [191]P9(a196,f132(f250(f3(a2),f3(a54))))
% 61.22/61.24 [192]P9(a197,f132(f250(f3(a1),f3(a54))))
% 61.22/61.24 [193]P9(a198,f132(f250(f3(a4),f3(a54))))
% 61.22/61.24 [194]P9(a199,f132(f250(f3(a43),f3(a54))))
% 61.22/61.24 [195]P9(a200,f132(f250(f3(a54),f3(a54))))
% 61.22/61.24 [196]P9(a201,f132(f250(f3(a65),f3(a54))))
% 61.22/61.24 [197]P9(a202,f132(f250(f3(a76),f3(a54))))
% 61.22/61.24 [198]P9(a203,f132(f250(f3(a87),f3(a54))))
% 61.22/61.24 [199]P9(a204,f132(f250(f3(a98),f3(a54))))
% 61.22/61.24 [200]P9(a205,f132(f250(f3(a109),f3(a54))))
% 61.22/61.24 [201]P9(a207,f132(f250(f3(a2),f3(a65))))
% 61.22/61.24 [202]P9(a208,f132(f250(f3(a1),f3(a65))))
% 61.22/61.24 [203]P9(a209,f132(f250(f3(a4),f3(a65))))
% 61.22/61.24 [204]P9(a210,f132(f250(f3(a43),f3(a65))))
% 61.22/61.24 [205]P9(a211,f132(f250(f3(a54),f3(a65))))
% 61.22/61.24 [206]P9(a212,f132(f250(f3(a65),f3(a65))))
% 61.22/61.24 [207]P9(a213,f132(f250(f3(a76),f3(a65))))
% 61.22/61.24 [208]P9(a214,f132(f250(f3(a87),f3(a65))))
% 61.22/61.24 [209]P9(a215,f132(f250(f3(a98),f3(a65))))
% 61.22/61.24 [210]P9(a216,f132(f250(f3(a109),f3(a65))))
% 61.22/61.24 [211]P9(a218,f132(f250(f3(a2),f3(a76))))
% 61.22/61.24 [212]P9(a219,f132(f250(f3(a1),f3(a76))))
% 61.22/61.24 [213]P9(a220,f132(f250(f3(a4),f3(a76))))
% 61.22/61.24 [214]P9(a221,f132(f250(f3(a43),f3(a76))))
% 61.22/61.24 [215]P9(a222,f132(f250(f3(a54),f3(a76))))
% 61.22/61.24 [216]P9(a223,f132(f250(f3(a65),f3(a76))))
% 61.22/61.24 [217]P9(a224,f132(f250(f3(a76),f3(a76))))
% 61.22/61.24 [218]P9(a225,f132(f250(f3(a87),f3(a76))))
% 61.22/61.24 [219]P9(a226,f132(f250(f3(a98),f3(a76))))
% 61.22/61.24 [220]P9(a227,f132(f250(f3(a109),f3(a76))))
% 61.22/61.24 [221]P9(a229,f132(f250(f3(a2),f3(a87))))
% 61.22/61.24 [222]P9(a230,f132(f250(f3(a1),f3(a87))))
% 61.22/61.24 [223]P9(a231,f132(f250(f3(a4),f3(a87))))
% 61.22/61.24 [224]P9(a232,f132(f250(f3(a43),f3(a87))))
% 61.22/61.24 [225]P9(a233,f132(f250(f3(a54),f3(a87))))
% 61.22/61.24 [226]P9(a234,f132(f250(f3(a65),f3(a87))))
% 61.22/61.24 [227]P9(a235,f132(f250(f3(a76),f3(a87))))
% 61.22/61.24 [228]P9(a236,f132(f250(f3(a87),f3(a87))))
% 61.22/61.24 [229]P9(a237,f132(f250(f3(a98),f3(a87))))
% 61.22/61.24 [230]P9(a238,f132(f250(f3(a109),f3(a87))))
% 61.22/61.24 [231]P9(a240,f132(f250(f3(a2),f3(a98))))
% 61.22/61.24 [232]P9(a241,f132(f250(f3(a1),f3(a98))))
% 61.22/61.24 [233]P9(a242,f132(f250(f3(a4),f3(a98))))
% 61.22/61.24 [234]P9(a243,f132(f250(f3(a43),f3(a98))))
% 61.22/61.24 [235]P9(a244,f132(f250(f3(a54),f3(a98))))
% 61.22/61.24 [236]P9(a245,f132(f250(f3(a65),f3(a98))))
% 61.22/61.24 [237]P9(a246,f132(f250(f3(a76),f3(a98))))
% 61.22/61.24 [238]P9(a247,f132(f250(f3(a87),f3(a98))))
% 61.22/61.24 [239]P9(a248,f132(f250(f3(a98),f3(a98))))
% 61.22/61.24 [240]P9(a249,f132(f250(f3(a109),f3(a98))))
% 61.22/61.24 [241]P9(a251,f132(f250(f3(a2),f3(a109))))
% 61.22/61.24 [242]P9(a252,f132(f250(f3(a1),f3(a109))))
% 61.22/61.24 [243]P9(a253,f132(f250(f3(a4),f3(a109))))
% 61.22/61.24 [244]P9(a254,f132(f250(f3(a43),f3(a109))))
% 61.22/61.24 [245]P9(a255,f132(f250(f3(a54),f3(a109))))
% 61.22/61.24 [246]P9(a256,f132(f250(f3(a65),f3(a109))))
% 61.22/61.24 [247]P9(a257,f132(f250(f3(a76),f3(a109))))
% 61.22/61.24 [248]P9(a258,f132(f250(f3(a87),f3(a109))))
% 61.22/61.24 [249]P9(a259,f132(f250(f3(a98),f3(a109))))
% 61.22/61.24 [250]P9(a260,f132(f250(f3(a109),f3(a109))))
% 61.22/61.24 [251]P9(a7,f120(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [252]P9(a8,f120(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [253]P9(a9,f120(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [254]P9(a10,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [255]P9(a11,f120(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [256]P9(a12,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [257]P9(a13,f120(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [258]P9(a14,f120(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [259]P9(a15,f120(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [260]P9(a16,f120(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [261]P9(a18,f120(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [262]P9(a19,f120(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [263]P9(a20,f120(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [264]P9(a21,f120(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [265]P9(a22,f120(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [266]P9(a23,f120(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [267]P9(a24,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [268]P9(a25,f120(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [269]P9(a26,f120(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [270]P9(a27,f120(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [271]P9(a29,f120(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [272]P9(a30,f120(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [273]P9(a31,f120(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [274]P9(a32,f120(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [275]P9(a33,f120(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [276]P9(a34,f120(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [277]P9(a35,f120(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [278]P9(a36,f120(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [279]P9(a136,f132(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [280]P9(a137,f132(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [281]P9(a138,f132(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [282]P9(a139,f132(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [283]P9(a140,f132(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [284]P9(a141,f132(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [285]P9(a142,f132(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [286]P9(a143,f132(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [287]P9(a144,f132(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [288]P9(a145,f132(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 61.22/61.24 [289]P9(a147,f132(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [290]P9(a148,f132(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [291]P9(a149,f132(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [292]P9(a150,f132(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [293]P9(a151,f132(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [294]P9(a152,f132(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [295]P9(a153,f132(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [296]P9(a154,f132(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [297]P9(a155,f132(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [298]P9(a156,f132(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 61.22/61.24 [299]P9(a158,f132(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [300]P9(a159,f132(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [301]P9(a160,f132(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [302]P9(a161,f132(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [303]P9(a162,f132(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [304]P9(a163,f132(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [305]P9(a164,f132(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [306]P9(a165,f132(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [307]P9(a166,f132(f250(f3(a98),f250(f3(a4),f3(a1)))))
% 61.22/61.24 [410]P7(f3(x4101))+~P1(f3(x4101))
% 61.22/61.24 [408]~E(x4081,x4082)+P3(x4081,x4082)
% 61.22/61.24 [409]~P4(x4092,x4091)+~E(x4091,x4092)
% 61.22/61.24 [412]~P4(x4121,x4122)+P3(x4121,x4122)
% 61.22/61.24 [414]~P4(x4142,x4141)+~P4(x4141,x4142)
% 61.22/61.24 [415]~P7(x4152)+P7(f250(f3(x4151),x4152))
% 61.22/61.24 [425]~P5(x4253,x4251,x4252)+P10(x4251,x4252,x4253)
% 61.22/61.24 [426]~P10(x4262,x4263,x4261)+P5(x4261,x4262,x4263)
% 61.22/61.24 [416]~P7(x4163)+P8(f3(x4161),f250(f3(x4162),x4163))
% 61.22/61.24 [421]~P8(x4212,x4214)+P8(f250(f3(x4211),x4212),f250(f3(x4213),x4214))
% 61.22/61.24 [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))
% 61.22/61.24 [411]P4(x4112,x4111)+P4(x4111,x4112)+E(x4111,x4112)
% 61.22/61.24 [413]P4(x4131,x4132)+~P3(x4131,x4132)+E(x4131,x4132)
% 61.22/61.24 [423]P3(x4231,x4232)+~P4(x4231,x4233)+~P10(x4232,a1,x4233)
% 61.22/61.24 [420]P8(f3(x4201),f3(x4202))+~P8(f3(x4203),f3(x4202))+~P8(f3(x4201),f3(x4203))
% 61.22/61.24 [422]P10(x4221,x4222,a2)+~P9(x4221,f120(x4223))+~P9(x4222,f132(x4223))
% 61.22/61.24 [424]~P7(x4242)+~P8(f3(x4241),f3(x4243))+P8(f250(f3(x4241),x4242),f250(f3(x4243),x4242))
% 61.22/61.24 [427]~P10(x4273,x4274,x4271)+E(x4271,x4272)+~P10(x4273,x4274,x4272)
% 61.22/61.24 [428]~P10(x4283,x4281,x4284)+E(x4281,x4282)+~P10(x4283,x4282,x4284)
% 61.22/61.24 [429]~P10(x4291,x4293,x4294)+E(x4291,x4292)+~P10(x4292,x4293,x4294)
% 61.22/61.24 [417]P4(x4171,x4172)+~P9(x4172,f120(x4173))+~P9(x4171,f132(x4174))
% 61.22/61.24 [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))
% 61.22/61.24 [418]P4(x4181,x4182)+~P8(x4183,x4184)+~P9(x4182,f132(x4183))+~P9(x4181,f132(x4184))
% 61.22/61.24 [419]P4(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f120(x4194))+~P9(x4191,f120(x4193))
% 61.22/61.24 [430]~P10(x4302,x4301,x4303)+P10(x4301,x4302,x4303)+~P9(x4302,f120(x4304))+~P9(x4301,f132(x4305))
% 61.22/61.24 [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)))
% 61.22/61.24 [431]P10(x4311,x4312,x4313)+~P6(f3(a2),x4316,x4315,x4314)+~P9(x4313,f120(x4314))+~P9(x4312,f120(x4315))+~P9(x4311,f120(x4316))
% 61.22/61.24 [432]P10(x4321,x4322,x4323)+~P6(f3(a2),x4326,x4325,x4324)+~P9(x4323,f132(x4324))+~P9(x4322,f132(x4325))+~P9(x4321,f132(x4326))
% 61.22/61.24 [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))
% 61.22/61.24 [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))
% 61.22/61.24 [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))
% 61.22/61.24 [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))
% 61.22/61.24 %EqnAxiom
% 61.22/61.24 [1]E(x11,x11)
% 61.22/61.24 [2]E(x22,x21)+~E(x21,x22)
% 61.22/61.24 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 61.22/61.24 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 61.22/61.24 [5]~E(x51,x52)+E(f250(x51,x53),f250(x52,x53))
% 61.22/61.24 [6]~E(x61,x62)+E(f250(x63,x61),f250(x63,x62))
% 61.22/61.24 [7]~E(x71,x72)+E(f132(x71),f132(x72))
% 61.22/61.24 [8]~E(x81,x82)+E(f120(x81),f120(x82))
% 61.22/61.24 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 61.22/61.24 [10]P2(x102,x103,x104,x105)+~E(x101,x102)+~P2(x101,x103,x104,x105)
% 61.22/61.24 [11]P2(x113,x112,x114,x115)+~E(x111,x112)+~P2(x113,x111,x114,x115)
% 61.22/61.24 [12]P2(x123,x124,x122,x125)+~E(x121,x122)+~P2(x123,x124,x121,x125)
% 61.22/61.24 [13]P2(x133,x134,x135,x132)+~E(x131,x132)+~P2(x133,x134,x135,x131)
% 61.22/61.24 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 61.22/61.24 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 61.22/61.24 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 61.22/61.24 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 61.22/61.24 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 61.22/61.24 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193)
% 61.22/61.24 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201)
% 61.22/61.24 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213)
% 61.22/61.24 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221)
% 61.22/61.24 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233)
% 61.22/61.24 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241)
% 61.22/61.24 [25]P9(x252,x253)+~E(x251,x252)+~P9(x251,x253)
% 61.22/61.24 [26]P9(x263,x262)+~E(x261,x262)+~P9(x263,x261)
% 61.22/61.24 [27]P10(x272,x273,x274)+~E(x271,x272)+~P10(x271,x273,x274)
% 61.22/61.24 [28]P10(x283,x282,x284)+~E(x281,x282)+~P10(x283,x281,x284)
% 61.22/61.24 [29]P10(x293,x294,x292)+~E(x291,x292)+~P10(x293,x294,x291)
% 61.22/61.24 [30]P5(x302,x303,x304)+~E(x301,x302)+~P5(x301,x303,x304)
% 61.22/61.24 [31]P5(x313,x312,x314)+~E(x311,x312)+~P5(x313,x311,x314)
% 61.22/61.24 [32]P5(x323,x324,x322)+~E(x321,x322)+~P5(x323,x324,x321)
% 61.22/61.24
% 61.22/61.24 %-------------------------------------------
% 61.22/61.24 cnf(441,plain,
% 61.22/61.24 (~P4(x4411,x4411)),
% 61.22/61.24 inference(equality_inference,[],[409])).
% 61.22/61.24 cnf(442,plain,
% 61.22/61.24 (P10(a1,a121,a2)),
% 61.22/61.24 inference(scs_inference,[],[52,61,422])).
% 61.22/61.24 cnf(449,plain,
% 61.22/61.24 (~P4(x4491,x4491)),
% 61.22/61.24 inference(rename_variables,[],[441])).
% 61.22/61.24 cnf(450,plain,
% 61.22/61.24 (P10(a121,a1,a2)),
% 61.22/61.25 inference(scs_inference,[],[441,308,51,52,61,422,417,436,24,430])).
% 61.22/61.25 cnf(452,plain,
% 61.22/61.25 (~P8(f3(a1),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[441,449,308,51,52,61,422,417,436,24,430,418])).
% 61.22/61.25 cnf(453,plain,
% 61.22/61.25 (~P4(x4531,x4531)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(456,plain,
% 61.22/61.25 (~P4(x4561,x4561)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(458,plain,
% 61.22/61.25 (P10(a2,a2,a2)),
% 61.22/61.25 inference(scs_inference,[],[441,449,453,308,51,52,61,422,417,436,24,430,418,419,431])).
% 61.22/61.25 cnf(464,plain,
% 61.22/61.25 (~E(f3(a1),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[70,441,449,453,308,42,51,52,61,422,417,436,24,430,418,419,431,414,27,21,22])).
% 61.22/61.25 cnf(467,plain,
% 61.22/61.25 (~P8(f3(a1),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[70,441,449,453,456,308,42,51,52,61,422,417,436,24,430,418,419,431,414,27,21,22,23,420])).
% 61.22/61.25 cnf(476,plain,
% 61.22/61.25 (P10(a4,a133,a2)),
% 61.22/61.25 inference(scs_inference,[],[464,53,62,4,422])).
% 61.22/61.25 cnf(480,plain,
% 61.22/61.25 (~P8(f3(a4),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[464,467,309,43,53,62,308,4,422,436,420])).
% 61.22/61.25 cnf(482,plain,
% 61.22/61.25 (P4(a133,a4)),
% 61.22/61.25 inference(scs_inference,[],[464,467,309,43,53,62,308,4,422,436,420,417])).
% 61.22/61.25 cnf(484,plain,
% 61.22/61.25 (~E(f3(a4),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[464,452,467,309,43,53,62,308,4,422,436,420,417,22])).
% 61.22/61.25 cnf(485,plain,
% 61.22/61.25 (~E(a4,a133)),
% 61.22/61.25 inference(scs_inference,[],[464,441,452,467,309,43,53,62,308,4,422,436,420,417,22,24])).
% 61.22/61.25 cnf(486,plain,
% 61.22/61.25 (~P4(x4861,x4861)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(487,plain,
% 61.22/61.25 (~E(a133,a4)),
% 61.22/61.25 inference(scs_inference,[],[464,441,486,452,467,309,43,53,62,308,4,422,436,420,417,22,24,23])).
% 61.22/61.25 cnf(488,plain,
% 61.22/61.25 (~P4(x4881,x4881)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(489,plain,
% 61.22/61.25 (P10(a133,a4,a2)),
% 61.22/61.25 inference(scs_inference,[],[464,441,486,452,467,309,43,53,62,308,4,422,436,420,417,22,24,23,430])).
% 61.22/61.25 cnf(491,plain,
% 61.22/61.25 (~P8(f3(a4),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[464,441,486,488,452,467,309,43,53,62,308,4,422,436,420,417,22,24,23,430,418])).
% 61.22/61.25 cnf(492,plain,
% 61.22/61.25 (~P4(x4921,x4921)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(494,plain,
% 61.22/61.25 (~P8(f3(a43),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[464,441,486,488,492,452,467,309,43,53,54,62,308,4,422,436,420,417,22,24,23,430,418,419])).
% 61.22/61.25 cnf(497,plain,
% 61.22/61.25 (~P4(a4,a133)),
% 61.22/61.25 inference(scs_inference,[],[464,441,486,488,492,452,467,309,43,53,54,62,308,4,422,436,420,417,22,24,23,430,418,419,414])).
% 61.22/61.25 cnf(500,plain,
% 61.22/61.25 (~E(f3(a1),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[464,441,486,488,492,452,467,309,43,53,54,62,308,4,422,436,420,417,22,24,23,430,418,419,414,12,21])).
% 61.22/61.25 cnf(512,plain,
% 61.22/61.25 (~E(a4,a1)),
% 61.22/61.25 inference(scs_inference,[],[484,4])).
% 61.22/61.25 cnf(513,plain,
% 61.22/61.25 (P10(a43,a173,a2)),
% 61.22/61.25 inference(scs_inference,[],[484,63,54,4,422])).
% 61.22/61.25 cnf(517,plain,
% 61.22/61.25 (~P8(f3(a4),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[484,491,310,63,54,43,308,4,422,436,420])).
% 61.22/61.25 cnf(519,plain,
% 61.22/61.25 (P4(a173,a2)),
% 61.22/61.25 inference(scs_inference,[],[484,51,491,310,63,54,43,308,4,422,436,420,417])).
% 61.22/61.25 cnf(521,plain,
% 61.22/61.25 (~E(f3(a4),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[484,51,491,494,310,44,63,54,43,308,4,422,436,420,417,21])).
% 61.22/61.25 cnf(522,plain,
% 61.22/61.25 (~E(f3(a43),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[484,51,491,494,310,44,63,54,43,308,4,422,436,420,417,21,22])).
% 61.22/61.25 cnf(523,plain,
% 61.22/61.25 (~E(a2,a173)),
% 61.22/61.25 inference(scs_inference,[],[484,441,51,491,494,310,44,63,54,43,308,4,422,436,420,417,21,22,24])).
% 61.22/61.25 cnf(524,plain,
% 61.22/61.25 (~P4(x5241,x5241)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(525,plain,
% 61.22/61.25 (~E(a173,a2)),
% 61.22/61.25 inference(scs_inference,[],[484,441,524,51,491,494,310,44,63,54,43,308,4,422,436,420,417,21,22,24,23])).
% 61.22/61.25 cnf(526,plain,
% 61.22/61.25 (~P4(x5261,x5261)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(527,plain,
% 61.22/61.25 (P10(a173,a43,a2)),
% 61.22/61.25 inference(scs_inference,[],[484,441,524,51,491,494,310,44,63,54,43,308,4,422,436,420,417,21,22,24,23,430])).
% 61.22/61.25 cnf(529,plain,
% 61.22/61.25 (~P8(f3(a54),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[484,441,524,526,51,491,494,310,44,63,64,54,43,308,4,422,436,420,417,21,22,24,23,430,418])).
% 61.22/61.25 cnf(530,plain,
% 61.22/61.25 (~P4(x5301,x5301)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(532,plain,
% 61.22/61.25 (~P8(f3(a65),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[484,441,524,526,530,51,491,494,310,44,56,63,64,54,43,308,4,422,436,420,417,21,22,24,23,430,418,419])).
% 61.22/61.25 cnf(535,plain,
% 61.22/61.25 (~P4(a2,a173)),
% 61.22/61.25 inference(scs_inference,[],[484,441,524,526,530,51,491,494,310,44,56,63,64,54,43,308,4,422,436,420,417,21,22,24,23,430,418,419,414])).
% 61.22/61.25 cnf(541,plain,
% 61.22/61.25 (~E(a1,a4)),
% 61.22/61.25 inference(scs_inference,[],[500,4])).
% 61.22/61.25 cnf(546,plain,
% 61.22/61.25 (P10(a65,a195,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,500,519,311,65,56,308,4,423,436,422])).
% 61.22/61.25 cnf(548,plain,
% 61.22/61.25 (~P8(f3(a54),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,500,529,519,311,45,65,56,308,4,423,436,422,420])).
% 61.22/61.25 cnf(550,plain,
% 61.22/61.25 (P4(a195,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,500,51,529,519,311,45,65,56,308,4,423,436,422,420,417])).
% 61.22/61.25 cnf(552,plain,
% 61.22/61.25 (~E(f3(a43),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,500,51,529,519,311,45,65,56,308,4,423,436,422,420,417,21])).
% 61.22/61.25 cnf(553,plain,
% 61.22/61.25 (~E(a2,a195)),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,51,529,519,311,45,65,56,308,4,423,436,422,420,417,21,24])).
% 61.22/61.25 cnf(554,plain,
% 61.22/61.25 (~P4(x5541,x5541)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(555,plain,
% 61.22/61.25 (~E(a195,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,554,51,529,519,311,45,65,56,308,4,423,436,422,420,417,21,24,23])).
% 61.22/61.25 cnf(556,plain,
% 61.22/61.25 (~P4(x5561,x5561)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(557,plain,
% 61.22/61.25 (~E(f3(a54),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,554,51,529,519,311,45,65,494,56,308,4,423,436,422,420,417,21,24,23,22])).
% 61.22/61.25 cnf(558,plain,
% 61.22/61.25 (P10(a195,a65,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,554,51,529,519,311,45,65,494,56,308,4,423,436,422,420,417,21,24,23,22,430])).
% 61.22/61.25 cnf(560,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,554,556,51,529,519,311,45,57,65,494,56,308,4,423,436,422,420,417,21,24,23,22,430,419])).
% 61.22/61.25 cnf(561,plain,
% 61.22/61.25 (~P4(x5611,x5611)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(563,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,554,556,561,51,529,519,311,45,57,65,67,494,56,308,4,423,436,422,420,417,21,24,23,22,430,419,418])).
% 61.22/61.25 cnf(566,plain,
% 61.22/61.25 (~P4(a2,a195)),
% 61.22/61.25 inference(scs_inference,[],[450,500,441,554,556,561,51,529,519,311,45,57,65,67,494,56,308,4,423,436,422,420,417,21,24,23,22,430,419,418,414])).
% 61.22/61.25 cnf(580,plain,
% 61.22/61.25 (~E(a4,a43)),
% 61.22/61.25 inference(scs_inference,[],[521,4])).
% 61.22/61.25 cnf(587,plain,
% 61.22/61.25 (~P8(f3(a65),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,521,550,532,312,46,66,57,308,4,423,436,422,420])).
% 61.22/61.25 cnf(589,plain,
% 61.22/61.25 (P4(a206,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,521,51,550,532,312,46,66,57,308,4,423,436,422,420,417])).
% 61.22/61.25 cnf(591,plain,
% 61.22/61.25 (~E(a2,a206)),
% 61.22/61.25 inference(scs_inference,[],[450,521,441,51,550,532,312,46,66,57,308,4,423,436,422,420,417,24])).
% 61.22/61.25 cnf(592,plain,
% 61.22/61.25 (~P4(x5921,x5921)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(593,plain,
% 61.22/61.25 (~E(f3(a54),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,521,441,51,550,532,312,46,66,57,308,4,423,436,422,420,417,24,21])).
% 61.22/61.25 cnf(594,plain,
% 61.22/61.25 (~E(f3(a65),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,521,441,51,550,532,548,312,46,66,57,308,4,423,436,422,420,417,24,21,22])).
% 61.22/61.25 cnf(596,plain,
% 61.22/61.25 (~P4(x5961,x5961)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(599,plain,
% 61.22/61.25 (~P8(f3(a98),f3(a98))),
% 61.22/61.25 inference(scs_inference,[],[450,521,441,592,596,51,550,532,548,312,46,59,66,57,308,4,423,436,422,420,417,24,21,22,23,430,419])).
% 61.22/61.25 cnf(600,plain,
% 61.22/61.25 (~P4(x6001,x6001)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(602,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,521,441,592,596,600,51,550,532,548,312,46,59,66,69,57,308,4,423,436,422,420,417,24,21,22,23,430,419,418])).
% 61.22/61.25 cnf(605,plain,
% 61.22/61.25 (~P4(a2,a206)),
% 61.22/61.25 inference(scs_inference,[],[450,521,441,592,596,600,51,550,532,548,312,46,59,66,69,57,308,4,423,436,422,420,417,24,21,22,23,430,419,418,414])).
% 61.22/61.25 cnf(626,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,522,560,589,313,47,68,59,308,4,423,436,422,420])).
% 61.22/61.25 cnf(628,plain,
% 61.22/61.25 (P4(a228,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,522,51,560,589,313,47,68,59,308,4,423,436,422,420,417])).
% 61.22/61.25 cnf(630,plain,
% 61.22/61.25 (~E(f3(a65),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,522,51,560,589,313,47,68,59,308,4,423,436,422,420,417,21])).
% 61.22/61.25 cnf(633,plain,
% 61.22/61.25 (~E(f3(a76),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,522,441,51,560,589,587,313,47,68,59,308,4,423,436,422,420,417,21,23,22])).
% 61.22/61.25 cnf(659,plain,
% 61.22/61.25 (~E(a43,a54)),
% 61.22/61.25 inference(scs_inference,[],[552,4])).
% 61.22/61.25 cnf(666,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,552,563,628,314,48,161,71,308,4,423,436,422,420])).
% 61.22/61.25 cnf(668,plain,
% 61.22/61.25 (P4(a134,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,552,51,563,628,314,48,161,71,308,4,423,436,422,420,417])).
% 61.22/61.25 cnf(671,plain,
% 61.22/61.25 (~P4(x6711,x6711)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(674,plain,
% 61.22/61.25 (~E(f3(a76),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,552,441,671,51,563,628,314,48,161,71,308,4,423,436,422,420,417,24,23,21])).
% 61.22/61.25 cnf(675,plain,
% 61.22/61.25 (~E(f3(a87),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,552,441,671,51,563,628,626,314,48,161,71,308,4,423,436,422,420,417,24,23,21,22])).
% 61.22/61.25 cnf(703,plain,
% 61.22/61.25 (~P8(f3(a98),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,557,599,668,315,49,308,4,436,423,420])).
% 61.22/61.25 cnf(707,plain,
% 61.22/61.25 (P4(a146,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,557,51,599,668,315,49,163,73,308,4,436,423,420,422,417])).
% 61.22/61.25 cnf(711,plain,
% 61.22/61.25 (~E(f3(a98),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,557,441,51,599,668,666,315,49,163,73,308,4,436,423,420,422,417,23,22])).
% 61.22/61.25 cnf(712,plain,
% 61.22/61.25 (~E(f3(a87),f3(a98))),
% 61.22/61.25 inference(scs_inference,[],[450,557,441,51,599,668,666,315,49,163,73,308,4,436,423,420,422,417,23,22,21])).
% 61.22/61.25 cnf(744,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a98))),
% 61.22/61.25 inference(scs_inference,[],[450,593,602,707,316,50,165,75,308,4,423,436,422,420])).
% 61.22/61.25 cnf(746,plain,
% 61.22/61.25 (P4(a167,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,593,51,602,707,316,50,165,75,308,4,423,436,422,420,417])).
% 61.22/61.25 cnf(748,plain,
% 61.22/61.25 (~E(f3(a109),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,593,51,602,707,703,316,50,165,75,308,4,423,436,422,420,417,22])).
% 61.22/61.25 cnf(750,plain,
% 61.22/61.25 (~P4(x7501,x7501)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(753,plain,
% 61.22/61.25 (~E(f3(a98),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,593,441,750,51,602,707,703,316,50,165,75,308,4,423,436,422,420,417,22,24,23,21])).
% 61.22/61.25 cnf(771,plain,
% 61.22/61.25 (~P8(f3(a43),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[594,480,167,77,44,4,422,420])).
% 61.22/61.25 cnf(777,plain,
% 61.22/61.25 (P4(a169,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,594,51,746,480,317,167,77,44,308,4,422,420,423,436,417])).
% 61.22/61.25 cnf(780,plain,
% 61.22/61.25 (~P4(x7801,x7801)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(783,plain,
% 61.22/61.25 (~E(f3(a4),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,594,441,780,51,746,480,317,167,548,77,44,308,4,422,420,423,436,417,24,23,21])).
% 61.22/61.25 cnf(784,plain,
% 61.22/61.25 (~E(f3(a43),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,594,441,780,51,746,480,317,167,548,77,44,308,4,422,420,423,436,417,24,23,21,22])).
% 61.22/61.25 cnf(806,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,630,777,744,318,169,79,49,4,423,422,436,420])).
% 61.22/61.25 cnf(808,plain,
% 61.22/61.25 (P4(a171,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,630,51,777,744,318,169,79,49,4,423,422,436,420,417])).
% 61.22/61.25 cnf(811,plain,
% 61.22/61.25 (~P4(x8111,x8111)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(812,plain,
% 61.22/61.25 (~E(f3(a2),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,630,441,51,777,517,744,318,169,79,42,49,4,423,422,436,420,417,23,21])).
% 61.22/61.25 cnf(815,plain,
% 61.22/61.25 (~E(f3(a54),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,630,441,811,51,777,517,744,771,318,169,79,42,45,49,4,423,422,436,420,417,23,21,24,22])).
% 61.22/61.25 cnf(836,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,633,808,806,319,318,48,4,423,436,420])).
% 61.22/61.25 cnf(840,plain,
% 61.22/61.25 (P4(a174,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,633,51,808,806,319,171,81,318,48,4,423,436,420,422,417])).
% 61.22/61.25 cnf(842,plain,
% 61.22/61.25 (~E(f3(a54),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,633,51,808,806,319,171,626,81,318,46,48,4,423,436,420,422,417,21])).
% 61.22/61.25 cnf(844,plain,
% 61.22/61.25 (~P4(x8441,x8441)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(847,plain,
% 61.22/61.25 (~E(f3(a65),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,633,441,844,51,808,806,319,171,626,81,529,318,46,48,4,423,436,420,422,417,21,24,23,22])).
% 61.22/61.25 cnf(863,plain,
% 61.22/61.25 (~E(a76,a87)),
% 61.22/61.25 inference(scs_inference,[],[674,4])).
% 61.22/61.25 cnf(864,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[674,836,47,4,420])).
% 61.22/61.25 cnf(872,plain,
% 61.22/61.25 (P4(a176,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,674,51,840,836,320,173,83,309,47,4,420,423,422,436,417])).
% 61.22/61.25 cnf(875,plain,
% 61.22/61.25 (~P4(x8751,x8751)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(877,plain,
% 61.22/61.25 (~P4(x8771,x8771)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(878,plain,
% 61.22/61.25 (~E(f3(a65),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,674,441,875,51,840,836,320,173,83,309,47,4,420,423,422,436,417,24,23,21])).
% 61.22/61.25 cnf(879,plain,
% 61.22/61.25 (~E(f3(a87),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,674,441,875,51,840,836,320,173,83,560,309,47,48,4,420,423,422,436,417,24,23,21,22])).
% 61.22/61.25 cnf(881,plain,
% 61.22/61.25 (~P4(x8811,x8811)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(893,plain,
% 61.22/61.25 (P9(x8931,f120(f3(a2)))+~E(a2,x8931)),
% 61.22/61.25 inference(scs_inference,[],[450,674,441,875,877,881,51,840,836,320,173,175,86,83,560,309,47,48,4,420,423,422,436,417,24,23,21,22,418,430,419,414,10,13,28,25])).
% 61.22/61.25 cnf(905,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[748,864,176,86,46,4,422,420])).
% 61.22/61.25 cnf(911,plain,
% 61.22/61.25 (P4(a179,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,748,51,872,864,321,176,86,318,46,4,422,420,436,423,417])).
% 61.22/61.25 cnf(914,plain,
% 61.22/61.25 (~P4(x9141,x9141)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(915,plain,
% 61.22/61.25 (~E(f3(a43),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,748,441,51,872,864,321,176,587,86,318,45,46,4,422,420,436,423,417,23,21])).
% 61.22/61.25 cnf(918,plain,
% 61.22/61.25 (~E(f3(a43),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[450,748,441,914,51,872,864,321,176,517,587,86,318,45,44,46,4,422,420,436,423,417,23,21,24,22])).
% 61.22/61.25 cnf(948,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,815,911,905,322,177,87,309,45,4,436,422,423,420])).
% 61.22/61.25 cnf(950,plain,
% 61.22/61.25 (P4(a180,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,815,51,911,905,322,177,87,309,45,4,436,422,423,420,417])).
% 61.22/61.25 cnf(952,plain,
% 61.22/61.25 (~E(f3(a87),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,815,51,911,905,322,177,744,87,309,49,45,4,436,422,423,420,417,21])).
% 61.22/61.25 cnf(954,plain,
% 61.22/61.25 (~P4(x9541,x9541)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(957,plain,
% 61.22/61.25 (~E(f3(a76),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,815,441,954,51,911,905,322,177,744,87,532,309,49,45,47,4,436,422,423,420,417,21,24,23,22])).
% 61.22/61.25 cnf(977,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,711,950,948,323,318,44,4,423,436,420])).
% 61.22/61.25 cnf(981,plain,
% 61.22/61.25 (P4(a182,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,711,51,950,948,323,179,89,318,44,4,423,436,420,422,417])).
% 61.22/61.25 cnf(984,plain,
% 61.22/61.25 (~P4(x9841,x9841)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.25 cnf(987,plain,
% 61.22/61.25 (~E(f3(a76),f3(a98))),
% 61.22/61.25 inference(scs_inference,[],[450,711,441,984,51,950,948,323,179,703,89,318,48,44,4,423,436,420,422,417,24,23,21])).
% 61.22/61.25 cnf(1002,plain,
% 61.22/61.25 (P7(f250(f3(x10021),f3(a1)))),
% 61.22/61.25 inference(scs_inference,[],[33,410,415])).
% 61.22/61.25 cnf(1004,plain,
% 61.22/61.25 (~P8(f3(a109),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[753,43,977,4,420])).
% 61.22/61.25 cnf(1010,plain,
% 61.22/61.25 (P4(a186,a2)),
% 61.22/61.25 inference(scs_inference,[],[450,753,51,43,981,977,182,92,4,420,423,422,417])).
% 61.22/61.25 cnf(1014,plain,
% 61.22/61.25 (~E(f3(a109),f3(a98))),
% 61.22/61.25 inference(scs_inference,[],[450,753,51,50,43,981,977,324,182,92,599,309,4,420,423,422,417,436,22])).
% 61.22/61.25 cnf(1017,plain,
% 61.22/61.25 (~E(f3(a1),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,753,441,51,50,43,981,977,324,182,92,599,309,4,420,423,422,417,436,22,23,21])).
% 61.22/61.25 cnf(1039,plain,
% 61.22/61.25 (P4(a188,a2)),
% 61.22/61.25 inference(scs_inference,[],[675,51,42,1004,184,94,4,422,420,417])).
% 61.22/61.25 cnf(1047,plain,
% 61.22/61.25 (~E(f3(a2),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,675,441,51,42,1010,1004,325,184,94,318,4,422,420,417,436,423,23,21])).
% 61.22/61.25 cnf(1073,plain,
% 61.22/61.25 (P4(a190,a2)),
% 61.22/61.25 inference(scs_inference,[],[712,51,186,4,417])).
% 61.22/61.25 cnf(1081,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,712,51,47,1039,326,186,666,96,309,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1083,plain,
% 61.22/61.25 (~E(f3(a43),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,712,51,45,47,1039,326,186,666,905,96,309,4,417,422,436,423,420,21])).
% 61.22/61.25 cnf(1106,plain,
% 61.22/61.25 (P4(a192,a2)),
% 61.22/61.25 inference(scs_inference,[],[952,51,188,4,417])).
% 61.22/61.25 cnf(1108,plain,
% 61.22/61.25 (P6(f3(a2),f3(a4),f3(a2),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[952,51,328,188,4,417,436])).
% 61.22/61.25 cnf(1114,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,952,51,46,1073,1081,328,188,98,4,417,436,422,423,420])).
% 61.22/61.25 cnf(1116,plain,
% 61.22/61.25 (~E(f3(a98),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,952,51,49,46,1073,1081,328,188,98,4,417,436,422,423,420,22])).
% 61.22/61.25 cnf(1119,plain,
% 61.22/61.25 (~E(f3(a54),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,952,441,51,49,46,1073,1081,328,188,98,4,417,436,422,423,420,22,24,21])).
% 61.22/61.25 cnf(1144,plain,
% 61.22/61.25 (~E(a4,a54)),
% 61.22/61.25 inference(scs_inference,[],[783,4])).
% 61.22/61.25 cnf(1145,plain,
% 61.22/61.25 (P4(a194,a2)),
% 61.22/61.25 inference(scs_inference,[],[783,51,190,4,417])).
% 61.22/61.25 cnf(1153,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,783,51,45,1106,1114,329,190,328,100,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1155,plain,
% 61.22/61.25 (~E(f3(a98),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,783,51,49,45,1106,1114,329,190,328,100,4,417,422,436,423,420,22])).
% 61.22/61.25 cnf(1158,plain,
% 61.22/61.25 (~E(f3(a76),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,783,441,51,48,49,45,1106,1114,329,190,806,328,100,4,417,422,436,423,420,22,23,21])).
% 61.22/61.25 cnf(1175,plain,
% 61.22/61.25 (~E(a43,a2)),
% 61.22/61.25 inference(scs_inference,[],[784,4])).
% 61.22/61.25 cnf(1176,plain,
% 61.22/61.25 (P4(a197,a2)),
% 61.22/61.25 inference(scs_inference,[],[784,51,192,4,417])).
% 61.22/61.25 cnf(1184,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,784,51,44,1145,1153,330,192,102,310,4,417,436,422,423,420])).
% 61.22/61.25 cnf(1186,plain,
% 61.22/61.25 (~E(f3(a98),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,784,51,44,49,1145,1153,330,192,102,310,4,417,436,422,423,420,22])).
% 61.22/61.25 cnf(1189,plain,
% 61.22/61.25 (~E(f3(a4),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,784,441,51,44,49,1145,1153,330,192,102,310,4,417,436,422,423,420,22,24,21])).
% 61.22/61.25 cnf(1208,plain,
% 61.22/61.25 (P4(a199,a2)),
% 61.22/61.25 inference(scs_inference,[],[812,51,194,4,417])).
% 61.22/61.25 cnf(1216,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[450,812,51,43,1176,1184,331,194,104,319,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1218,plain,
% 61.22/61.25 (~E(f3(a98),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,812,51,43,49,1176,1184,331,194,104,319,4,417,422,436,423,420,22])).
% 61.22/61.25 cnf(1221,plain,
% 61.22/61.25 (~E(f3(a1),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,812,441,51,43,49,1176,1184,331,194,104,319,4,417,422,436,423,420,22,23,21])).
% 61.22/61.25 cnf(1244,plain,
% 61.22/61.25 (P4(a201,a2)),
% 61.22/61.25 inference(scs_inference,[],[842,51,196,4,417])).
% 61.22/61.25 cnf(1252,plain,
% 61.22/61.25 (~P8(f3(a87),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,842,51,42,1208,1216,332,196,106,328,4,417,436,422,423,420])).
% 61.22/61.25 cnf(1254,plain,
% 61.22/61.25 (~E(f3(a98),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[450,842,51,42,49,1208,1216,332,196,106,328,4,417,436,422,423,420,22])).
% 61.22/61.25 cnf(1283,plain,
% 61.22/61.25 (P4(a203,a2)),
% 61.22/61.25 inference(scs_inference,[],[847,51,198,4,417])).
% 61.22/61.25 cnf(1291,plain,
% 61.22/61.25 (~P8(f3(a98),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,847,51,49,1244,1252,333,198,108,310,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1293,plain,
% 61.22/61.25 (~E(f3(a98),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,847,51,49,1244,1252,333,198,108,310,4,417,422,436,423,420,22])).
% 61.22/61.25 cnf(1294,plain,
% 61.22/61.25 (~E(f3(a65),f3(a87))),
% 61.22/61.25 inference(scs_inference,[],[450,847,51,47,49,1244,1252,333,198,108,666,310,4,417,422,436,423,420,22,21])).
% 61.22/61.25 cnf(1322,plain,
% 61.22/61.25 (P4(a204,a2)),
% 61.22/61.25 inference(scs_inference,[],[878,51,199,4,417])).
% 61.22/61.25 cnf(1330,plain,
% 61.22/61.25 (~P8(f3(a54),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,878,51,45,1283,334,199,771,109,319,4,417,436,422,423,420])).
% 61.22/61.25 cnf(1332,plain,
% 61.22/61.25 (~E(f3(a109),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,878,51,50,45,1283,1291,334,199,771,109,319,4,417,436,422,423,420,22])).
% 61.22/61.25 cnf(1335,plain,
% 61.22/61.25 (~E(f3(a54),f3(a109))),
% 61.22/61.25 inference(scs_inference,[],[450,878,441,51,50,45,46,1283,1291,334,199,771,864,109,319,4,417,436,422,423,420,22,24,21])).
% 61.22/61.25 cnf(1360,plain,
% 61.22/61.25 (~E(a43,a65)),
% 61.22/61.25 inference(scs_inference,[],[915,4])).
% 61.22/61.25 cnf(1369,plain,
% 61.22/61.25 (~P8(f3(a65),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,915,51,46,1322,1330,335,202,112,328,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1373,plain,
% 61.22/61.25 (~E(f3(a65),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,915,441,51,46,1322,1330,335,202,112,328,4,417,422,436,423,420,23,22])).
% 61.22/61.25 cnf(1400,plain,
% 61.22/61.25 (P4(a210,a2)),
% 61.22/61.25 inference(scs_inference,[],[1332,51,204,4,417])).
% 61.22/61.25 cnf(1406,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[1332,51,47,1369,338,204,114,4,417,436,422,420])).
% 61.22/61.25 cnf(1446,plain,
% 61.22/61.25 (~P8(f3(a43),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,879,51,44,1400,339,206,311,116,494,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1450,plain,
% 61.22/61.25 (~E(f3(a87),f3(a2))),
% 61.22/61.25 inference(scs_inference,[],[450,879,441,51,48,44,1400,1406,339,206,311,116,494,4,417,422,436,423,420,24,22])).
% 61.22/61.25 cnf(1476,plain,
% 61.22/61.25 (~E(a43,a1)),
% 61.22/61.25 inference(scs_inference,[],[918,4])).
% 61.22/61.25 cnf(1477,plain,
% 61.22/61.25 (P4(a214,a2)),
% 61.22/61.25 inference(scs_inference,[],[918,51,208,4,417])).
% 61.22/61.25 cnf(1483,plain,
% 61.22/61.25 (~P8(f3(a43),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[918,51,43,1446,340,208,338,118,4,417,436,422,420])).
% 61.22/61.25 cnf(1524,plain,
% 61.22/61.25 (~P8(f3(a54),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,1450,51,44,1477,341,210,120,548,311,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1526,plain,
% 61.22/61.25 (~E(f3(a2),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,1450,51,42,44,1477,1483,341,210,120,548,311,4,417,422,436,423,420,21])).
% 61.22/61.25 cnf(1555,plain,
% 61.22/61.25 (~E(a76,a65)),
% 61.22/61.25 inference(scs_inference,[],[957,4])).
% 61.22/61.25 cnf(1556,plain,
% 61.22/61.25 (P4(a219,a2)),
% 61.22/61.25 inference(scs_inference,[],[957,51,212,4,417])).
% 61.22/61.25 cnf(1562,plain,
% 61.22/61.25 (~P8(f3(a54),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[957,51,43,1524,342,212,122,329,4,417,436,422,420])).
% 61.22/61.25 cnf(1594,plain,
% 61.22/61.25 (~E(a76,a98)),
% 61.22/61.25 inference(scs_inference,[],[987,4])).
% 61.22/61.25 cnf(1595,plain,
% 61.22/61.25 (P4(a221,a2)),
% 61.22/61.25 inference(scs_inference,[],[987,51,214,4,417])).
% 61.22/61.25 cnf(1603,plain,
% 61.22/61.25 (~P8(f3(a65),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,987,51,45,1556,343,214,124,587,338,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1606,plain,
% 61.22/61.25 (~E(f3(a2),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,987,51,42,45,46,1556,1562,343,214,124,587,338,4,417,422,436,423,420,22,21])).
% 61.22/61.25 cnf(1634,plain,
% 61.22/61.25 (P4(a223,a2)),
% 61.22/61.25 inference(scs_inference,[],[1014,51,216,4,417])).
% 61.22/61.25 cnf(1642,plain,
% 61.22/61.25 (~P8(f3(a65),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,1014,51,44,1595,1603,344,216,126,311,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1673,plain,
% 61.22/61.25 (P4(a225,a2)),
% 61.22/61.25 inference(scs_inference,[],[1017,51,218,4,417])).
% 61.22/61.25 cnf(1686,plain,
% 61.22/61.25 (~E(f3(a1),f3(a65))),
% 61.22/61.25 inference(scs_inference,[],[450,1017,441,51,47,43,1634,1642,348,218,128,4,417,422,436,423,420,22,24,21])).
% 61.22/61.25 cnf(1705,plain,
% 61.22/61.25 (P4(a227,a2)),
% 61.22/61.25 inference(scs_inference,[],[1047,51,220,4,417])).
% 61.22/61.25 cnf(1713,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a54))),
% 61.22/61.25 inference(scs_inference,[],[450,1047,51,46,1673,349,220,321,130,626,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1745,plain,
% 61.22/61.25 (P4(a230,a2)),
% 61.22/61.25 inference(scs_inference,[],[1083,51,222,4,417])).
% 61.22/61.25 cnf(1753,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,1083,51,45,1705,1713,350,222,339,132,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1784,plain,
% 61.22/61.25 (P4(a232,a2)),
% 61.22/61.25 inference(scs_inference,[],[1116,51,224,4,417])).
% 61.22/61.25 cnf(1792,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a4))),
% 61.22/61.25 inference(scs_inference,[],[450,1116,51,44,1745,1753,351,224,348,134,4,417,422,436,423,420])).
% 61.22/61.25 cnf(1794,plain,
% 61.22/61.25 (~E(f3(a87),f3(a43))),
% 61.22/61.25 inference(scs_inference,[],[450,1116,51,48,44,1745,1753,351,224,348,134,4,417,422,436,423,420,22])).
% 61.22/61.25 cnf(1823,plain,
% 61.22/61.25 (P4(a234,a2)),
% 61.22/61.25 inference(scs_inference,[],[1119,51,226,4,417])).
% 61.22/61.25 cnf(1831,plain,
% 61.22/61.25 (~P8(f3(a76),f3(a1))),
% 61.22/61.25 inference(scs_inference,[],[450,1119,51,43,1784,1792,352,226,136,321,4,417,436,422,423,420])).
% 61.22/61.25 cnf(1864,plain,
% 61.22/61.25 (P4(a236,a2)),
% 61.22/61.25 inference(scs_inference,[],[1155,51,228,138,4,422,417])).
% 61.22/61.25 cnf(1870,plain,
% 61.22/61.25 (~P8(f3(a98),f3(a76))),
% 61.22/61.25 inference(scs_inference,[],[450,1155,51,48,1823,353,228,138,703,330,4,422,417,436,423,420])).
% 61.22/61.25 cnf(1874,plain,
% 61.22/61.25 (~P4(x18741,x18741)),
% 61.22/61.25 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(1877,plain,
% 61.22/61.26 (~P4(x18771,x18771)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(1880,plain,
% 61.22/61.26 (~P8(f250(f3(a98),f3(a87)),f250(f3(a98),f3(a87)))),
% 61.22/61.26 inference(scs_inference,[],[450,1155,441,1874,1877,51,42,48,1823,1831,353,228,139,138,703,330,4,422,417,436,423,420,22,24,21,23,430,419])).
% 61.22/61.26 cnf(1900,plain,
% 61.22/61.26 (~E(a76,a109)),
% 61.22/61.26 inference(scs_inference,[],[1158,4])).
% 61.22/61.26 cnf(1905,plain,
% 61.22/61.26 (P4(a237,a2)),
% 61.22/61.26 inference(scs_inference,[],[1158,51,358,229,139,4,436,422,417])).
% 61.22/61.26 cnf(1907,plain,
% 61.22/61.26 (P3(a236,a121)),
% 61.22/61.26 inference(scs_inference,[],[450,1158,51,1864,358,229,139,4,436,422,417,423])).
% 61.22/61.26 cnf(1909,plain,
% 61.22/61.26 (~P8(f3(a98),f3(a65))),
% 61.22/61.26 inference(scs_inference,[],[450,1158,51,47,1864,1870,358,229,139,4,436,422,417,423,420])).
% 61.22/61.26 cnf(1914,plain,
% 61.22/61.26 (~E(f3(a65),f3(a98))),
% 61.22/61.26 inference(scs_inference,[],[450,1158,441,51,50,47,1864,1870,358,229,139,4,436,422,417,423,420,24,22,21])).
% 61.22/61.26 cnf(1940,plain,
% 61.22/61.26 (P4(a184,a2)),
% 61.22/61.26 inference(scs_inference,[],[1606,51,64,4,417])).
% 61.22/61.26 cnf(1948,plain,
% 61.22/61.26 (~P8(f3(a98),f3(a54))),
% 61.22/61.26 inference(scs_inference,[],[450,1606,51,46,55,64,1905,1909,359,313,4,417,436,422,423,420])).
% 61.22/61.26 cnf(1980,plain,
% 61.22/61.26 (P10(a111,a241,a2)),
% 61.22/61.26 inference(scs_inference,[],[1186,232,142,4,422])).
% 61.22/61.26 cnf(1982,plain,
% 61.22/61.26 (P4(a184,a54)),
% 61.22/61.26 inference(scs_inference,[],[1186,55,64,232,142,4,422,417])).
% 61.22/61.26 cnf(1988,plain,
% 61.22/61.26 (~P8(f3(a98),f3(a43))),
% 61.22/61.26 inference(scs_inference,[],[450,1186,45,55,64,1940,1948,360,232,340,142,4,422,417,436,423,420])).
% 61.22/61.26 cnf(2016,plain,
% 61.22/61.26 (~E(a4,a87)),
% 61.22/61.26 inference(scs_inference,[],[1189,4])).
% 61.22/61.26 cnf(2017,plain,
% 61.22/61.26 (P10(a112,a242,a2)),
% 61.22/61.26 inference(scs_inference,[],[1189,233,143,4,422])).
% 61.22/61.26 cnf(2019,plain,
% 61.22/61.26 (P4(a184,a6)),
% 61.22/61.26 inference(scs_inference,[],[1189,64,233,72,143,4,422,417])).
% 61.22/61.26 cnf(2028,plain,
% 61.22/61.26 (~E(f3(a4),f3(a98))),
% 61.22/61.26 inference(scs_inference,[],[1189,441,50,44,64,1988,361,233,72,349,143,4,422,417,436,420,24,22,21])).
% 61.22/61.26 cnf(2052,plain,
% 61.22/61.26 (P10(a115,a245,a2)),
% 61.22/61.26 inference(scs_inference,[],[1218,236,146,4,422])).
% 61.22/61.26 cnf(2087,plain,
% 61.22/61.26 (P10(a117,a247,a2)),
% 61.22/61.26 inference(scs_inference,[],[1221,238,148,4,422])).
% 61.22/61.26 cnf(2122,plain,
% 61.22/61.26 (P10(a119,a249,a2)),
% 61.22/61.26 inference(scs_inference,[],[1254,240,150,4,422])).
% 61.22/61.26 cnf(2154,plain,
% 61.22/61.26 (P10(a123,a252,a2)),
% 61.22/61.26 inference(scs_inference,[],[1335,242,152,4,422])).
% 61.22/61.26 cnf(2221,plain,
% 61.22/61.26 (P6(f3(a2),f3(a87),f3(a2),f3(a87))),
% 61.22/61.26 inference(scs_inference,[],[1293,64,378,246,84,156,4,422,417,436])).
% 61.22/61.26 cnf(2250,plain,
% 61.22/61.26 (P10(a129,a258,a2)),
% 61.22/61.26 inference(scs_inference,[],[1373,248,158,4,422])).
% 61.22/61.26 cnf(2354,plain,
% 61.22/61.26 (~P4(x23541,x23541)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2356,plain,
% 61.22/61.26 (~P4(x23561,x23561)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2357,plain,
% 61.22/61.26 (~P8(f250(f3(a87),f250(f3(a4),f3(a1))),f250(f3(a87),f250(f3(a4),f3(a1))))),
% 61.22/61.26 inference(scs_inference,[],[1294,441,2354,2356,64,389,91,297,306,316,269,4,422,436,417,24,23,418])).
% 61.22/61.26 cnf(2450,plain,
% 61.22/61.26 (~P4(x24501,x24501)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2452,plain,
% 61.22/61.26 (~P4(x24521,x24521)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2454,plain,
% 61.22/61.26 (~P4(x24541,x24541)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2459,plain,
% 61.22/61.26 (~P4(a61,a184)),
% 61.22/61.26 inference(scs_inference,[],[1526,441,2450,2452,2454,64,97,305,304,255,352,277,339,4,422,436,417,24,23,418,419,414])).
% 61.22/61.26 cnf(2707,plain,
% 61.22/61.26 (~P4(x27071,x27071)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2709,plain,
% 61.22/61.26 (~P4(x27091,x27091)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(2710,plain,
% 61.22/61.26 (~P8(f250(f3(a98),f250(f3(a4),f3(a1))),f250(f3(a98),f250(f3(a4),f3(a1))))),
% 61.22/61.26 inference(scs_inference,[],[1686,441,2707,2709,64,113,279,307,388,389,251,4,422,436,417,24,23,418])).
% 61.22/61.26 cnf(2827,plain,
% 61.22/61.26 (~E(a87,a43)),
% 61.22/61.26 inference(scs_inference,[],[1794,4])).
% 61.22/61.26 cnf(2991,plain,
% 61.22/61.26 (P6(f3(a43),f3(a1),f3(a65),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[1914,88,178,371,323,4,422,436])).
% 61.22/61.26 cnf(3126,plain,
% 61.22/61.26 (P6(f3(a87),f3(a2),f3(a4),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[2028,99,189,335,310,4,422,436])).
% 61.22/61.26 cnf(3340,plain,
% 61.22/61.26 (~P4(x33401,x33401)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3350,plain,
% 61.22/61.26 (P9(x33501,f120(f3(a54)))+~E(a54,x33501)),
% 61.22/61.26 inference(scs_inference,[],[489,441,3340,55,64,278,117,207,2991,336,354,368,370,422,436,417,24,23,414,13,27,28,10,15,25])).
% 61.22/61.26 cnf(3424,plain,
% 61.22/61.26 (P6(f3(a87),f3(a2),f3(a1),f3(a98))),
% 61.22/61.26 inference(scs_inference,[],[125,215,325,309,422,436])).
% 61.22/61.26 cnf(3429,plain,
% 61.22/61.26 (~P4(x34291,x34291)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3434,plain,
% 61.22/61.26 (P9(x34341,f132(f3(a54)))+~E(a184,x34341)),
% 61.22/61.26 inference(scs_inference,[],[441,3429,64,265,125,215,325,309,422,436,417,24,23,414,25])).
% 61.22/61.26 cnf(3492,plain,
% 61.22/61.26 (~P4(x34921,x34921)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3499,plain,
% 61.22/61.26 (P9(x34991,f120(f250(f3(a4),f250(f3(a1),f3(a1)))))+~E(a20,x34991)),
% 61.22/61.26 inference(scs_inference,[],[441,3492,64,263,131,221,3126,353,321,422,436,417,24,23,414,17,26,25])).
% 61.22/61.26 cnf(3556,plain,
% 61.22/61.26 (P6(f3(a43),f3(a43),f3(a43),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[137,227,371,341,422,436])).
% 61.22/61.26 cnf(3585,plain,
% 61.22/61.26 (~P4(x35851,x35851)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3588,plain,
% 61.22/61.26 (~P4(a87,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,3585,64,58,140,230,344,338,422,436,417,24,23,414])).
% 61.22/61.26 cnf(3590,plain,
% 61.22/61.26 (P9(x35901,f120(f250(f3(a2),f3(a98))))+~E(a110,x35901)),
% 61.22/61.26 inference(scs_inference,[],[441,3585,64,141,58,140,230,344,338,422,436,417,24,23,414,25])).
% 61.22/61.26 cnf(3669,plain,
% 61.22/61.26 (~P4(x36691,x36691)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3675,plain,
% 61.22/61.26 (P9(x36751,f120(f250(f3(a2),f3(a109))))+~E(a122,x36751)),
% 61.22/61.26 inference(scs_inference,[],[441,3669,1907,64,151,147,143,237,331,310,422,436,417,24,23,414,20,25])).
% 61.22/61.26 cnf(3757,plain,
% 61.22/61.26 (~P4(x37571,x37571)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3762,plain,
% 61.22/61.26 (P9(x37621,f120(f250(f3(a76),f3(a109))))+~E(a128,x37621)),
% 61.22/61.26 inference(scs_inference,[],[441,3757,64,157,155,152,245,339,338,422,436,417,24,23,414,25])).
% 61.22/61.26 cnf(3814,plain,
% 61.22/61.26 (P4(a184,a129)),
% 61.22/61.26 inference(scs_inference,[],[64,260,158,288,349,359,422,436,417])).
% 61.22/61.26 cnf(3838,plain,
% 61.22/61.26 (P4(a184,a130)),
% 61.22/61.26 inference(scs_inference,[],[64,259,159,287,332,310,422,436,417])).
% 61.22/61.26 cnf(3841,plain,
% 61.22/61.26 (~P4(x38411,x38411)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3844,plain,
% 61.22/61.26 (P9(x38441,f120(f250(f3(a87),f250(f3(a2),f3(a1)))))+~E(a14,x38441)),
% 61.22/61.26 inference(scs_inference,[],[441,64,258,259,159,287,332,310,422,436,417,24,414,25])).
% 61.22/61.26 cnf(3846,plain,
% 61.22/61.26 (~P4(x38461,x38461)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3847,plain,
% 61.22/61.26 (~E(a14,a2)+~P8(f3(a2),f250(f3(a87),f250(f3(a2),f3(a1))))),
% 61.22/61.26 inference(scs_inference,[],[441,3841,3846,51,64,258,259,159,287,332,310,422,436,417,24,414,25,23,419])).
% 61.22/61.26 cnf(3857,plain,
% 61.22/61.26 (P4(a184,a27)),
% 61.22/61.26 inference(scs_inference,[],[64,258,270,286,341,320,436,422,417])).
% 61.22/61.26 cnf(3881,plain,
% 61.22/61.26 (P4(a184,a26)),
% 61.22/61.26 inference(scs_inference,[],[64,278,269,306,342,311,436,422,417])).
% 61.22/61.26 cnf(3901,plain,
% 61.22/61.26 (P4(a184,a25)),
% 61.22/61.26 inference(scs_inference,[],[441,64,267,268,295,3881,344,329,436,422,23,417])).
% 61.22/61.26 cnf(3916,plain,
% 61.22/61.26 (~P4(x39161,x39161)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3924,plain,
% 61.22/61.26 (P9(x39241,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))+~E(a12,x39241)),
% 61.22/61.26 inference(scs_inference,[],[441,3916,64,256,257,284,3901,3424,322,318,422,436,23,417,24,414,16,25])).
% 61.22/61.26 cnf(3956,plain,
% 61.22/61.26 (P4(a184,a23)),
% 61.22/61.26 inference(scs_inference,[],[64,265,266,293,351,330,422,436,417])).
% 61.22/61.26 cnf(3979,plain,
% 61.22/61.26 (~P4(x39791,x39791)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(3987,plain,
% 61.22/61.26 (P9(x39871,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))+~E(a10,x39871)),
% 61.22/61.26 inference(scs_inference,[],[441,3979,64,254,255,282,3956,3556,398,353,339,422,436,417,23,24,414,11,16,10,25])).
% 61.22/61.26 cnf(4081,plain,
% 61.22/61.26 (P4(a184,a19)),
% 61.22/61.26 inference(scs_inference,[],[64,261,262,289,349,330,422,436,417])).
% 61.22/61.26 cnf(4106,plain,
% 61.22/61.26 (~P4(x41061,x41061)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4113,plain,
% 61.22/61.26 (P9(x41131,f120(f250(f3(a1),f3(a1))))+~E(a6,x41131)),
% 61.22/61.26 inference(scs_inference,[],[441,4106,64,72,251,4081,356,363,351,339,436,417,23,24,414,12,11,25])).
% 61.22/61.26 cnf(4191,plain,
% 61.22/61.26 (P4(a184,a65)),
% 61.22/61.26 inference(scs_inference,[],[64,56,331,328,436,417])).
% 61.22/61.26 cnf(4216,plain,
% 61.22/61.26 (~P4(x42161,x42161)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4219,plain,
% 61.22/61.26 (~P4(a76,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4216,64,57,4191,320,318,436,417,23,24,414])).
% 61.22/61.26 cnf(4317,plain,
% 61.22/61.26 (P4(a184,a41)),
% 61.22/61.26 inference(scs_inference,[],[64,79,417])).
% 61.22/61.26 cnf(4337,plain,
% 61.22/61.26 (P4(a184,a44)),
% 61.22/61.26 inference(scs_inference,[],[64,81,417])).
% 61.22/61.26 cnf(4340,plain,
% 61.22/61.26 (~P4(x43401,x43401)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4341,plain,
% 61.22/61.26 (~E(a44,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4340,64,81,4317,417,23,24])).
% 61.22/61.26 cnf(4343,plain,
% 61.22/61.26 (~P4(a44,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4340,64,81,4317,417,23,24,414])).
% 61.22/61.26 cnf(4357,plain,
% 61.22/61.26 (P4(a184,a46)),
% 61.22/61.26 inference(scs_inference,[],[64,83,417])).
% 61.22/61.26 cnf(4360,plain,
% 61.22/61.26 (~P4(x43601,x43601)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4363,plain,
% 61.22/61.26 (~P4(a46,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4360,64,83,4337,417,23,24,414])).
% 61.22/61.26 cnf(4369,plain,
% 61.22/61.26 (P4(a184,a49)),
% 61.22/61.26 inference(scs_inference,[],[64,86,417])).
% 61.22/61.26 cnf(4372,plain,
% 61.22/61.26 (~P4(x43721,x43721)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4373,plain,
% 61.22/61.26 (~E(a49,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4372,64,86,4357,417,23,24])).
% 61.22/61.26 cnf(4375,plain,
% 61.22/61.26 (~P4(a49,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4372,64,86,4357,417,23,24,414])).
% 61.22/61.26 cnf(4389,plain,
% 61.22/61.26 (P4(a184,a50)),
% 61.22/61.26 inference(scs_inference,[],[64,87,417])).
% 61.22/61.26 cnf(4392,plain,
% 61.22/61.26 (~P4(x43921,x43921)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4393,plain,
% 61.22/61.26 (~E(a50,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4392,64,87,4369,417,23,24])).
% 61.22/61.26 cnf(4395,plain,
% 61.22/61.26 (~P4(a50,a184)),
% 61.22/61.26 inference(scs_inference,[],[441,4392,64,87,4369,417,23,24,414])).
% 61.22/61.26 cnf(4406,plain,
% 61.22/61.26 (P7(f3(a4))),
% 61.22/61.26 inference(scs_inference,[],[4389,34,412,410])).
% 61.22/61.26 cnf(4414,plain,
% 61.22/61.26 (P8(f3(x44141),f250(f3(x44142),f250(f3(x44143),f3(a1))))),
% 61.22/61.26 inference(scs_inference,[],[70,4389,34,1002,49,412,410,426,415,421,416])).
% 61.22/61.26 cnf(4417,plain,
% 61.22/61.26 (~P10(a1,a43,a76)),
% 61.22/61.26 inference(scs_inference,[],[70,512,2827,4389,34,1002,49,412,410,426,415,421,416,2,429])).
% 61.22/61.26 cnf(4427,plain,
% 61.22/61.26 (P8(f250(f3(a87),f250(f3(a4),f3(a1))),f250(f3(a98),f250(f3(a4),f3(a1))))),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,4389,34,2710,497,1880,1002,49,412,410,426,415,421,416,2,429,428,21,22,427,413,424])).
% 61.22/61.26 cnf(4430,plain,
% 61.22/61.26 (P8(f3(a76),f3(a98))),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,4389,34,2710,497,1880,1002,49,48,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420])).
% 61.22/61.26 cnf(4432,plain,
% 61.22/61.26 (P6(f3(a2),f3(a98),f3(a1),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,4389,34,2710,497,1880,1002,389,398,49,48,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420,436])).
% 61.22/61.26 cnf(4434,plain,
% 61.22/61.26 (~P9(a258,f120(x44341))),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,4389,34,2710,497,1880,1002,248,389,398,49,48,441,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420,436,417])).
% 61.22/61.26 cnf(4435,plain,
% 61.22/61.26 (~P4(x44351,x44351)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4438,plain,
% 61.22/61.26 (~P4(x44381,x44381)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4439,plain,
% 61.22/61.26 (P6(f3(a2),f3(a4),f3(a109),f250(f3(a1),f3(a1)))),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,4389,34,2710,497,1880,1002,248,337,389,398,318,49,48,441,4435,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420,436,417,23,437])).
% 61.22/61.26 cnf(4448,plain,
% 61.22/61.26 (~E(a2,a258)),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,2250,4389,34,3588,2710,497,1880,1002,248,337,389,307,398,58,158,318,49,48,441,4435,4438,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420,436,417,23,437,430,419,418,893])).
% 61.22/61.26 cnf(4449,plain,
% 61.22/61.26 (~E(a184,a166)),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,2250,4389,34,3588,2710,497,1880,1002,248,337,389,307,398,58,158,318,49,48,441,4435,4438,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420,436,417,23,437,430,419,418,893,3434])).
% 61.22/61.26 cnf(4454,plain,
% 61.22/61.26 (P10(a109,a228,a1)),
% 61.22/61.26 inference(scs_inference,[],[70,512,659,863,2827,485,2250,4389,34,3588,2710,497,1880,1002,248,2221,337,389,307,398,58,60,52,158,68,318,49,50,48,51,441,4435,4438,412,410,426,415,421,416,2,429,428,21,22,427,413,424,420,436,417,23,437,430,419,418,893,3434,423,431,433])).
% 61.22/61.26 cnf(4460,plain,
% 61.22/61.26 (~E(a14,a2)),
% 61.22/61.26 inference(scs_inference,[],[4414,3847])).
% 61.22/61.26 cnf(4462,plain,
% 61.22/61.26 (~P9(a258,f120(x44621))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4464,plain,
% 61.22/61.26 (~P9(a258,f120(x44641))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4466,plain,
% 61.22/61.26 (~P9(a258,f120(x44661))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4468,plain,
% 61.22/61.26 (~P9(a258,f120(x44681))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4470,plain,
% 61.22/61.26 (~P9(a258,f120(x44701))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4472,plain,
% 61.22/61.26 (~P9(a258,f120(x44721))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4474,plain,
% 61.22/61.26 (~P9(a258,f120(x44741))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4476,plain,
% 61.22/61.26 (~P9(a258,f120(x44761))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4478,plain,
% 61.22/61.26 (~P9(a258,f120(x44781))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4483,plain,
% 61.22/61.26 (P7(f3(a43))),
% 61.22/61.26 inference(scs_inference,[],[4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,35,3857,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410])).
% 61.22/61.26 cnf(4494,plain,
% 61.22/61.26 (~P10(a4,a121,a2)),
% 61.22/61.26 inference(scs_inference,[],[458,487,541,442,476,4448,4406,4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,35,3857,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410,426,415,416,2,428,429])).
% 61.22/61.26 cnf(4496,plain,
% 61.22/61.26 (~P10(a109,a228,a4)),
% 61.22/61.26 inference(scs_inference,[],[458,487,541,442,476,4448,4454,4406,4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,35,3857,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410,426,415,416,2,428,429,427])).
% 61.22/61.26 cnf(4502,plain,
% 61.22/61.26 (P8(f3(a76),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[458,487,541,442,476,4393,4395,4448,4454,4406,4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,35,3857,50,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410,426,415,416,2,428,429,427,413,424,420])).
% 61.22/61.26 cnf(4508,plain,
% 61.22/61.26 (~P9(a258,f120(x45081))),
% 61.22/61.26 inference(rename_variables,[],[4434])).
% 61.22/61.26 cnf(4510,plain,
% 61.22/61.26 (~P9(a259,f120(x45101))),
% 61.22/61.26 inference(scs_inference,[],[458,487,541,442,476,4393,4395,4448,4454,4406,4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,4478,4508,35,3857,249,74,248,53,50,441,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410,426,415,416,2,428,429,427,413,424,420,28,422,25,26,417])).
% 61.22/61.26 cnf(4511,plain,
% 61.22/61.26 (~P4(x45111,x45111)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4520,plain,
% 61.22/61.26 (~E(a2,a259)),
% 61.22/61.26 inference(scs_inference,[],[458,487,541,442,476,4393,4395,4448,4454,4406,4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,4478,4508,35,3857,605,249,402,74,389,66,248,53,57,309,50,441,4511,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410,426,415,416,2,428,429,427,413,424,420,28,422,25,26,417,437,419,418,893])).
% 61.22/61.26 cnf(4525,plain,
% 61.22/61.26 (~P6(f3(a2),f3(a1),f3(a43),f3(a76))),
% 61.22/61.26 inference(scs_inference,[],[458,487,541,1980,442,476,4393,4395,4417,4448,4454,4406,4430,4434,4462,4464,4466,4468,4470,4472,4474,4476,4478,4508,35,3857,605,249,402,74,232,389,142,66,248,52,53,54,57,309,50,441,4511,3350,3590,3675,3762,4113,3499,3844,3924,3987,421,412,410,426,415,416,2,428,429,427,413,424,420,28,422,25,26,417,437,419,418,893,423,430,431])).
% 61.22/61.26 cnf(4529,plain,
% 61.22/61.26 (~P9(a259,f120(x45291))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4533,plain,
% 61.22/61.26 (~P9(a259,f120(x45331))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4535,plain,
% 61.22/61.26 (~P9(a259,f120(x45351))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4537,plain,
% 61.22/61.26 (~P9(a259,f120(x45371))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4539,plain,
% 61.22/61.26 (~P9(a259,f120(x45391))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4541,plain,
% 61.22/61.26 (~P9(a259,f120(x45411))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4545,plain,
% 61.22/61.26 (~P9(a259,f120(x45451))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4546,plain,
% 61.22/61.26 (P7(f3(a54))),
% 61.22/61.26 inference(scs_inference,[],[4502,4510,4529,4533,4535,4537,4539,4541,36,3838,3499,421,4113,3844,3350,3987,3590,412,3924,410])).
% 61.22/61.26 cnf(4549,plain,
% 61.22/61.26 (~P9(a259,f120(x45491))),
% 61.22/61.26 inference(rename_variables,[],[4510])).
% 61.22/61.26 cnf(4559,plain,
% 61.22/61.26 (~P10(a4,a2,a76)),
% 61.22/61.26 inference(scs_inference,[],[70,1175,4460,2017,4483,4502,4510,4529,4533,4535,4537,4539,4541,4545,4549,36,3838,3499,421,4113,3844,3350,3987,3590,412,3924,410,3675,3762,415,426,416,2,428])).
% 61.22/61.26 cnf(4561,plain,
% 61.22/61.26 (~P10(a43,a43,a76)),
% 61.22/61.26 inference(scs_inference,[],[70,580,1175,4460,2017,4483,4502,4510,4529,4533,4535,4537,4539,4541,4545,4549,36,3838,3499,421,4113,3844,3350,3987,3590,412,3924,410,3675,3762,415,426,416,2,428,429])).
% 61.22/61.26 cnf(4567,plain,
% 61.22/61.26 (P8(f250(f3(a76),f3(a43)),f250(f3(a109),f3(a43)))),
% 61.22/61.26 inference(scs_inference,[],[70,580,1175,1555,4460,523,2017,4483,4502,4510,4529,4533,4535,4537,4539,4541,4545,4549,36,3838,535,3499,421,4113,3844,3350,3987,3590,412,3924,410,3675,3762,415,426,416,2,428,429,427,413,424])).
% 61.22/61.26 cnf(4569,plain,
% 61.22/61.26 (P8(f3(a65),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[70,580,1175,1555,4460,523,2017,4483,4502,4510,4529,4533,4535,4537,4539,4541,4545,4549,36,3838,535,47,3499,421,4113,3844,3350,3987,3590,412,3924,410,3675,3762,415,426,416,2,428,429,427,413,424,420])).
% 61.22/61.26 cnf(4575,plain,
% 61.22/61.26 (~P9(a156,f120(x45751))),
% 61.22/61.26 inference(scs_inference,[],[70,580,1175,1555,4460,523,2017,4494,4483,4502,4510,4529,4533,4535,4537,4539,4541,4545,4549,4525,36,3838,535,298,53,321,47,441,3499,421,4113,3844,3350,3987,3590,412,3924,410,3675,3762,415,426,416,2,428,429,427,413,424,420,422,436,417])).
% 61.22/61.26 cnf(4576,plain,
% 61.22/61.26 (~P4(x45761,x45761)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4589,plain,
% 61.22/61.26 (~E(a2,a156)),
% 61.22/61.26 inference(scs_inference,[],[70,580,1175,1555,4460,523,2017,4494,4496,4432,4483,4502,4510,4529,4533,4535,4537,4539,4541,4545,4549,4525,36,4439,3838,4219,535,298,404,72,69,360,60,53,68,57,321,318,47,50,441,4576,3499,421,4113,3844,3350,3987,3590,412,3924,410,3675,3762,415,426,416,2,428,429,427,413,424,420,422,436,417,437,419,418,431,433,893])).
% 61.22/61.26 cnf(4599,plain,
% 61.22/61.26 (~P9(a156,f120(x45991))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4601,plain,
% 61.22/61.26 (~P9(a156,f120(x46011))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4603,plain,
% 61.22/61.26 (~P9(a156,f120(x46031))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4605,plain,
% 61.22/61.26 (~P9(a156,f120(x46051))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4606,plain,
% 61.22/61.26 (P7(f3(a65))),
% 61.22/61.26 inference(scs_inference,[],[4569,4575,4599,4601,4603,37,421,3499,3350,4113,3844,410])).
% 61.22/61.26 cnf(4609,plain,
% 61.22/61.26 (~P9(a156,f120(x46091))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4611,plain,
% 61.22/61.26 (~P9(a156,f120(x46111))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4613,plain,
% 61.22/61.26 (~P9(a156,f120(x46131))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4617,plain,
% 61.22/61.26 (~P9(a156,f120(x46171))),
% 61.22/61.26 inference(rename_variables,[],[4575])).
% 61.22/61.26 cnf(4629,plain,
% 61.22/61.26 (~P10(a2,a43,a2)),
% 61.22/61.26 inference(scs_inference,[],[525,2052,4449,4546,4569,4575,4599,4601,4603,4605,4609,4611,4613,4617,37,3814,513,527,421,3499,3350,4113,3844,410,3987,3924,3762,412,3590,3675,426,415,416,2,428,429])).
% 61.22/61.26 cnf(4637,plain,
% 61.22/61.26 (P8(f3(a54),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[525,2052,4373,4449,4546,4569,4575,4599,4601,4603,4605,4609,4611,4613,4617,37,4375,3814,513,527,46,421,3499,3350,4113,3844,410,3987,3924,3762,412,3590,3675,426,415,416,2,428,429,427,413,424,420])).
% 61.22/61.26 cnf(4643,plain,
% 61.22/61.26 (~P9(a155,f120(x46431))),
% 61.22/61.26 inference(scs_inference,[],[525,2052,4373,4449,4546,4569,4575,4599,4601,4603,4605,4609,4611,4613,4617,37,4375,3814,513,297,527,316,388,54,46,441,421,3499,3350,4113,3844,410,3987,3924,3762,412,3590,3675,426,415,416,2,428,429,427,413,424,420,422,436,417])).
% 61.22/61.26 cnf(4644,plain,
% 61.22/61.26 (~P4(x46441,x46441)),
% 61.22/61.26 inference(rename_variables,[],[441])).
% 61.22/61.26 cnf(4656,plain,
% 61.22/61.26 (~E(a184,a155)),
% 61.22/61.26 inference(scs_inference,[],[525,2052,4373,4449,4559,4546,4569,4575,4599,4601,4603,4605,4609,4611,4613,4617,37,4567,4414,4375,3814,2459,513,1108,297,406,97,527,316,326,388,54,53,309,46,51,441,4644,421,3499,3350,4113,3844,410,3987,3924,3762,412,3590,3675,426,415,416,2,428,429,427,413,424,420,422,436,417,437,419,418,431,3434])).
% 61.22/61.26 cnf(4669,plain,
% 61.22/61.26 (~P9(a155,f120(x46691))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4670,plain,
% 61.22/61.26 (P7(f3(a76))),
% 61.22/61.26 inference(scs_inference,[],[4637,4643,38,421,3499,410])).
% 61.22/61.26 cnf(4673,plain,
% 61.22/61.26 (~P9(a155,f120(x46731))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4675,plain,
% 61.22/61.26 (~P9(a155,f120(x46751))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4677,plain,
% 61.22/61.26 (~P9(a155,f120(x46771))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4681,plain,
% 61.22/61.26 (~P9(a155,f120(x46811))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4683,plain,
% 61.22/61.26 (~P9(a155,f120(x46831))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4685,plain,
% 61.22/61.26 (~P9(a155,f120(x46851))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4691,plain,
% 61.22/61.26 (~P9(a155,f120(x46911))),
% 61.22/61.26 inference(rename_variables,[],[4643])).
% 61.22/61.26 cnf(4705,plain,
% 61.22/61.26 (P8(f3(a43),f3(a109))),
% 61.22/61.26 inference(scs_inference,[],[70,553,1144,1360,1594,2087,4520,4606,4637,4643,4669,4673,4675,4677,4681,4683,4685,4691,38,482,566,45,421,3499,410,3844,3350,4113,412,3762,3675,3987,415,426,3590,416,3924,2,428,429,427,413,420])).
% 61.22/61.26 cnf(4711,plain,
% 61.22/61.26 (~P9(a154,f120(x47111))),
% 61.36/61.26 inference(scs_inference,[],[70,553,1144,1360,1594,2087,4520,4629,4606,4637,4643,4669,4673,4675,4677,4681,4683,4685,4691,38,482,566,296,45,51,441,421,3499,410,3844,3350,4113,412,3762,3675,3987,415,426,3590,416,3924,2,428,429,427,413,420,424,422,417])).
% 61.36/61.26 cnf(4712,plain,
% 61.36/61.26 (~P4(x47121,x47121)),
% 61.36/61.26 inference(rename_variables,[],[441])).
% 61.36/61.26 cnf(4723,plain,
% 61.36/61.26 (~P6(f3(a2),f3(a43),f3(a43),f3(a76))),
% 61.36/61.26 inference(scs_inference,[],[70,553,1144,1360,1594,2087,4520,4561,4629,4606,4637,4643,4669,4673,4675,4677,4681,4683,4685,4691,38,4363,482,566,4432,296,407,398,61,69,54,68,55,57,309,45,51,64,441,4712,421,3499,410,3844,3350,4113,412,3762,3675,3987,415,426,3590,416,3924,2,428,429,427,413,420,424,422,417,437,419,418,432,431])).
% 61.36/61.26 cnf(4736,plain,
% 61.36/61.26 (P7(f3(a87))),
% 61.36/61.26 inference(scs_inference,[],[4705,39,421,410])).
% 61.36/61.26 cnf(4739,plain,
% 61.36/61.26 (~P9(a154,f120(x47391))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4741,plain,
% 61.36/61.26 (~P9(a154,f120(x47411))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4745,plain,
% 61.36/61.26 (~P9(a154,f120(x47451))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4747,plain,
% 61.36/61.26 (~P9(a154,f120(x47471))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4755,plain,
% 61.36/61.26 (~P9(a154,f120(x47551))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4757,plain,
% 61.36/61.26 (~P9(a154,f120(x47571))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4759,plain,
% 61.36/61.26 (~P9(a154,f120(x47591))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4761,plain,
% 61.36/61.26 (~P9(a154,f120(x47611))),
% 61.36/61.26 inference(rename_variables,[],[4711])).
% 61.36/61.26 cnf(4768,plain,
% 61.36/61.26 (~P10(a2,a65,a2)),
% 61.36/61.26 inference(scs_inference,[],[555,2122,4589,4670,4705,4711,4739,4741,4745,4747,4755,4757,4759,4761,39,4427,1982,2357,546,558,421,410,3499,3350,412,4113,3844,416,415,426,3590,3762,3924,3675,3987,2,428,22,429])).
% 61.36/61.26 cnf(4774,plain,
% 61.36/61.26 (P8(f3(a87),f3(a109))),
% 61.36/61.26 inference(scs_inference,[],[555,2122,4341,4589,4670,4705,4711,4739,4741,4745,4747,4755,4757,4759,4761,39,4427,4343,1982,2357,546,558,49,50,421,410,3499,3350,412,4113,3844,416,415,426,3590,3762,3924,3675,3987,2,428,22,429,427,413,420])).
% 61.36/61.26 cnf(4782,plain,
% 61.36/61.26 (~P9(a142,f120(x47821))),
% 61.36/61.26 inference(scs_inference,[],[555,2122,4341,4589,4670,4705,4711,4739,4741,4745,4747,4755,4757,4759,4761,39,4427,4343,1982,2357,546,285,558,378,315,56,49,50,441,421,410,3499,3350,412,4113,3844,416,415,426,3590,3762,3924,3675,3987,2,428,22,429,427,413,420,424,422,436,417])).
% 61.36/61.26 cnf(4804,plain,
% 61.36/61.26 (~P9(a142,f120(x48041))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4808,plain,
% 61.36/61.26 (~P9(a142,f120(x48081))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4816,plain,
% 61.36/61.26 (~P9(a142,f120(x48161))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4818,plain,
% 61.36/61.26 (~P9(a142,f120(x48181))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4820,plain,
% 61.36/61.26 (~P9(a142,f120(x48201))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4822,plain,
% 61.36/61.26 (~P9(a142,f120(x48221))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4824,plain,
% 61.36/61.26 (~P9(a142,f120(x48241))),
% 61.36/61.26 inference(rename_variables,[],[4782])).
% 61.36/61.26 cnf(4842,plain,
% 61.36/61.26 ($false),
% 61.36/61.26 inference(scs_inference,[],[70,591,1476,1900,2016,2154,4656,4768,4723,4736,4774,4782,4804,4808,4816,4818,4820,4822,4824,40,2019,605,4705,368,341,44,51,421,410,3499,412,3350,416,415,426,3844,3675,3924,3987,3590,3762,2,428,429,427,413,424,420,422,436]),
% 61.36/61.26 ['proof']).
% 61.36/61.26 % SZS output end Proof
% 61.36/61.26 % Total time :60.550000s
%------------------------------------------------------------------------------