%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM294+1 : TPTP v8.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:45 EDT 2024
% Result : Theorem 70.37s 70.50s
% Output : CNFRefutation 70.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM294+1 : TPTP v8.2.0. Released v3.1.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n017.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 : Sun Jun 23 03:50:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 70.37/70.49 %-------------------------------------------
% 70.37/70.49 % File :CSE---1.7
% 70.37/70.49 % Problem :theBenchmark
% 70.37/70.49 % Transform :cnf
% 70.37/70.49 % Format :tptp:raw
% 70.37/70.49 % Command :java -jar mcs_scs.jar %d %s
% 70.37/70.49
% 70.37/70.49 % Result :Theorem 69.800000s
% 70.37/70.49 % Output :CNFRefutation 69.800000s
% 70.37/70.49 %-------------------------------------------
% 70.37/70.50 %------------------------------------------------------------------------------
% 70.37/70.50 % File : NUM294+1 : TPTP v8.2.0. Released v3.1.0.
% 70.37/70.50 % Domain : Number Theory (RDN arithmetic)
% 70.37/70.50 % Problem : 12 < ?
% 70.37/70.50 % Version : Especial.
% 70.37/70.50 % English :
% 70.37/70.50
% 70.37/70.50 % Refs :
% 70.37/70.50 % Source : [TPTP]
% 70.37/70.50 % Names :
% 70.37/70.50
% 70.37/70.50 % Status : Theorem
% 70.37/70.50 % Rating : 0.39 v8.1.0, 0.42 v7.5.0, 0.44 v7.4.0, 0.37 v7.3.0, 0.48 v7.2.0, 0.45 v7.1.0, 0.35 v7.0.0, 0.37 v6.4.0, 0.35 v6.3.0, 0.46 v6.2.0, 0.48 v6.1.0, 0.53 v6.0.0, 0.61 v5.5.0, 0.59 v5.4.0, 0.68 v5.3.0, 0.74 v5.2.0, 0.50 v5.1.0, 0.48 v5.0.0, 0.58 v4.1.0, 0.57 v4.0.1, 0.52 v4.0.0, 0.50 v3.7.0, 0.45 v3.5.0, 0.53 v3.3.0, 0.50 v3.2.0, 0.55 v3.1.0
% 70.37/70.50 % Syntax : Number of formulae : 402 ( 375 unt; 0 def)
% 70.37/70.50 % Number of atoms : 473 ( 5 equ)
% 70.37/70.50 % Maximal formula atoms : 8 ( 1 avg)
% 70.37/70.50 % Number of connectives : 73 ( 2 ~; 1 |; 43 &)
% 70.37/70.50 % ( 3 <=>; 24 =>; 0 <=; 0 <~>)
% 70.37/70.50 % Maximal formula depth : 19 ( 1 avg)
% 70.37/70.50 % Maximal term depth : 5 ( 2 avg)
% 70.37/70.50 % Number of predicates : 11 ( 10 usr; 0 prp; 1-4 aty)
% 70.37/70.50 % Number of functors : 260 ( 260 usr; 256 con; 0-2 aty)
% 70.37/70.50 % Number of variables : 122 ( 121 !; 1 ?)
% 70.37/70.50 % SPC : FOF_THM_RFO_SEQ
% 70.37/70.50
% 70.37/70.50 % Comments :
% 70.37/70.50 %------------------------------------------------------------------------------
% 70.37/70.50 %----Include axioms for RDN arithmetic
% 70.37/70.50 include('Axioms/NUM005+0.ax').
% 70.37/70.50 include('Axioms/NUM005+1.ax').
% 70.37/70.50 include('Axioms/NUM005+2.ax').
% 70.37/70.50 %------------------------------------------------------------------------------
% 70.37/70.50 fof(n12_less_something,conjecture,
% 70.37/70.50 ? [X] : less(n12,X) ).
% 70.37/70.50
% 70.37/70.50 %------------------------------------------------------------------------------
% 70.37/70.50 %-------------------------------------------
% 70.37/70.50 % Proof found
% 70.37/70.50 % SZS status Theorem for theBenchmark
% 70.37/70.50 % SZS output start Proof
% 70.37/70.50 %ClaNum:439(EqnAxiom:32)
% 70.37/70.50 %VarNum:272(SingletonVarNum:133)
% 70.37/70.50 %MaxLitNum:8
% 70.37/70.50 %MaxfuncDepth:4
% 70.37/70.50 %SharedTerms:966
% 70.37/70.50 %goalClause: 407
% 70.37/70.50 %singleGoalClaCount:1
% 70.37/70.50 [33]P1(f3(a1))
% 70.37/70.50 [34]P1(f3(a4))
% 70.37/70.50 [35]P1(f3(a43))
% 70.37/70.50 [36]P1(f3(a54))
% 70.37/70.50 [37]P1(f3(a65))
% 70.37/70.50 [38]P1(f3(a76))
% 70.37/70.50 [39]P1(f3(a87))
% 70.37/70.50 [40]P1(f3(a98))
% 70.37/70.50 [41]P1(f3(a109))
% 70.37/70.50 [42]P8(f3(a2),f3(a1))
% 70.37/70.50 [43]P8(f3(a1),f3(a4))
% 70.37/70.50 [44]P8(f3(a4),f3(a43))
% 70.37/70.50 [45]P8(f3(a43),f3(a54))
% 70.37/70.50 [46]P8(f3(a54),f3(a65))
% 70.37/70.50 [47]P8(f3(a65),f3(a76))
% 70.37/70.50 [48]P8(f3(a76),f3(a87))
% 70.37/70.50 [49]P8(f3(a87),f3(a98))
% 70.37/70.50 [50]P8(f3(a98),f3(a109))
% 70.37/70.50 [307]P2(f3(a2),f3(a2),f3(a2),f3(a2))
% 70.37/70.50 [308]P2(f3(a2),f3(a1),f3(a1),f3(a2))
% 70.37/70.50 [309]P2(f3(a2),f3(a4),f3(a4),f3(a2))
% 70.37/70.50 [310]P2(f3(a2),f3(a43),f3(a43),f3(a2))
% 70.37/70.50 [311]P2(f3(a2),f3(a54),f3(a54),f3(a2))
% 70.37/70.50 [312]P2(f3(a2),f3(a65),f3(a65),f3(a2))
% 70.37/70.50 [313]P2(f3(a2),f3(a76),f3(a76),f3(a2))
% 70.37/70.50 [314]P2(f3(a2),f3(a87),f3(a87),f3(a2))
% 70.37/70.50 [315]P2(f3(a2),f3(a98),f3(a98),f3(a2))
% 70.37/70.50 [316]P2(f3(a2),f3(a109),f3(a109),f3(a2))
% 70.37/70.50 [317]P2(f3(a1),f3(a2),f3(a1),f3(a2))
% 70.37/70.50 [318]P2(f3(a1),f3(a1),f3(a4),f3(a2))
% 70.37/70.50 [319]P2(f3(a1),f3(a4),f3(a43),f3(a2))
% 70.37/70.50 [320]P2(f3(a1),f3(a43),f3(a54),f3(a2))
% 70.37/70.50 [321]P2(f3(a1),f3(a54),f3(a65),f3(a2))
% 70.37/70.50 [322]P2(f3(a1),f3(a65),f3(a76),f3(a2))
% 70.37/70.50 [323]P2(f3(a1),f3(a76),f3(a87),f3(a2))
% 70.37/70.50 [324]P2(f3(a1),f3(a87),f3(a98),f3(a2))
% 70.37/70.50 [325]P2(f3(a1),f3(a98),f3(a109),f3(a2))
% 70.37/70.50 [326]P2(f3(a1),f3(a109),f3(a2),f3(a1))
% 70.37/70.50 [327]P2(f3(a4),f3(a2),f3(a4),f3(a2))
% 70.37/70.50 [328]P2(f3(a4),f3(a1),f3(a43),f3(a2))
% 70.37/70.50 [329]P2(f3(a4),f3(a4),f3(a54),f3(a2))
% 70.37/70.50 [330]P2(f3(a4),f3(a43),f3(a65),f3(a2))
% 70.37/70.50 [331]P2(f3(a4),f3(a54),f3(a76),f3(a2))
% 70.37/70.50 [332]P2(f3(a4),f3(a65),f3(a87),f3(a2))
% 70.37/70.50 [333]P2(f3(a4),f3(a76),f3(a98),f3(a2))
% 70.37/70.50 [334]P2(f3(a4),f3(a87),f3(a109),f3(a2))
% 70.37/70.50 [335]P2(f3(a4),f3(a98),f3(a2),f3(a1))
% 70.37/70.51 [336]P2(f3(a4),f3(a109),f3(a1),f3(a1))
% 70.37/70.51 [337]P2(f3(a43),f3(a2),f3(a43),f3(a2))
% 70.37/70.51 [338]P2(f3(a43),f3(a1),f3(a54),f3(a2))
% 70.37/70.51 [339]P2(f3(a43),f3(a4),f3(a65),f3(a2))
% 70.37/70.51 [340]P2(f3(a43),f3(a43),f3(a76),f3(a2))
% 70.37/70.51 [341]P2(f3(a43),f3(a54),f3(a87),f3(a2))
% 70.37/70.51 [342]P2(f3(a43),f3(a65),f3(a98),f3(a2))
% 70.37/70.51 [343]P2(f3(a43),f3(a76),f3(a109),f3(a2))
% 70.37/70.51 [344]P2(f3(a43),f3(a87),f3(a2),f3(a1))
% 70.37/70.51 [345]P2(f3(a43),f3(a98),f3(a1),f3(a1))
% 70.37/70.51 [346]P2(f3(a43),f3(a109),f3(a4),f3(a1))
% 70.37/70.51 [347]P2(f3(a54),f3(a2),f3(a54),f3(a2))
% 70.37/70.51 [348]P2(f3(a54),f3(a1),f3(a65),f3(a2))
% 70.37/70.51 [349]P2(f3(a54),f3(a4),f3(a76),f3(a2))
% 70.37/70.51 [350]P2(f3(a54),f3(a43),f3(a87),f3(a2))
% 70.37/70.51 [351]P2(f3(a54),f3(a54),f3(a98),f3(a2))
% 70.37/70.51 [352]P2(f3(a54),f3(a65),f3(a109),f3(a2))
% 70.37/70.51 [353]P2(f3(a54),f3(a76),f3(a2),f3(a1))
% 70.37/70.51 [354]P2(f3(a54),f3(a87),f3(a1),f3(a1))
% 70.37/70.51 [355]P2(f3(a54),f3(a98),f3(a4),f3(a1))
% 70.37/70.51 [356]P2(f3(a54),f3(a109),f3(a43),f3(a1))
% 70.37/70.51 [357]P2(f3(a65),f3(a2),f3(a65),f3(a2))
% 70.37/70.51 [358]P2(f3(a65),f3(a1),f3(a76),f3(a2))
% 70.37/70.51 [359]P2(f3(a65),f3(a4),f3(a87),f3(a2))
% 70.37/70.51 [360]P2(f3(a65),f3(a43),f3(a98),f3(a2))
% 70.37/70.51 [361]P2(f3(a65),f3(a54),f3(a109),f3(a2))
% 70.37/70.51 [362]P2(f3(a65),f3(a65),f3(a2),f3(a1))
% 70.37/70.51 [363]P2(f3(a65),f3(a76),f3(a1),f3(a1))
% 70.37/70.51 [364]P2(f3(a65),f3(a87),f3(a4),f3(a1))
% 70.37/70.51 [365]P2(f3(a65),f3(a98),f3(a43),f3(a1))
% 70.37/70.51 [366]P2(f3(a65),f3(a109),f3(a54),f3(a1))
% 70.37/70.51 [367]P2(f3(a76),f3(a2),f3(a76),f3(a2))
% 70.37/70.51 [368]P2(f3(a76),f3(a1),f3(a87),f3(a2))
% 70.37/70.51 [369]P2(f3(a76),f3(a4),f3(a98),f3(a2))
% 70.37/70.51 [370]P2(f3(a76),f3(a43),f3(a109),f3(a2))
% 70.37/70.51 [371]P2(f3(a76),f3(a54),f3(a2),f3(a1))
% 70.37/70.51 [372]P2(f3(a76),f3(a65),f3(a1),f3(a1))
% 70.37/70.51 [373]P2(f3(a76),f3(a76),f3(a4),f3(a1))
% 70.37/70.51 [374]P2(f3(a76),f3(a87),f3(a43),f3(a1))
% 70.37/70.51 [375]P2(f3(a76),f3(a98),f3(a54),f3(a1))
% 70.37/70.51 [376]P2(f3(a76),f3(a109),f3(a65),f3(a1))
% 70.37/70.51 [377]P2(f3(a87),f3(a2),f3(a87),f3(a2))
% 70.37/70.51 [378]P2(f3(a87),f3(a1),f3(a98),f3(a2))
% 70.37/70.51 [379]P2(f3(a87),f3(a4),f3(a109),f3(a2))
% 70.37/70.51 [380]P2(f3(a87),f3(a43),f3(a2),f3(a1))
% 70.37/70.51 [381]P2(f3(a87),f3(a54),f3(a1),f3(a1))
% 70.37/70.51 [382]P2(f3(a87),f3(a65),f3(a4),f3(a1))
% 70.37/70.51 [383]P2(f3(a87),f3(a76),f3(a43),f3(a1))
% 70.37/70.51 [384]P2(f3(a87),f3(a87),f3(a54),f3(a1))
% 70.37/70.51 [385]P2(f3(a87),f3(a98),f3(a65),f3(a1))
% 70.37/70.51 [386]P2(f3(a87),f3(a109),f3(a76),f3(a1))
% 70.37/70.51 [387]P2(f3(a98),f3(a2),f3(a98),f3(a2))
% 70.37/70.51 [388]P2(f3(a98),f3(a1),f3(a109),f3(a2))
% 70.37/70.51 [389]P2(f3(a98),f3(a4),f3(a2),f3(a1))
% 70.37/70.51 [390]P2(f3(a98),f3(a43),f3(a1),f3(a1))
% 70.37/70.51 [391]P2(f3(a98),f3(a54),f3(a4),f3(a1))
% 70.37/70.51 [392]P2(f3(a98),f3(a65),f3(a43),f3(a1))
% 70.37/70.51 [393]P2(f3(a98),f3(a76),f3(a54),f3(a1))
% 70.37/70.51 [394]P2(f3(a98),f3(a87),f3(a65),f3(a1))
% 70.37/70.51 [395]P2(f3(a98),f3(a98),f3(a76),f3(a1))
% 70.37/70.51 [396]P2(f3(a98),f3(a109),f3(a87),f3(a1))
% 70.37/70.51 [397]P2(f3(a109),f3(a2),f3(a109),f3(a2))
% 70.37/70.51 [398]P2(f3(a109),f3(a1),f3(a2),f3(a1))
% 70.37/70.51 [399]P2(f3(a109),f3(a4),f3(a1),f3(a1))
% 70.37/70.51 [400]P2(f3(a109),f3(a43),f3(a4),f3(a1))
% 70.37/70.51 [401]P2(f3(a109),f3(a54),f3(a43),f3(a1))
% 70.37/70.51 [402]P2(f3(a109),f3(a65),f3(a54),f3(a1))
% 70.37/70.51 [403]P2(f3(a109),f3(a76),f3(a65),f3(a1))
% 70.37/70.51 [404]P2(f3(a109),f3(a87),f3(a76),f3(a1))
% 70.37/70.51 [405]P2(f3(a109),f3(a98),f3(a87),f3(a1))
% 70.37/70.51 [406]P2(f3(a109),f3(a109),f3(a98),f3(a1))
% 70.37/70.51 [51]P9(a2,f120(f3(a2)))
% 70.37/70.51 [52]P9(a1,f120(f3(a1)))
% 70.37/70.51 [53]P9(a4,f120(f3(a4)))
% 70.37/70.51 [54]P9(a43,f120(f3(a43)))
% 70.37/70.51 [55]P9(a54,f120(f3(a54)))
% 70.37/70.51 [56]P9(a65,f120(f3(a65)))
% 70.37/70.51 [57]P9(a76,f120(f3(a76)))
% 70.37/70.51 [58]P9(a87,f120(f3(a87)))
% 70.37/70.51 [59]P9(a98,f120(f3(a98)))
% 70.37/70.51 [60]P9(a109,f120(f3(a109)))
% 70.37/70.51 [61]P9(a121,f132(f3(a1)))
% 70.37/70.51 [62]P9(a133,f132(f3(a4)))
% 70.37/70.51 [63]P9(a173,f132(f3(a43)))
% 70.37/70.51 [64]P9(a184,f132(f3(a54)))
% 70.37/70.51 [65]P9(a195,f132(f3(a65)))
% 70.37/70.51 [66]P9(a206,f132(f3(a76)))
% 70.37/70.51 [67]P9(a217,f132(f3(a87)))
% 70.37/70.51 [68]P9(a228,f132(f3(a98)))
% 70.37/70.51 [69]P9(a239,f132(f3(a109)))
% 70.37/70.51 [70]P9(a5,f120(f250(f3(a2),f3(a1))))
% 70.37/70.51 [71]P9(a6,f120(f250(f3(a1),f3(a1))))
% 70.37/70.51 [72]P9(a17,f120(f250(f3(a4),f3(a1))))
% 70.37/70.51 [73]P9(a28,f120(f250(f3(a43),f3(a1))))
% 70.37/70.51 [74]P9(a37,f120(f250(f3(a54),f3(a1))))
% 70.37/70.51 [75]P9(a38,f120(f250(f3(a65),f3(a1))))
% 70.37/70.51 [76]P9(a39,f120(f250(f3(a76),f3(a1))))
% 70.37/70.51 [77]P9(a40,f120(f250(f3(a87),f3(a1))))
% 70.37/70.51 [78]P9(a41,f120(f250(f3(a98),f3(a1))))
% 70.37/70.51 [79]P9(a42,f120(f250(f3(a109),f3(a1))))
% 70.37/70.51 [80]P9(a44,f120(f250(f3(a2),f3(a4))))
% 70.37/70.51 [81]P9(a45,f120(f250(f3(a1),f3(a4))))
% 70.37/70.51 [82]P9(a46,f120(f250(f3(a4),f3(a4))))
% 70.37/70.51 [83]P9(a47,f120(f250(f3(a43),f3(a4))))
% 70.37/70.51 [84]P9(a48,f120(f250(f3(a54),f3(a4))))
% 70.37/70.51 [85]P9(a49,f120(f250(f3(a65),f3(a4))))
% 70.37/70.51 [86]P9(a50,f120(f250(f3(a76),f3(a4))))
% 70.37/70.51 [87]P9(a51,f120(f250(f3(a87),f3(a4))))
% 70.37/70.51 [88]P9(a52,f120(f250(f3(a98),f3(a4))))
% 70.37/70.51 [89]P9(a53,f120(f250(f3(a109),f3(a4))))
% 70.37/70.51 [90]P9(a55,f120(f250(f3(a2),f3(a43))))
% 70.37/70.51 [91]P9(a56,f120(f250(f3(a1),f3(a43))))
% 70.37/70.51 [92]P9(a57,f120(f250(f3(a4),f3(a43))))
% 70.37/70.51 [93]P9(a58,f120(f250(f3(a43),f3(a43))))
% 70.37/70.51 [94]P9(a59,f120(f250(f3(a54),f3(a43))))
% 70.37/70.51 [95]P9(a60,f120(f250(f3(a65),f3(a43))))
% 70.37/70.51 [96]P9(a61,f120(f250(f3(a76),f3(a43))))
% 70.37/70.51 [97]P9(a62,f120(f250(f3(a87),f3(a43))))
% 70.37/70.51 [98]P9(a63,f120(f250(f3(a98),f3(a43))))
% 70.37/70.51 [99]P9(a64,f120(f250(f3(a109),f3(a43))))
% 70.37/70.51 [100]P9(a66,f120(f250(f3(a2),f3(a54))))
% 70.37/70.51 [101]P9(a67,f120(f250(f3(a1),f3(a54))))
% 70.37/70.51 [102]P9(a68,f120(f250(f3(a4),f3(a54))))
% 70.37/70.51 [103]P9(a69,f120(f250(f3(a43),f3(a54))))
% 70.37/70.51 [104]P9(a70,f120(f250(f3(a54),f3(a54))))
% 70.37/70.51 [105]P9(a71,f120(f250(f3(a65),f3(a54))))
% 70.37/70.51 [106]P9(a72,f120(f250(f3(a76),f3(a54))))
% 70.37/70.51 [107]P9(a73,f120(f250(f3(a87),f3(a54))))
% 70.37/70.51 [108]P9(a74,f120(f250(f3(a98),f3(a54))))
% 70.37/70.51 [109]P9(a75,f120(f250(f3(a109),f3(a54))))
% 70.37/70.51 [110]P9(a77,f120(f250(f3(a2),f3(a65))))
% 70.37/70.51 [111]P9(a78,f120(f250(f3(a1),f3(a65))))
% 70.37/70.51 [112]P9(a79,f120(f250(f3(a4),f3(a65))))
% 70.37/70.51 [113]P9(a80,f120(f250(f3(a43),f3(a65))))
% 70.37/70.51 [114]P9(a81,f120(f250(f3(a54),f3(a65))))
% 70.37/70.51 [115]P9(a82,f120(f250(f3(a65),f3(a65))))
% 70.37/70.51 [116]P9(a83,f120(f250(f3(a76),f3(a65))))
% 70.37/70.51 [117]P9(a84,f120(f250(f3(a87),f3(a65))))
% 70.37/70.51 [118]P9(a85,f120(f250(f3(a98),f3(a65))))
% 70.37/70.51 [119]P9(a86,f120(f250(f3(a109),f3(a65))))
% 70.37/70.51 [120]P9(a88,f120(f250(f3(a2),f3(a76))))
% 70.37/70.51 [121]P9(a89,f120(f250(f3(a1),f3(a76))))
% 70.37/70.51 [122]P9(a90,f120(f250(f3(a4),f3(a76))))
% 70.37/70.51 [123]P9(a91,f120(f250(f3(a43),f3(a76))))
% 70.37/70.51 [124]P9(a92,f120(f250(f3(a54),f3(a76))))
% 70.37/70.51 [125]P9(a93,f120(f250(f3(a65),f3(a76))))
% 70.37/70.51 [126]P9(a94,f120(f250(f3(a76),f3(a76))))
% 70.37/70.51 [127]P9(a95,f120(f250(f3(a87),f3(a76))))
% 70.37/70.51 [128]P9(a96,f120(f250(f3(a98),f3(a76))))
% 70.37/70.51 [129]P9(a97,f120(f250(f3(a109),f3(a76))))
% 70.37/70.51 [130]P9(a99,f120(f250(f3(a2),f3(a87))))
% 70.37/70.51 [131]P9(a100,f120(f250(f3(a1),f3(a87))))
% 70.37/70.51 [132]P9(a101,f120(f250(f3(a4),f3(a87))))
% 70.37/70.51 [133]P9(a102,f120(f250(f3(a43),f3(a87))))
% 70.37/70.51 [134]P9(a103,f120(f250(f3(a54),f3(a87))))
% 70.37/70.51 [135]P9(a104,f120(f250(f3(a65),f3(a87))))
% 70.37/70.51 [136]P9(a105,f120(f250(f3(a76),f3(a87))))
% 70.37/70.51 [137]P9(a106,f120(f250(f3(a87),f3(a87))))
% 70.37/70.51 [138]P9(a107,f120(f250(f3(a98),f3(a87))))
% 70.37/70.51 [139]P9(a108,f120(f250(f3(a109),f3(a87))))
% 70.37/70.51 [140]P9(a110,f120(f250(f3(a2),f3(a98))))
% 70.37/70.51 [141]P9(a111,f120(f250(f3(a1),f3(a98))))
% 70.37/70.51 [142]P9(a112,f120(f250(f3(a4),f3(a98))))
% 70.37/70.51 [143]P9(a113,f120(f250(f3(a43),f3(a98))))
% 70.37/70.51 [144]P9(a114,f120(f250(f3(a54),f3(a98))))
% 70.37/70.51 [145]P9(a115,f120(f250(f3(a65),f3(a98))))
% 70.37/70.51 [146]P9(a116,f120(f250(f3(a76),f3(a98))))
% 70.37/70.51 [147]P9(a117,f120(f250(f3(a87),f3(a98))))
% 70.37/70.51 [148]P9(a118,f120(f250(f3(a98),f3(a98))))
% 70.37/70.51 [149]P9(a119,f120(f250(f3(a109),f3(a98))))
% 70.37/70.51 [150]P9(a122,f120(f250(f3(a2),f3(a109))))
% 70.37/70.51 [151]P9(a123,f120(f250(f3(a1),f3(a109))))
% 70.37/70.51 [152]P9(a124,f120(f250(f3(a4),f3(a109))))
% 70.37/70.51 [153]P9(a125,f120(f250(f3(a43),f3(a109))))
% 70.37/70.51 [154]P9(a126,f120(f250(f3(a54),f3(a109))))
% 70.37/70.51 [155]P9(a127,f120(f250(f3(a65),f3(a109))))
% 70.37/70.51 [156]P9(a128,f120(f250(f3(a76),f3(a109))))
% 70.37/70.51 [157]P9(a129,f120(f250(f3(a87),f3(a109))))
% 70.37/70.51 [158]P9(a130,f120(f250(f3(a98),f3(a109))))
% 70.37/70.51 [159]P9(a131,f120(f250(f3(a109),f3(a109))))
% 70.37/70.51 [160]P9(a134,f132(f250(f3(a2),f3(a1))))
% 70.37/70.51 [161]P9(a135,f132(f250(f3(a1),f3(a1))))
% 70.37/70.51 [162]P9(a146,f132(f250(f3(a4),f3(a1))))
% 70.37/70.51 [163]P9(a157,f132(f250(f3(a43),f3(a1))))
% 70.37/70.51 [164]P9(a167,f132(f250(f3(a54),f3(a1))))
% 70.37/70.51 [165]P9(a168,f132(f250(f3(a65),f3(a1))))
% 70.37/70.51 [166]P9(a169,f132(f250(f3(a76),f3(a1))))
% 70.37/70.51 [167]P9(a170,f132(f250(f3(a87),f3(a1))))
% 70.37/70.51 [168]P9(a171,f132(f250(f3(a98),f3(a1))))
% 70.37/70.51 [169]P9(a172,f132(f250(f3(a109),f3(a1))))
% 70.37/70.51 [170]P9(a174,f132(f250(f3(a2),f3(a4))))
% 70.37/70.51 [171]P9(a175,f132(f250(f3(a1),f3(a4))))
% 70.37/70.51 [172]P9(a176,f132(f250(f3(a4),f3(a4))))
% 70.37/70.51 [173]P9(a177,f132(f250(f3(a43),f3(a4))))
% 70.37/70.51 [174]P9(a178,f132(f250(f3(a54),f3(a4))))
% 70.37/70.51 [175]P9(a179,f132(f250(f3(a65),f3(a4))))
% 70.37/70.51 [176]P9(a180,f132(f250(f3(a76),f3(a4))))
% 70.37/70.51 [177]P9(a181,f132(f250(f3(a87),f3(a4))))
% 70.37/70.51 [178]P9(a182,f132(f250(f3(a98),f3(a4))))
% 70.37/70.51 [179]P9(a183,f132(f250(f3(a109),f3(a4))))
% 70.37/70.51 [180]P9(a185,f132(f250(f3(a2),f3(a43))))
% 70.37/70.51 [181]P9(a186,f132(f250(f3(a1),f3(a43))))
% 70.37/70.51 [182]P9(a187,f132(f250(f3(a4),f3(a43))))
% 70.37/70.51 [183]P9(a188,f132(f250(f3(a43),f3(a43))))
% 70.37/70.51 [184]P9(a189,f132(f250(f3(a54),f3(a43))))
% 70.37/70.51 [185]P9(a190,f132(f250(f3(a65),f3(a43))))
% 70.37/70.51 [186]P9(a191,f132(f250(f3(a76),f3(a43))))
% 70.37/70.51 [187]P9(a192,f132(f250(f3(a87),f3(a43))))
% 70.37/70.51 [188]P9(a193,f132(f250(f3(a98),f3(a43))))
% 70.37/70.51 [189]P9(a194,f132(f250(f3(a109),f3(a43))))
% 70.37/70.51 [190]P9(a196,f132(f250(f3(a2),f3(a54))))
% 70.37/70.51 [191]P9(a197,f132(f250(f3(a1),f3(a54))))
% 70.37/70.51 [192]P9(a198,f132(f250(f3(a4),f3(a54))))
% 70.37/70.51 [193]P9(a199,f132(f250(f3(a43),f3(a54))))
% 70.37/70.51 [194]P9(a200,f132(f250(f3(a54),f3(a54))))
% 70.37/70.51 [195]P9(a201,f132(f250(f3(a65),f3(a54))))
% 70.37/70.51 [196]P9(a202,f132(f250(f3(a76),f3(a54))))
% 70.37/70.51 [197]P9(a203,f132(f250(f3(a87),f3(a54))))
% 70.37/70.51 [198]P9(a204,f132(f250(f3(a98),f3(a54))))
% 70.37/70.51 [199]P9(a205,f132(f250(f3(a109),f3(a54))))
% 70.37/70.51 [200]P9(a207,f132(f250(f3(a2),f3(a65))))
% 70.37/70.51 [201]P9(a208,f132(f250(f3(a1),f3(a65))))
% 70.37/70.51 [202]P9(a209,f132(f250(f3(a4),f3(a65))))
% 70.37/70.51 [203]P9(a210,f132(f250(f3(a43),f3(a65))))
% 70.37/70.51 [204]P9(a211,f132(f250(f3(a54),f3(a65))))
% 70.37/70.51 [205]P9(a212,f132(f250(f3(a65),f3(a65))))
% 70.37/70.51 [206]P9(a213,f132(f250(f3(a76),f3(a65))))
% 70.37/70.51 [207]P9(a214,f132(f250(f3(a87),f3(a65))))
% 70.37/70.51 [208]P9(a215,f132(f250(f3(a98),f3(a65))))
% 70.37/70.51 [209]P9(a216,f132(f250(f3(a109),f3(a65))))
% 70.37/70.51 [210]P9(a218,f132(f250(f3(a2),f3(a76))))
% 70.37/70.51 [211]P9(a219,f132(f250(f3(a1),f3(a76))))
% 70.37/70.51 [212]P9(a220,f132(f250(f3(a4),f3(a76))))
% 70.37/70.51 [213]P9(a221,f132(f250(f3(a43),f3(a76))))
% 70.37/70.51 [214]P9(a222,f132(f250(f3(a54),f3(a76))))
% 70.37/70.51 [215]P9(a223,f132(f250(f3(a65),f3(a76))))
% 70.37/70.51 [216]P9(a224,f132(f250(f3(a76),f3(a76))))
% 70.37/70.51 [217]P9(a225,f132(f250(f3(a87),f3(a76))))
% 70.37/70.51 [218]P9(a226,f132(f250(f3(a98),f3(a76))))
% 70.37/70.51 [219]P9(a227,f132(f250(f3(a109),f3(a76))))
% 70.37/70.51 [220]P9(a229,f132(f250(f3(a2),f3(a87))))
% 70.37/70.51 [221]P9(a230,f132(f250(f3(a1),f3(a87))))
% 70.37/70.51 [222]P9(a231,f132(f250(f3(a4),f3(a87))))
% 70.37/70.51 [223]P9(a232,f132(f250(f3(a43),f3(a87))))
% 70.37/70.51 [224]P9(a233,f132(f250(f3(a54),f3(a87))))
% 70.37/70.51 [225]P9(a234,f132(f250(f3(a65),f3(a87))))
% 70.37/70.51 [226]P9(a235,f132(f250(f3(a76),f3(a87))))
% 70.37/70.51 [227]P9(a236,f132(f250(f3(a87),f3(a87))))
% 70.37/70.51 [228]P9(a237,f132(f250(f3(a98),f3(a87))))
% 70.37/70.51 [229]P9(a238,f132(f250(f3(a109),f3(a87))))
% 70.37/70.51 [230]P9(a240,f132(f250(f3(a2),f3(a98))))
% 70.37/70.51 [231]P9(a241,f132(f250(f3(a1),f3(a98))))
% 70.37/70.51 [232]P9(a242,f132(f250(f3(a4),f3(a98))))
% 70.37/70.51 [233]P9(a243,f132(f250(f3(a43),f3(a98))))
% 70.37/70.51 [234]P9(a244,f132(f250(f3(a54),f3(a98))))
% 70.37/70.51 [235]P9(a245,f132(f250(f3(a65),f3(a98))))
% 70.37/70.52 [236]P9(a246,f132(f250(f3(a76),f3(a98))))
% 70.37/70.52 [237]P9(a247,f132(f250(f3(a87),f3(a98))))
% 70.37/70.52 [238]P9(a248,f132(f250(f3(a98),f3(a98))))
% 70.37/70.52 [239]P9(a249,f132(f250(f3(a109),f3(a98))))
% 70.37/70.52 [240]P9(a251,f132(f250(f3(a2),f3(a109))))
% 70.37/70.52 [241]P9(a252,f132(f250(f3(a1),f3(a109))))
% 70.37/70.52 [242]P9(a253,f132(f250(f3(a4),f3(a109))))
% 70.37/70.52 [243]P9(a254,f132(f250(f3(a43),f3(a109))))
% 70.37/70.52 [244]P9(a255,f132(f250(f3(a54),f3(a109))))
% 70.37/70.52 [245]P9(a256,f132(f250(f3(a65),f3(a109))))
% 70.37/70.52 [246]P9(a257,f132(f250(f3(a76),f3(a109))))
% 70.37/70.52 [247]P9(a258,f132(f250(f3(a87),f3(a109))))
% 70.37/70.52 [248]P9(a259,f132(f250(f3(a98),f3(a109))))
% 70.37/70.52 [249]P9(a260,f132(f250(f3(a109),f3(a109))))
% 70.37/70.52 [250]P9(a7,f120(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 70.37/70.52 [251]P9(a8,f120(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 70.37/70.52 [252]P9(a9,f120(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 70.37/70.52 [253]P9(a10,f120(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 70.37/70.52 [254]P9(a11,f120(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 70.37/70.52 [255]P9(a12,f120(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 70.37/70.52 [256]P9(a13,f120(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [257]P9(a14,f120(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [258]P9(a15,f120(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [259]P9(a16,f120(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [260]P9(a18,f120(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [261]P9(a19,f120(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [262]P9(a20,f120(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [263]P9(a21,f120(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [264]P9(a22,f120(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [265]P9(a23,f120(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [266]P9(a24,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [267]P9(a25,f120(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [268]P9(a26,f120(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [269]P9(a27,f120(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [270]P9(a29,f120(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [271]P9(a30,f120(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [272]P9(a31,f120(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [273]P9(a32,f120(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [274]P9(a33,f120(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [275]P9(a34,f120(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [276]P9(a35,f120(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [277]P9(a36,f120(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [278]P9(a136,f132(f250(f3(a2),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [279]P9(a137,f132(f250(f3(a1),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [280]P9(a138,f132(f250(f3(a4),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [281]P9(a139,f132(f250(f3(a43),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [282]P9(a140,f132(f250(f3(a54),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [283]P9(a141,f132(f250(f3(a65),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [284]P9(a142,f132(f250(f3(a76),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [285]P9(a143,f132(f250(f3(a87),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [286]P9(a144,f132(f250(f3(a98),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [287]P9(a145,f132(f250(f3(a109),f250(f3(a2),f3(a1)))))
% 70.49/70.52 [288]P9(a147,f132(f250(f3(a2),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [289]P9(a148,f132(f250(f3(a1),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [290]P9(a149,f132(f250(f3(a4),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [291]P9(a150,f132(f250(f3(a43),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [292]P9(a151,f132(f250(f3(a54),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [293]P9(a152,f132(f250(f3(a65),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [294]P9(a153,f132(f250(f3(a76),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [295]P9(a154,f132(f250(f3(a87),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [296]P9(a155,f132(f250(f3(a98),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [297]P9(a156,f132(f250(f3(a109),f250(f3(a1),f3(a1)))))
% 70.49/70.52 [298]P9(a158,f132(f250(f3(a2),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [299]P9(a159,f132(f250(f3(a1),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [300]P9(a160,f132(f250(f3(a4),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [301]P9(a161,f132(f250(f3(a43),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [302]P9(a162,f132(f250(f3(a54),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [303]P9(a163,f132(f250(f3(a65),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [304]P9(a164,f132(f250(f3(a76),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [305]P9(a165,f132(f250(f3(a87),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [306]P9(a166,f132(f250(f3(a98),f250(f3(a4),f3(a1)))))
% 70.49/70.52 [407]~P3(a17,x4071)
% 70.49/70.52 [410]P7(f3(x4101))+~P1(f3(x4101))
% 70.49/70.52 [408]~E(x4081,x4082)+P5(x4081,x4082)
% 70.49/70.52 [409]~P3(x4092,x4091)+~E(x4091,x4092)
% 70.49/70.52 [412]~P3(x4121,x4122)+P5(x4121,x4122)
% 70.49/70.52 [414]~P3(x4142,x4141)+~P3(x4141,x4142)
% 70.49/70.52 [415]~P7(x4152)+P7(f250(f3(x4151),x4152))
% 70.49/70.52 [425]~P4(x4253,x4251,x4252)+P10(x4251,x4252,x4253)
% 70.49/70.52 [426]~P10(x4262,x4263,x4261)+P4(x4261,x4262,x4263)
% 70.49/70.52 [416]~P7(x4163)+P8(f3(x4161),f250(f3(x4162),x4163))
% 70.49/70.52 [421]~P8(x4212,x4214)+P8(f250(f3(x4211),x4212),f250(f3(x4213),x4214))
% 70.49/70.52 [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))
% 70.49/70.52 [411]P3(x4112,x4111)+P3(x4111,x4112)+E(x4111,x4112)
% 70.49/70.52 [413]P3(x4131,x4132)+~P5(x4131,x4132)+E(x4131,x4132)
% 70.49/70.52 [423]P5(x4231,x4232)+~P3(x4231,x4233)+~P10(x4232,a1,x4233)
% 70.49/70.52 [420]P8(f3(x4201),f3(x4202))+~P8(f3(x4203),f3(x4202))+~P8(f3(x4201),f3(x4203))
% 70.49/70.52 [422]P10(x4221,x4222,a2)+~P9(x4221,f120(x4223))+~P9(x4222,f132(x4223))
% 70.49/70.52 [424]~P7(x4242)+~P8(f3(x4241),f3(x4243))+P8(f250(f3(x4241),x4242),f250(f3(x4243),x4242))
% 70.49/70.52 [427]~P10(x4273,x4274,x4271)+E(x4271,x4272)+~P10(x4273,x4274,x4272)
% 70.49/70.52 [428]~P10(x4283,x4281,x4284)+E(x4281,x4282)+~P10(x4283,x4282,x4284)
% 70.49/70.52 [429]~P10(x4291,x4293,x4294)+E(x4291,x4292)+~P10(x4292,x4293,x4294)
% 70.49/70.52 [417]P3(x4171,x4172)+~P9(x4172,f120(x4173))+~P9(x4171,f132(x4174))
% 70.49/70.52 [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))
% 70.49/70.52 [418]P3(x4181,x4182)+~P8(x4183,x4184)+~P9(x4182,f132(x4183))+~P9(x4181,f132(x4184))
% 70.49/70.52 [419]P3(x4191,x4192)+~P8(x4193,x4194)+~P9(x4192,f120(x4194))+~P9(x4191,f120(x4193))
% 70.49/70.52 [430]~P10(x4302,x4301,x4303)+P10(x4301,x4302,x4303)+~P9(x4302,f120(x4304))+~P9(x4301,f132(x4305))
% 70.49/70.52 [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)))
% 70.49/70.52 [431]P10(x4311,x4312,x4313)+~P6(f3(a2),x4316,x4315,x4314)+~P9(x4313,f120(x4314))+~P9(x4312,f120(x4315))+~P9(x4311,f120(x4316))
% 70.49/70.52 [432]P10(x4321,x4322,x4323)+~P6(f3(a2),x4326,x4325,x4324)+~P9(x4323,f132(x4324))+~P9(x4322,f132(x4325))+~P9(x4321,f132(x4326))
% 70.49/70.52 [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))
% 70.49/70.52 [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))
% 70.49/70.52 [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))
% 70.49/70.52 [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))
% 70.49/70.52 %EqnAxiom
% 70.49/70.52 [1]E(x11,x11)
% 70.49/70.52 [2]E(x22,x21)+~E(x21,x22)
% 70.49/70.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 70.49/70.52 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 70.49/70.52 [5]~E(x51,x52)+E(f250(x51,x53),f250(x52,x53))
% 70.49/70.52 [6]~E(x61,x62)+E(f250(x63,x61),f250(x63,x62))
% 70.49/70.52 [7]~E(x71,x72)+E(f132(x71),f132(x72))
% 70.49/70.52 [8]~E(x81,x82)+E(f120(x81),f120(x82))
% 70.49/70.52 [9]~P1(x91)+P1(x92)+~E(x91,x92)
% 70.49/70.52 [10]P2(x102,x103,x104,x105)+~E(x101,x102)+~P2(x101,x103,x104,x105)
% 70.49/70.52 [11]P2(x113,x112,x114,x115)+~E(x111,x112)+~P2(x113,x111,x114,x115)
% 70.49/70.52 [12]P2(x123,x124,x122,x125)+~E(x121,x122)+~P2(x123,x124,x121,x125)
% 70.49/70.52 [13]P2(x133,x134,x135,x132)+~E(x131,x132)+~P2(x133,x134,x135,x131)
% 70.49/70.52 [14]P6(x142,x143,x144,x145)+~E(x141,x142)+~P6(x141,x143,x144,x145)
% 70.49/70.52 [15]P6(x153,x152,x154,x155)+~E(x151,x152)+~P6(x153,x151,x154,x155)
% 70.49/70.52 [16]P6(x163,x164,x162,x165)+~E(x161,x162)+~P6(x163,x164,x161,x165)
% 70.49/70.52 [17]P6(x173,x174,x175,x172)+~E(x171,x172)+~P6(x173,x174,x175,x171)
% 70.49/70.52 [18]~P7(x181)+P7(x182)+~E(x181,x182)
% 70.49/70.52 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193)
% 70.49/70.52 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201)
% 70.49/70.52 [21]P8(x212,x213)+~E(x211,x212)+~P8(x211,x213)
% 70.49/70.52 [22]P8(x223,x222)+~E(x221,x222)+~P8(x223,x221)
% 70.49/70.52 [23]P10(x232,x233,x234)+~E(x231,x232)+~P10(x231,x233,x234)
% 70.49/70.52 [24]P10(x243,x242,x244)+~E(x241,x242)+~P10(x243,x241,x244)
% 70.49/70.52 [25]P10(x253,x254,x252)+~E(x251,x252)+~P10(x253,x254,x251)
% 70.49/70.52 [26]P9(x262,x263)+~E(x261,x262)+~P9(x261,x263)
% 70.49/70.52 [27]P9(x273,x272)+~E(x271,x272)+~P9(x273,x271)
% 70.49/70.52 [28]P5(x282,x283)+~E(x281,x282)+~P5(x281,x283)
% 70.49/70.52 [29]P5(x293,x292)+~E(x291,x292)+~P5(x293,x291)
% 70.49/70.52 [30]P4(x302,x303,x304)+~E(x301,x302)+~P4(x301,x303,x304)
% 70.49/70.52 [31]P4(x313,x312,x314)+~E(x311,x312)+~P4(x313,x311,x314)
% 70.49/70.52 [32]P4(x323,x324,x322)+~E(x321,x322)+~P4(x323,x324,x321)
% 70.49/70.52
% 70.49/70.52 %-------------------------------------------
% 70.49/70.52 cnf(440,plain,
% 70.49/70.52 (P5(x4401,x4401)),
% 70.49/70.52 inference(equality_inference,[],[408])).
% 70.49/70.52 cnf(441,plain,
% 70.49/70.52 (~P3(x4411,x4411)),
% 70.49/70.52 inference(equality_inference,[],[409])).
% 70.49/70.52 cnf(444,plain,
% 70.49/70.52 (~E(a121,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,51,61,417,19])).
% 70.49/70.52 cnf(447,plain,
% 70.49/70.52 (~P3(x4471,x4471)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(450,plain,
% 70.49/70.52 (P6(f3(a2),f3(a2),f3(a2),f3(a2))),
% 70.49/70.52 inference(scs_inference,[],[407,441,307,51,52,61,417,19,20,422,436])).
% 70.49/70.52 cnf(452,plain,
% 70.49/70.52 (~P8(f3(a1),f3(a1))),
% 70.49/70.52 inference(scs_inference,[],[407,441,447,307,51,52,61,417,19,20,422,436,418])).
% 70.49/70.52 cnf(453,plain,
% 70.49/70.52 (~P3(x4531,x4531)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(458,plain,
% 70.49/70.52 (P10(a121,a1,a2)),
% 70.49/70.52 inference(scs_inference,[],[407,441,447,453,307,51,52,61,417,19,20,422,436,418,419,430])).
% 70.49/70.52 cnf(466,plain,
% 70.49/70.52 (~E(f3(a1),f3(a2))),
% 70.49/70.52 inference(scs_inference,[],[407,441,447,453,307,42,51,52,61,417,19,20,422,436,418,419,430,431,414,10,21,22])).
% 70.49/70.52 cnf(467,plain,
% 70.49/70.52 (~P8(f3(a1),f3(a2))),
% 70.49/70.52 inference(scs_inference,[],[407,441,447,453,307,42,51,52,61,417,19,20,422,436,418,419,430,431,414,10,21,22,420])).
% 70.49/70.52 cnf(469,plain,
% 70.49/70.52 (~E(a2,a1)),
% 70.49/70.52 inference(scs_inference,[],[407,441,447,453,307,42,51,52,61,417,19,20,422,436,418,419,430,431,414,10,21,22,420,4])).
% 70.49/70.52 cnf(481,plain,
% 70.49/70.52 (~E(a1,a2)),
% 70.49/70.52 inference(scs_inference,[],[466,4])).
% 70.49/70.52 cnf(482,plain,
% 70.49/70.52 (~P8(f3(a4),f3(a2))),
% 70.49/70.52 inference(scs_inference,[],[466,467,43,4,420])).
% 70.49/70.52 cnf(486,plain,
% 70.49/70.52 (P10(a4,a133,a2)),
% 70.49/70.52 inference(scs_inference,[],[466,467,308,43,53,62,307,4,420,436,422])).
% 70.49/70.52 cnf(488,plain,
% 70.49/70.52 (~E(f3(a4),f3(a1))),
% 70.49/70.52 inference(scs_inference,[],[452,466,467,308,43,53,62,307,4,420,436,422,22])).
% 70.49/70.52 cnf(491,plain,
% 70.49/70.52 (~E(a4,a133)),
% 70.49/70.52 inference(scs_inference,[],[452,441,466,467,308,43,53,62,307,4,420,436,422,22,417,20])).
% 70.49/70.52 cnf(492,plain,
% 70.49/70.52 (~P3(x4921,x4921)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(495,plain,
% 70.49/70.52 (~P8(f3(a4),f3(a4))),
% 70.49/70.52 inference(scs_inference,[],[407,452,441,492,466,467,308,43,53,62,307,4,420,436,422,22,417,20,19,419])).
% 70.49/70.52 cnf(496,plain,
% 70.49/70.52 (~P3(x4961,x4961)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(498,plain,
% 70.49/70.52 (P10(a133,a4,a2)),
% 70.49/70.52 inference(scs_inference,[],[407,452,441,492,466,467,308,43,53,62,307,4,420,436,422,22,417,20,19,419,430])).
% 70.49/70.52 cnf(500,plain,
% 70.49/70.52 (~P8(f3(a43),f3(a43))),
% 70.49/70.52 inference(scs_inference,[],[407,452,441,492,496,466,467,308,43,53,62,63,307,4,420,436,422,22,417,20,19,419,430,418])).
% 70.49/70.52 cnf(503,plain,
% 70.49/70.52 (~P3(a4,a133)),
% 70.49/70.52 inference(scs_inference,[],[407,452,441,492,496,466,467,308,43,53,62,63,307,4,420,436,422,22,417,20,19,419,430,418,414])).
% 70.49/70.52 cnf(506,plain,
% 70.49/70.52 (~E(f3(a1),f3(a4))),
% 70.49/70.52 inference(scs_inference,[],[407,452,441,492,496,466,450,467,308,43,53,62,63,307,4,420,436,422,22,417,20,19,419,430,418,414,16,21])).
% 70.49/70.52 cnf(514,plain,
% 70.49/70.52 (~E(a4,a1)),
% 70.49/70.52 inference(scs_inference,[],[488,4])).
% 70.49/70.52 cnf(515,plain,
% 70.49/70.52 (~P8(f3(a4),f3(a1))),
% 70.49/70.52 inference(scs_inference,[],[495,488,43,4,420])).
% 70.49/70.52 cnf(517,plain,
% 70.49/70.52 (P6(f3(a4),f3(a2),f3(a2),f3(a4))),
% 70.49/70.52 inference(scs_inference,[],[495,488,309,43,307,4,420,436])).
% 70.49/70.52 cnf(519,plain,
% 70.49/70.52 (P10(a54,a184,a2)),
% 70.49/70.52 inference(scs_inference,[],[495,488,309,55,64,43,307,4,420,436,422])).
% 70.49/70.52 cnf(521,plain,
% 70.49/70.52 (~E(f3(a4),f3(a43))),
% 70.49/70.52 inference(scs_inference,[],[495,500,488,309,44,55,64,43,307,4,420,436,422,21])).
% 70.49/70.52 cnf(522,plain,
% 70.49/70.52 (P3(a184,a2)),
% 70.49/70.52 inference(scs_inference,[],[495,500,488,51,309,44,55,64,43,307,4,420,436,422,21,417])).
% 70.49/70.52 cnf(524,plain,
% 70.49/70.52 (~E(f3(a43),f3(a4))),
% 70.49/70.52 inference(scs_inference,[],[495,500,488,51,309,44,55,64,43,307,4,420,436,422,21,417,22])).
% 70.49/70.52 cnf(526,plain,
% 70.49/70.52 (~P3(x5261,x5261)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(527,plain,
% 70.49/70.52 (~E(a184,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,495,500,441,488,51,309,44,55,64,43,307,4,420,436,422,21,417,22,20,19])).
% 70.49/70.52 cnf(529,plain,
% 70.49/70.52 (~P8(f3(a54),f3(a54))),
% 70.49/70.52 inference(scs_inference,[],[407,495,500,441,526,488,51,309,44,55,64,43,307,4,420,436,422,21,417,22,20,19,419])).
% 70.49/70.52 cnf(530,plain,
% 70.49/70.52 (~P3(x5301,x5301)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(534,plain,
% 70.49/70.52 (~P8(f3(a65),f3(a65))),
% 70.49/70.52 inference(scs_inference,[],[407,495,500,441,526,530,488,51,309,44,55,64,65,43,307,4,420,436,422,21,417,22,20,19,419,430,418])).
% 70.49/70.52 cnf(540,plain,
% 70.49/70.52 (P5(x5401,x5402)+~E(x5402,x5401)),
% 70.49/70.52 inference(scs_inference,[],[407,495,500,441,526,530,440,488,51,309,44,55,64,65,43,307,4,420,436,422,21,417,22,20,19,419,430,418,414,27,28])).
% 70.49/70.52 cnf(544,plain,
% 70.49/70.52 (~E(a1,a4)),
% 70.49/70.52 inference(scs_inference,[],[506,4])).
% 70.49/70.52 cnf(545,plain,
% 70.49/70.52 (P3(a206,a2)),
% 70.49/70.52 inference(scs_inference,[],[506,51,66,4,417])).
% 70.49/70.52 cnf(549,plain,
% 70.49/70.52 (~P8(f3(a54),f3(a43))),
% 70.49/70.52 inference(scs_inference,[],[529,506,51,45,57,66,4,417,422,420])).
% 70.49/70.52 cnf(553,plain,
% 70.49/70.52 (~E(f3(a43),f3(a54))),
% 70.49/70.52 inference(scs_inference,[],[529,506,51,310,45,57,66,307,4,417,422,420,436,21])).
% 70.49/70.52 cnf(554,plain,
% 70.49/70.52 (~E(f3(a54),f3(a43))),
% 70.49/70.52 inference(scs_inference,[],[529,500,506,51,310,45,57,66,307,4,417,422,420,436,21,22])).
% 70.49/70.52 cnf(556,plain,
% 70.49/70.52 (~P3(x5561,x5561)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(557,plain,
% 70.49/70.52 (~E(a206,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,529,500,441,506,51,310,45,57,66,307,4,417,422,420,436,21,22,20,19])).
% 70.49/70.52 cnf(559,plain,
% 70.49/70.52 (~P8(f3(a76),f3(a76))),
% 70.49/70.52 inference(scs_inference,[],[407,529,500,441,556,506,51,310,45,57,66,307,4,417,422,420,436,21,22,20,19,419])).
% 70.49/70.52 cnf(560,plain,
% 70.49/70.52 (~P3(x5601,x5601)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(562,plain,
% 70.49/70.52 (P10(a206,a76,a2)),
% 70.49/70.52 inference(scs_inference,[],[407,529,500,441,556,506,51,310,45,57,66,307,4,417,422,420,436,21,22,20,19,419,430])).
% 70.49/70.52 cnf(564,plain,
% 70.49/70.52 (~P8(f3(a87),f3(a87))),
% 70.49/70.52 inference(scs_inference,[],[407,529,500,441,556,560,506,51,310,45,57,66,67,307,4,417,422,420,436,21,22,20,19,419,430,418])).
% 70.49/70.52 cnf(567,plain,
% 70.49/70.52 (~P3(a2,a206)),
% 70.49/70.52 inference(scs_inference,[],[407,529,500,441,556,560,506,51,310,45,57,66,67,307,4,417,422,420,436,21,22,20,19,419,430,418,414])).
% 70.49/70.52 cnf(574,plain,
% 70.49/70.52 (P9(x5741,f120(f3(a2)))+~E(a2,x5741)),
% 70.49/70.52 inference(scs_inference,[],[407,529,500,441,556,560,506,458,51,517,310,45,54,57,66,67,307,4,417,422,420,436,21,22,20,19,419,430,418,414,11,23,27,10,15,26])).
% 70.49/70.52 cnf(581,plain,
% 70.49/70.52 (~E(a4,a43)),
% 70.49/70.52 inference(scs_inference,[],[521,4])).
% 70.49/70.52 cnf(584,plain,
% 70.49/70.52 (~P8(f3(a65),f3(a54))),
% 70.49/70.52 inference(scs_inference,[],[534,521,311,46,307,4,436,420])).
% 70.49/70.52 cnf(586,plain,
% 70.49/70.52 (P3(a228,a2)),
% 70.49/70.52 inference(scs_inference,[],[534,521,51,311,46,68,307,4,436,420,417])).
% 70.49/70.52 cnf(590,plain,
% 70.49/70.52 (~E(f3(a65),f3(a54))),
% 70.49/70.52 inference(scs_inference,[],[534,529,521,51,311,46,59,68,307,4,436,420,417,422,22])).
% 70.49/70.52 cnf(592,plain,
% 70.49/70.52 (~P3(x5921,x5921)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(593,plain,
% 70.49/70.52 (~E(f3(a54),f3(a65))),
% 70.49/70.52 inference(scs_inference,[],[534,529,441,521,51,311,46,59,68,307,4,436,420,417,422,22,20,21])).
% 70.49/70.52 cnf(594,plain,
% 70.49/70.52 (~E(a228,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,534,529,441,521,51,311,46,59,68,307,4,436,420,417,422,22,20,21,19])).
% 70.49/70.52 cnf(598,plain,
% 70.49/70.52 (~P8(f3(a98),f3(a98))),
% 70.49/70.52 inference(scs_inference,[],[407,534,529,441,592,521,51,311,46,59,68,307,4,436,420,417,422,22,20,21,19,430,419])).
% 70.49/70.52 cnf(599,plain,
% 70.49/70.52 (~P3(x5991,x5991)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(601,plain,
% 70.49/70.52 (~P8(f3(a109),f3(a109))),
% 70.49/70.52 inference(scs_inference,[],[407,534,529,441,592,599,521,51,311,46,59,68,69,307,4,436,420,417,422,22,20,21,19,430,419,418])).
% 70.49/70.52 cnf(618,plain,
% 70.49/70.52 (~E(a43,a4)),
% 70.49/70.52 inference(scs_inference,[],[524,4])).
% 70.49/70.52 cnf(621,plain,
% 70.49/70.52 (P3(a134,a2)),
% 70.49/70.52 inference(scs_inference,[],[524,51,160,70,4,422,417])).
% 70.49/70.52 cnf(625,plain,
% 70.49/70.52 (~P8(f3(a76),f3(a65))),
% 70.49/70.52 inference(scs_inference,[],[559,524,51,312,47,160,70,307,4,422,417,436,420])).
% 70.49/70.52 cnf(629,plain,
% 70.49/70.52 (~E(f3(a65),f3(a76))),
% 70.49/70.52 inference(scs_inference,[],[559,441,524,51,312,47,160,70,307,4,422,417,436,420,20,21])).
% 70.49/70.52 cnf(630,plain,
% 70.49/70.52 (~E(f3(a76),f3(a65))),
% 70.49/70.52 inference(scs_inference,[],[559,534,441,524,51,312,47,160,70,307,4,422,417,436,420,20,21,22])).
% 70.49/70.52 cnf(631,plain,
% 70.49/70.52 (~E(a134,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,559,534,441,524,51,312,47,160,70,307,4,422,417,436,420,20,21,22,19])).
% 70.49/70.52 cnf(648,plain,
% 70.49/70.52 (~E(a43,a54)),
% 70.49/70.52 inference(scs_inference,[],[553,4])).
% 70.49/70.52 cnf(649,plain,
% 70.49/70.52 (P10(a17,a146,a2)),
% 70.49/70.52 inference(scs_inference,[],[553,162,72,4,422])).
% 70.49/70.52 cnf(653,plain,
% 70.49/70.52 (~P8(f3(a87),f3(a76))),
% 70.49/70.52 inference(scs_inference,[],[564,553,313,48,162,72,307,4,422,436,420])).
% 70.49/70.52 cnf(655,plain,
% 70.49/70.52 (P3(a146,a2)),
% 70.49/70.52 inference(scs_inference,[],[564,553,51,313,48,162,72,307,4,422,436,420,417])).
% 70.49/70.52 cnf(657,plain,
% 70.49/70.52 (~E(a2,a146)),
% 70.49/70.52 inference(scs_inference,[],[564,441,553,51,313,48,162,72,307,4,422,436,420,417,20])).
% 70.49/70.52 cnf(658,plain,
% 70.49/70.52 (~P3(x6581,x6581)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(659,plain,
% 70.49/70.52 (~E(f3(a87),f3(a76))),
% 70.49/70.52 inference(scs_inference,[],[564,559,441,553,51,313,48,162,72,307,4,422,436,420,417,20,22])).
% 70.49/70.52 cnf(660,plain,
% 70.49/70.52 (~E(a146,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,564,559,441,553,51,313,48,162,72,307,4,422,436,420,417,20,22,19])).
% 70.49/70.52 cnf(662,plain,
% 70.49/70.52 (~E(f3(a76),f3(a87))),
% 70.49/70.52 inference(scs_inference,[],[407,564,559,441,553,51,313,48,162,72,307,4,422,436,420,417,20,22,19,21])).
% 70.49/70.52 cnf(663,plain,
% 70.49/70.52 (P10(a146,a17,a2)),
% 70.49/70.52 inference(scs_inference,[],[407,564,559,441,553,51,313,48,162,72,307,4,422,436,420,417,20,22,19,21,430])).
% 70.49/70.52 cnf(666,plain,
% 70.49/70.52 (~P3(x6661,x6661)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(671,plain,
% 70.49/70.52 (~P3(a2,a146)),
% 70.49/70.52 inference(scs_inference,[],[407,564,559,441,658,666,553,51,313,48,162,72,73,307,4,422,436,420,417,20,22,19,21,430,418,419,414])).
% 70.49/70.52 cnf(677,plain,
% 70.49/70.52 (~E(a54,a43)),
% 70.49/70.52 inference(scs_inference,[],[554,4])).
% 70.49/70.52 cnf(680,plain,
% 70.49/70.52 (~P8(f3(a109),f3(a98))),
% 70.49/70.52 inference(scs_inference,[],[601,554,50,163,73,4,422,420])).
% 70.49/70.52 cnf(682,plain,
% 70.49/70.52 (P3(a157,a2)),
% 70.49/70.52 inference(scs_inference,[],[601,554,51,50,163,73,4,422,420,417])).
% 70.49/70.52 cnf(688,plain,
% 70.49/70.52 (~E(a157,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,601,441,554,51,314,50,163,73,307,4,422,420,417,436,20,19])).
% 70.49/70.52 cnf(690,plain,
% 70.49/70.52 (~E(f3(a87),f3(a98))),
% 70.49/70.52 inference(scs_inference,[],[407,601,598,441,554,51,314,49,50,163,73,307,4,422,420,417,436,20,19,21])).
% 70.49/70.52 cnf(691,plain,
% 70.49/70.52 (~E(f3(a98),f3(a87))),
% 70.49/70.52 inference(scs_inference,[],[407,601,598,564,441,554,51,314,49,50,163,73,307,4,422,420,417,436,20,19,21,22])).
% 70.49/70.52 cnf(706,plain,
% 70.49/70.52 (~E(a65,a54)),
% 70.49/70.52 inference(scs_inference,[],[590,4])).
% 70.49/70.52 cnf(709,plain,
% 70.49/70.52 (P3(a168,a2)),
% 70.49/70.52 inference(scs_inference,[],[590,51,165,75,4,422,417])).
% 70.49/70.52 cnf(713,plain,
% 70.49/70.52 (~P8(f3(a98),f3(a87))),
% 70.49/70.52 inference(scs_inference,[],[598,590,51,315,165,75,49,307,4,422,417,436,420])).
% 70.49/70.52 cnf(715,plain,
% 70.49/70.52 (~E(a2,a168)),
% 70.49/70.52 inference(scs_inference,[],[598,441,590,51,315,165,75,49,307,4,422,417,436,420,20])).
% 70.49/70.52 cnf(716,plain,
% 70.49/70.52 (~P3(x7161,x7161)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(717,plain,
% 70.49/70.52 (~E(f3(a98),f3(a109))),
% 70.49/70.52 inference(scs_inference,[],[601,598,441,590,51,315,165,50,75,49,307,4,422,417,436,420,20,21])).
% 70.49/70.52 cnf(718,plain,
% 70.49/70.52 (~E(f3(a109),f3(a98))),
% 70.49/70.52 inference(scs_inference,[],[601,598,441,590,51,315,165,50,75,49,307,4,422,417,436,420,20,21,22])).
% 70.49/70.52 cnf(719,plain,
% 70.49/70.52 (~E(a168,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,601,598,441,590,51,315,165,50,75,49,307,4,422,417,436,420,20,21,22,19])).
% 70.49/70.52 cnf(722,plain,
% 70.49/70.52 (~P3(x7221,x7221)),
% 70.49/70.52 inference(rename_variables,[],[441])).
% 70.49/70.52 cnf(729,plain,
% 70.49/70.52 (~P3(a2,a168)),
% 70.49/70.52 inference(scs_inference,[],[407,601,598,441,716,722,590,51,315,165,167,76,50,75,49,307,4,422,417,436,420,20,21,22,19,419,430,418,414])).
% 70.49/70.52 cnf(731,plain,
% 70.49/70.52 (P9(x7311,f120(f3(a87)))+~E(a87,x7311)),
% 70.49/70.52 inference(scs_inference,[],[407,601,598,441,716,722,590,51,315,58,165,167,76,50,75,49,307,4,422,417,436,420,20,21,22,19,419,430,418,414,26])).
% 70.49/70.52 cnf(743,plain,
% 70.49/70.52 (~E(a54,a65)),
% 70.49/70.52 inference(scs_inference,[],[593,4])).
% 70.49/70.52 cnf(748,plain,
% 70.49/70.52 (~P8(f3(a43),f3(a4))),
% 70.49/70.52 inference(scs_inference,[],[500,593,316,166,76,44,307,4,422,436,420])).
% 70.49/70.52 cnf(750,plain,
% 70.49/70.52 (P3(a169,a2)),
% 70.49/70.52 inference(scs_inference,[],[500,593,51,316,166,76,44,307,4,422,436,420,417])).
% 70.49/70.52 cnf(754,plain,
% 70.49/70.52 (~E(a169,a17)),
% 70.49/70.52 inference(scs_inference,[],[407,500,441,593,51,316,166,76,44,307,4,422,436,420,417,20,19])).
% 70.49/70.52 cnf(778,plain,
% 70.49/70.52 (~E(a65,a76)),
% 70.49/70.52 inference(scs_inference,[],[629,4])).
% 70.49/70.52 cnf(779,plain,
% 70.49/70.52 (P10(a42,a172,a2)),
% 70.49/70.52 inference(scs_inference,[],[629,169,79,4,422])).
% 70.49/70.52 cnf(781,plain,
% 70.49/70.52 (~P8(f3(a109),f3(a87))),
% 70.49/70.53 inference(scs_inference,[],[629,49,680,169,79,4,422,420])).
% 70.49/70.53 cnf(783,plain,
% 70.49/70.53 (P3(a172,a2)),
% 70.49/70.53 inference(scs_inference,[],[629,51,49,680,169,79,4,422,420,417])).
% 70.49/70.53 cnf(785,plain,
% 70.49/70.53 (P6(f3(a2),f3(a1),f3(a2),f3(a1))),
% 70.49/70.53 inference(scs_inference,[],[629,51,49,680,317,169,79,4,422,420,417,436])).
% 70.49/70.53 cnf(789,plain,
% 70.49/70.53 (~E(a172,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,441,629,51,49,680,317,169,79,4,422,420,417,436,20,19])).
% 70.49/70.53 cnf(791,plain,
% 70.49/70.53 (P10(a172,a42,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,441,629,51,49,680,317,169,79,4,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(805,plain,
% 70.49/70.53 (~E(a76,a65)),
% 70.49/70.53 inference(scs_inference,[],[630,4])).
% 70.49/70.53 cnf(806,plain,
% 70.49/70.53 (P10(a45,a175,a2)),
% 70.49/70.53 inference(scs_inference,[],[630,171,81,4,422])).
% 70.49/70.53 cnf(808,plain,
% 70.49/70.53 (P3(a175,a2)),
% 70.49/70.53 inference(scs_inference,[],[630,51,171,81,4,422,417])).
% 70.49/70.53 cnf(812,plain,
% 70.49/70.53 (~P8(f3(a54),f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[630,51,44,549,318,171,308,81,4,422,417,436,420])).
% 70.49/70.53 cnf(814,plain,
% 70.49/70.53 (~E(a2,a175)),
% 70.49/70.53 inference(scs_inference,[],[441,630,51,44,549,318,171,308,81,4,422,417,436,420,20])).
% 70.49/70.53 cnf(815,plain,
% 70.49/70.53 (~P3(x8151,x8151)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(816,plain,
% 70.49/70.53 (~E(a175,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,441,630,51,44,549,318,171,308,81,4,422,417,436,420,20,19])).
% 70.49/70.53 cnf(819,plain,
% 70.49/70.53 (~P3(x8191,x8191)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(821,plain,
% 70.49/70.53 (P10(a175,a45,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,441,815,630,51,44,549,318,171,172,308,81,4,422,417,436,420,20,19,418,430])).
% 70.49/70.53 cnf(826,plain,
% 70.49/70.53 (~P3(a2,a175)),
% 70.49/70.53 inference(scs_inference,[],[407,441,815,819,630,51,44,549,318,171,172,83,308,81,4,422,417,436,420,20,19,418,430,419,414])).
% 70.49/70.53 cnf(845,plain,
% 70.49/70.53 (~P8(f3(a65),f3(a43))),
% 70.49/70.53 inference(scs_inference,[],[659,45,584,319,173,83,308,4,422,436,420])).
% 70.49/70.53 cnf(847,plain,
% 70.49/70.53 (P3(a177,a2)),
% 70.49/70.53 inference(scs_inference,[],[659,51,45,584,319,173,83,308,4,422,436,420,417])).
% 70.49/70.53 cnf(851,plain,
% 70.49/70.53 (~E(a177,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,441,659,51,45,584,319,173,83,308,4,422,436,420,417,20,19])).
% 70.49/70.53 cnf(875,plain,
% 70.49/70.53 (~E(a76,a87)),
% 70.49/70.53 inference(scs_inference,[],[662,4])).
% 70.49/70.53 cnf(878,plain,
% 70.49/70.53 (~P8(f3(a76),f3(a54))),
% 70.49/70.53 inference(scs_inference,[],[662,46,625,175,85,4,422,420])).
% 70.49/70.53 cnf(880,plain,
% 70.49/70.53 (P3(a179,a2)),
% 70.49/70.53 inference(scs_inference,[],[662,51,46,625,175,85,4,422,420,417])).
% 70.49/70.53 cnf(884,plain,
% 70.49/70.53 (~E(a2,a179)),
% 70.49/70.53 inference(scs_inference,[],[441,662,51,46,625,320,175,85,317,4,422,420,417,436,20])).
% 70.49/70.53 cnf(885,plain,
% 70.49/70.53 (~P3(x8851,x8851)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(886,plain,
% 70.49/70.53 (~E(a179,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,441,662,51,46,625,320,175,85,317,4,422,420,417,436,20,19])).
% 70.49/70.53 cnf(889,plain,
% 70.49/70.53 (~P3(x8891,x8891)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(896,plain,
% 70.49/70.53 (~P3(a2,a179)),
% 70.49/70.53 inference(scs_inference,[],[407,441,885,889,662,51,46,625,320,175,176,87,85,317,4,422,420,417,436,20,19,418,430,419,414])).
% 70.49/70.53 cnf(910,plain,
% 70.49/70.53 (~E(a87,a98)),
% 70.49/70.53 inference(scs_inference,[],[690,4])).
% 70.49/70.53 cnf(913,plain,
% 70.49/70.53 (P3(a181,a2)),
% 70.49/70.53 inference(scs_inference,[],[690,51,177,87,4,422,417])).
% 70.49/70.53 cnf(915,plain,
% 70.49/70.53 (P6(f3(a54),f3(a2),f3(a1),f3(a65))),
% 70.49/70.53 inference(scs_inference,[],[690,51,321,177,87,308,4,422,417,436])).
% 70.49/70.53 cnf(917,plain,
% 70.49/70.53 (~P8(f3(a87),f3(a65))),
% 70.49/70.53 inference(scs_inference,[],[690,51,47,653,321,177,87,308,4,422,417,436,420])).
% 70.49/70.53 cnf(921,plain,
% 70.49/70.53 (~E(a181,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,441,690,51,47,653,321,177,87,308,4,422,417,436,420,20,19])).
% 70.49/70.53 cnf(945,plain,
% 70.49/70.53 (~E(a98,a87)),
% 70.49/70.53 inference(scs_inference,[],[691,4])).
% 70.49/70.53 cnf(946,plain,
% 70.49/70.53 (P10(a53,a183,a2)),
% 70.49/70.53 inference(scs_inference,[],[691,179,89,4,422])).
% 70.49/70.53 cnf(950,plain,
% 70.49/70.53 (~P8(f3(a98),f3(a76))),
% 70.49/70.53 inference(scs_inference,[],[691,48,713,322,179,89,317,4,422,436,420])).
% 70.49/70.53 cnf(952,plain,
% 70.49/70.53 (P3(a183,a2)),
% 70.49/70.53 inference(scs_inference,[],[691,51,48,713,322,179,89,317,4,422,436,420,417])).
% 70.49/70.53 cnf(954,plain,
% 70.49/70.53 (~E(a2,a183)),
% 70.49/70.53 inference(scs_inference,[],[441,691,51,48,713,322,179,89,317,4,422,436,420,417,20])).
% 70.49/70.53 cnf(955,plain,
% 70.49/70.53 (~P3(x9551,x9551)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(956,plain,
% 70.49/70.53 (~E(a183,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,441,691,51,48,713,322,179,89,317,4,422,436,420,417,20,19])).
% 70.49/70.53 cnf(959,plain,
% 70.49/70.53 (~P3(x9591,x9591)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(961,plain,
% 70.49/70.53 (P10(a183,a53,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,441,955,691,51,48,713,322,179,180,89,317,4,422,436,420,417,20,19,418,430])).
% 70.49/70.53 cnf(966,plain,
% 70.49/70.53 (~P3(a2,a183)),
% 70.49/70.53 inference(scs_inference,[],[407,441,955,959,691,51,48,713,322,179,180,91,89,317,4,422,436,420,417,20,19,418,430,419,414])).
% 70.49/70.53 cnf(972,plain,
% 70.49/70.53 (P3(a121,a17)),
% 70.49/70.53 inference(scs_inference,[],[444,407,2,411])).
% 70.49/70.53 cnf(973,plain,
% 70.49/70.53 (~E(a98,a109)),
% 70.49/70.53 inference(scs_inference,[],[717,4])).
% 70.49/70.53 cnf(978,plain,
% 70.49/70.53 (P3(a186,a2)),
% 70.49/70.53 inference(scs_inference,[],[717,51,43,748,181,91,4,422,420,417])).
% 70.49/70.53 cnf(983,plain,
% 70.49/70.53 (~P3(x9831,x9831)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(984,plain,
% 70.49/70.53 (~E(a186,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,972,441,717,51,43,748,323,181,91,308,4,422,420,417,436,20,19])).
% 70.49/70.53 cnf(989,plain,
% 70.49/70.53 (~P3(x9891,x9891)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(994,plain,
% 70.49/70.53 (~P3(a2,a186)),
% 70.49/70.53 inference(scs_inference,[],[407,972,441,983,989,717,51,43,748,323,181,182,93,91,308,4,422,420,417,436,20,19,430,418,419,414])).
% 70.49/70.53 cnf(999,plain,
% 70.49/70.53 (P9(x9991,f132(f250(f3(a1),f3(a43))))+~E(a186,x9991)),
% 70.49/70.53 inference(scs_inference,[],[407,972,441,983,989,717,51,43,748,785,323,181,182,93,91,308,4,422,420,417,436,20,19,430,418,419,414,14,13,17,26])).
% 70.49/70.53 cnf(1008,plain,
% 70.49/70.53 (~E(a109,a98)),
% 70.49/70.53 inference(scs_inference,[],[718,4])).
% 70.49/70.53 cnf(1009,plain,
% 70.49/70.53 (P10(a58,a188,a2)),
% 70.49/70.53 inference(scs_inference,[],[718,183,93,4,422])).
% 70.49/70.53 cnf(1011,plain,
% 70.49/70.53 (P3(a188,a2)),
% 70.49/70.53 inference(scs_inference,[],[718,51,183,93,4,422,417])).
% 70.49/70.53 cnf(1015,plain,
% 70.49/70.53 (~P8(f3(a43),f3(a2))),
% 70.49/70.53 inference(scs_inference,[],[718,51,44,482,324,183,93,317,4,422,417,436,420])).
% 70.49/70.53 cnf(1017,plain,
% 70.49/70.53 (~E(a2,a186)),
% 70.49/70.53 inference(scs_inference,[],[978,441,718,51,44,482,324,183,93,317,4,422,417,436,420,20])).
% 70.49/70.53 cnf(1018,plain,
% 70.49/70.53 (~P3(x10181,x10181)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1019,plain,
% 70.49/70.53 (~E(a188,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,978,441,718,51,44,482,324,183,93,317,4,422,417,436,420,20,19])).
% 70.49/70.53 cnf(1024,plain,
% 70.49/70.53 (P10(a188,a58,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,978,441,1018,718,51,44,482,324,183,184,93,317,4,422,417,436,420,20,19,418,430])).
% 70.49/70.53 cnf(1045,plain,
% 70.49/70.53 (P3(a190,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,185,95,422,417])).
% 70.49/70.53 cnf(1047,plain,
% 70.49/70.53 (~P8(f3(a109),f3(a76))),
% 70.49/70.53 inference(scs_inference,[],[51,48,781,185,95,422,417,420])).
% 70.49/70.53 cnf(1052,plain,
% 70.49/70.53 (~P3(x10521,x10521)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1053,plain,
% 70.49/70.53 (~E(a190,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1011,441,51,48,781,325,185,95,308,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1056,plain,
% 70.49/70.53 (~P3(x10561,x10561)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1065,plain,
% 70.49/70.53 (P9(x10651,f132(f250(f3(a65),f3(a43))))+~E(a190,x10651)),
% 70.49/70.53 inference(scs_inference,[],[407,1011,441,1052,1056,51,48,781,325,185,186,97,95,308,422,417,420,436,20,19,418,430,419,414,26])).
% 70.49/70.53 cnf(1079,plain,
% 70.49/70.53 (P3(a192,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,187,97,422,417])).
% 70.49/70.53 cnf(1081,plain,
% 70.49/70.53 (~P8(f3(a54),f3(a1))),
% 70.49/70.53 inference(scs_inference,[],[51,43,812,187,97,422,417,420])).
% 70.49/70.53 cnf(1087,plain,
% 70.49/70.53 (~E(a192,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1045,441,51,43,812,327,187,97,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1113,plain,
% 70.49/70.53 (P3(a194,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,189,99,422,417])).
% 70.49/70.53 cnf(1115,plain,
% 70.49/70.53 (~P8(f3(a65),f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[51,44,845,189,99,422,417,420])).
% 70.49/70.53 cnf(1120,plain,
% 70.49/70.53 (~P3(x11201,x11201)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1121,plain,
% 70.49/70.53 (~E(a194,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1079,441,51,44,845,328,189,309,99,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1126,plain,
% 70.49/70.53 (~P3(x11261,x11261)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1136,plain,
% 70.49/70.53 (P9(x11361,f132(f250(f3(a109),f3(a43))))+~E(a194,x11361)),
% 70.49/70.53 inference(scs_inference,[],[407,1079,441,1120,1126,51,44,845,915,328,189,190,101,309,99,422,417,420,436,20,19,430,418,419,414,17,27,16,26])).
% 70.49/70.53 cnf(1147,plain,
% 70.49/70.53 (P3(a197,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,191,101,422,417])).
% 70.49/70.53 cnf(1149,plain,
% 70.49/70.53 (~P8(f3(a76),f3(a43))),
% 70.49/70.53 inference(scs_inference,[],[51,45,878,191,101,422,417,420])).
% 70.49/70.53 cnf(1155,plain,
% 70.49/70.53 (~E(a197,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1113,441,51,45,878,329,191,327,101,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1181,plain,
% 70.49/70.53 (P3(a199,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,193,103,422,417])).
% 70.49/70.53 cnf(1183,plain,
% 70.49/70.53 (~P8(f3(a87),f3(a54))),
% 70.49/70.53 inference(scs_inference,[],[51,46,917,193,103,422,417,420])).
% 70.49/70.53 cnf(1189,plain,
% 70.49/70.53 (~E(a199,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1147,441,51,46,917,330,193,103,309,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1215,plain,
% 70.49/70.53 (P3(a201,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,195,105,422,417])).
% 70.49/70.53 cnf(1217,plain,
% 70.49/70.53 (~P8(f3(a98),f3(a65))),
% 70.49/70.53 inference(scs_inference,[],[51,47,950,195,105,422,417,420])).
% 70.49/70.53 cnf(1223,plain,
% 70.49/70.53 (~E(a201,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1181,441,51,47,950,331,195,105,327,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1249,plain,
% 70.49/70.53 (P3(a203,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,197,107,422,417])).
% 70.49/70.53 cnf(1251,plain,
% 70.49/70.53 (~P8(f3(a54),f3(a2))),
% 70.49/70.53 inference(scs_inference,[],[51,45,1015,197,107,422,417,420])).
% 70.49/70.53 cnf(1257,plain,
% 70.49/70.53 (~E(a203,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1215,441,51,45,1015,332,197,107,309,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1280,plain,
% 70.49/70.53 (P3(a205,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,199,109,422,417])).
% 70.49/70.53 cnf(1282,plain,
% 70.49/70.53 (~P8(f3(a109),f3(a65))),
% 70.49/70.53 inference(scs_inference,[],[51,47,1047,199,109,422,417,420])).
% 70.49/70.53 cnf(1287,plain,
% 70.49/70.53 (~P3(x12871,x12871)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1288,plain,
% 70.49/70.53 (~E(a205,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1249,441,51,47,1047,333,199,109,327,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1293,plain,
% 70.49/70.53 (P10(a205,a75,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1249,441,1287,51,47,1047,333,199,200,109,327,422,417,420,436,20,19,418,430])).
% 70.49/70.53 cnf(1306,plain,
% 70.49/70.53 (P3(a208,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,201,111,422,417])).
% 70.49/70.53 cnf(1308,plain,
% 70.49/70.53 (~P8(f3(a65),f3(a1))),
% 70.49/70.53 inference(scs_inference,[],[51,43,1115,201,111,422,417,420])).
% 70.49/70.53 cnf(1314,plain,
% 70.49/70.53 (~E(a208,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1280,441,51,43,1115,334,201,111,318,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1316,plain,
% 70.49/70.53 (P10(a208,a78,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1280,441,51,43,1115,334,201,111,318,422,417,420,436,20,19,430])).
% 70.49/70.53 cnf(1338,plain,
% 70.49/70.53 (P10(a80,a210,a2)),
% 70.49/70.53 inference(scs_inference,[],[203,113,422])).
% 70.49/70.53 cnf(1340,plain,
% 70.49/70.53 (P3(a210,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,203,113,422,417])).
% 70.49/70.53 cnf(1342,plain,
% 70.49/70.53 (~P8(f3(a65),f3(a2))),
% 70.49/70.53 inference(scs_inference,[],[51,46,1251,203,113,422,417,420])).
% 70.49/70.53 cnf(1348,plain,
% 70.49/70.53 (~E(a210,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1306,441,51,46,1251,337,203,113,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1374,plain,
% 70.49/70.53 (~P8(f3(a76),f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[44,1149,205,115,422,420])).
% 70.49/70.53 cnf(1376,plain,
% 70.49/70.53 (P3(a212,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,44,1149,205,115,422,420,417])).
% 70.49/70.53 cnf(1384,plain,
% 70.49/70.53 (P10(a212,a82,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1340,441,51,44,1149,338,205,337,115,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1408,plain,
% 70.49/70.53 (P3(a214,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,207,117,422,417])).
% 70.49/70.53 cnf(1410,plain,
% 70.49/70.53 (~P8(f3(a87),f3(a43))),
% 70.49/70.53 inference(scs_inference,[],[51,45,1183,207,117,422,417,420])).
% 70.49/70.53 cnf(1416,plain,
% 70.49/70.53 (~E(a214,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1376,441,51,45,1183,339,207,117,319,422,417,420,436,20,19])).
% 70.49/70.53 cnf(1418,plain,
% 70.49/70.53 (P10(a214,a84,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1376,441,51,45,1183,339,207,117,319,422,417,420,436,20,19,430])).
% 70.49/70.53 cnf(1442,plain,
% 70.49/70.53 (~P8(f3(a98),f3(a54))),
% 70.49/70.53 inference(scs_inference,[],[46,1217,209,119,422,420])).
% 70.49/70.53 cnf(1446,plain,
% 70.49/70.53 (P3(a216,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,46,1217,340,209,119,328,422,420,436,417])).
% 70.49/70.53 cnf(1450,plain,
% 70.49/70.53 (~E(a216,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1408,441,51,46,1217,340,209,119,328,422,420,436,417,20,19])).
% 70.49/70.53 cnf(1474,plain,
% 70.49/70.53 (P7(f250(f3(x14741),f3(a1)))),
% 70.49/70.53 inference(scs_inference,[],[33,410,415])).
% 70.49/70.53 cnf(1475,plain,
% 70.49/70.53 (P10(a89,a219,a2)),
% 70.49/70.53 inference(scs_inference,[],[211,121,422])).
% 70.49/70.53 cnf(1477,plain,
% 70.49/70.53 (P3(a219,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,211,121,422,417])).
% 70.49/70.53 cnf(1481,plain,
% 70.49/70.53 (~P8(f3(a109),f3(a54))),
% 70.49/70.53 inference(scs_inference,[],[51,46,1282,341,211,121,337,422,417,436,420])).
% 70.49/70.53 cnf(1485,plain,
% 70.49/70.53 (~E(a219,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1446,441,51,46,1282,341,211,121,337,422,417,436,420,20,19])).
% 70.49/70.53 cnf(1487,plain,
% 70.49/70.53 (P10(a219,a89,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1446,441,51,46,1282,341,211,121,337,422,417,436,420,20,19,430])).
% 70.49/70.53 cnf(1510,plain,
% 70.49/70.53 (~P8(f3(a76),f3(a2))),
% 70.49/70.53 inference(scs_inference,[],[47,1342,342,213,123,310,422,436,420])).
% 70.49/70.53 cnf(1512,plain,
% 70.49/70.53 (P3(a221,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,47,1342,342,213,123,310,422,436,420,417])).
% 70.49/70.53 cnf(1516,plain,
% 70.49/70.53 (~E(a221,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,1477,441,51,47,1342,342,213,123,310,422,436,420,417,20,19])).
% 70.49/70.53 cnf(1518,plain,
% 70.49/70.53 (P10(a221,a91,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1477,441,51,47,1342,342,213,123,310,422,436,420,417,20,19,430])).
% 70.49/70.53 cnf(1540,plain,
% 70.49/70.53 (P10(a93,a223,a2)),
% 70.49/70.53 inference(scs_inference,[],[215,125,422])).
% 70.49/70.53 cnf(1544,plain,
% 70.49/70.53 (P3(a223,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,43,1374,215,125,422,420,417])).
% 70.49/70.53 cnf(1552,plain,
% 70.49/70.53 (P10(a223,a93,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1512,441,51,43,1374,343,215,125,319,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1569,plain,
% 70.49/70.53 (P10(a95,a225,a2)),
% 70.49/70.53 inference(scs_inference,[],[217,127,422])).
% 70.49/70.53 cnf(1571,plain,
% 70.49/70.53 (P3(a225,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,217,127,422,417])).
% 70.49/70.53 cnf(1573,plain,
% 70.49/70.53 (~P8(f3(a87),f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[51,44,1410,217,127,422,417,420])).
% 70.49/70.53 cnf(1581,plain,
% 70.49/70.53 (P10(a225,a95,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,1544,441,51,44,1410,347,217,127,422,417,420,436,20,19,430])).
% 70.49/70.53 cnf(1604,plain,
% 70.49/70.53 (~P8(f3(a98),f3(a43))),
% 70.49/70.53 inference(scs_inference,[],[522,458,45,1442,219,129,423,422,420])).
% 70.49/70.53 cnf(1606,plain,
% 70.49/70.53 (P3(a227,a2)),
% 70.49/70.53 inference(scs_inference,[],[522,458,51,45,1442,219,129,423,422,420,417])).
% 70.49/70.53 cnf(1612,plain,
% 70.49/70.53 (~E(a227,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,522,1571,441,458,51,45,1442,348,219,338,129,423,422,420,417,436,20,19])).
% 70.49/70.53 cnf(1614,plain,
% 70.49/70.53 (P10(a227,a97,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,522,1571,441,458,51,45,1442,348,219,338,129,423,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1643,plain,
% 70.49/70.53 (~P8(f3(a109),f3(a43))),
% 70.49/70.53 inference(scs_inference,[],[545,458,45,1481,221,131,423,422,420])).
% 70.49/70.53 cnf(1645,plain,
% 70.49/70.53 (P3(a230,a2)),
% 70.49/70.53 inference(scs_inference,[],[545,458,51,45,1481,221,131,423,422,420,417])).
% 70.49/70.53 cnf(1650,plain,
% 70.49/70.53 (~P3(x16501,x16501)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1653,plain,
% 70.49/70.53 (P10(a230,a100,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,545,1606,441,458,51,45,1481,349,221,347,131,423,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1656,plain,
% 70.49/70.53 (~P3(x16561,x16561)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1661,plain,
% 70.49/70.53 (~P3(a2,a230)),
% 70.49/70.53 inference(scs_inference,[],[407,545,1606,441,1650,1656,458,51,45,1481,349,221,222,133,347,131,423,422,420,417,436,20,19,430,418,419,414])).
% 70.49/70.53 cnf(1682,plain,
% 70.49/70.53 (~P8(f3(a87),f3(a2))),
% 70.49/70.53 inference(scs_inference,[],[586,458,48,1510,223,133,423,422,420])).
% 70.49/70.53 cnf(1684,plain,
% 70.49/70.53 (P3(a232,a2)),
% 70.49/70.53 inference(scs_inference,[],[586,458,51,48,1510,223,133,423,422,420,417])).
% 70.49/70.53 cnf(1688,plain,
% 70.49/70.53 (~E(a2,a230)),
% 70.49/70.53 inference(scs_inference,[],[586,1645,441,458,51,48,1510,350,223,133,338,423,422,420,417,436,20])).
% 70.49/70.53 cnf(1689,plain,
% 70.49/70.53 (~P3(x16891,x16891)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1692,plain,
% 70.49/70.53 (P10(a232,a102,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,586,1645,441,458,51,48,1510,350,223,133,338,423,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1695,plain,
% 70.49/70.53 (~P3(x16951,x16951)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1700,plain,
% 70.49/70.53 (~P3(a2,a232)),
% 70.49/70.53 inference(scs_inference,[],[407,586,1645,441,1689,1695,458,51,48,1510,350,223,224,135,133,338,423,422,420,417,436,20,19,430,418,419,414])).
% 70.49/70.53 cnf(1724,plain,
% 70.49/70.53 (P3(a234,a2)),
% 70.49/70.53 inference(scs_inference,[],[621,458,51,43,1573,225,135,423,422,420,417])).
% 70.49/70.53 cnf(1728,plain,
% 70.49/70.53 (~E(a2,a232)),
% 70.49/70.53 inference(scs_inference,[],[621,1684,441,458,51,43,1573,351,225,135,347,423,422,420,417,436,20])).
% 70.49/70.53 cnf(1729,plain,
% 70.49/70.53 (~P3(x17291,x17291)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1730,plain,
% 70.49/70.53 (~E(a234,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,621,1684,441,458,51,43,1573,351,225,135,347,423,422,420,417,436,20,19])).
% 70.49/70.53 cnf(1732,plain,
% 70.49/70.53 (P10(a234,a104,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,621,1684,441,458,51,43,1573,351,225,135,347,423,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1735,plain,
% 70.49/70.53 (~P3(x17351,x17351)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1740,plain,
% 70.49/70.53 (~P3(a2,a234)),
% 70.49/70.53 inference(scs_inference,[],[407,621,1684,441,1729,1735,458,51,43,1573,351,225,226,137,135,347,423,422,420,417,436,20,19,430,418,419,414])).
% 70.49/70.53 cnf(1761,plain,
% 70.49/70.53 (~P8(f3(a98),f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[655,458,44,1604,227,137,423,422,420])).
% 70.49/70.53 cnf(1763,plain,
% 70.49/70.53 (P3(a236,a2)),
% 70.49/70.53 inference(scs_inference,[],[655,458,51,44,1604,227,137,423,422,420,417])).
% 70.49/70.53 cnf(1767,plain,
% 70.49/70.53 (~E(a2,a234)),
% 70.49/70.53 inference(scs_inference,[],[655,1724,441,458,51,44,1604,352,227,137,311,423,422,420,417,436,20])).
% 70.49/70.53 cnf(1768,plain,
% 70.49/70.53 (~P3(x17681,x17681)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1769,plain,
% 70.49/70.53 (~E(a236,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,655,1724,441,458,51,44,1604,352,227,137,311,423,422,420,417,436,20,19])).
% 70.49/70.53 cnf(1771,plain,
% 70.49/70.53 (P10(a236,a106,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,655,1724,441,458,51,44,1604,352,227,137,311,423,422,420,417,436,20,19,430])).
% 70.49/70.53 cnf(1774,plain,
% 70.49/70.53 (~P3(x17741,x17741)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1779,plain,
% 70.49/70.53 (~P3(a2,a236)),
% 70.49/70.53 inference(scs_inference,[],[407,655,1724,441,1768,1774,458,51,44,1604,352,227,228,139,137,311,423,422,420,417,436,20,19,430,418,419,414])).
% 70.49/70.53 cnf(1801,plain,
% 70.49/70.53 (~P8(f3(a109),f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[682,458,44,1643,229,139,423,422,420])).
% 70.49/70.53 cnf(1803,plain,
% 70.49/70.53 (P3(a238,a2)),
% 70.49/70.53 inference(scs_inference,[],[682,458,51,44,1643,229,139,423,422,420,417])).
% 70.49/70.53 cnf(1807,plain,
% 70.49/70.53 (~E(a2,a236)),
% 70.49/70.53 inference(scs_inference,[],[682,1763,441,458,51,44,1643,357,229,139,423,422,420,417,436,20])).
% 70.49/70.53 cnf(1841,plain,
% 70.49/70.53 (~P8(f3(a98),f3(a2))),
% 70.49/70.53 inference(scs_inference,[],[709,458,49,1682,231,141,423,422,420])).
% 70.49/70.53 cnf(1847,plain,
% 70.49/70.53 (~E(a2,a238)),
% 70.49/70.53 inference(scs_inference,[],[709,1803,441,458,51,49,1682,358,231,348,141,423,422,420,417,436,20])).
% 70.49/70.53 cnf(1886,plain,
% 70.49/70.53 (P3(a243,a2)),
% 70.49/70.53 inference(scs_inference,[],[750,458,51,43,1761,233,143,423,422,420,417])).
% 70.49/70.53 cnf(1923,plain,
% 70.49/70.53 (P3(a245,a2)),
% 70.49/70.53 inference(scs_inference,[],[783,458,51,43,1801,235,145,423,422,420,417])).
% 70.49/70.53 cnf(1928,plain,
% 70.49/70.53 (~P3(x19281,x19281)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1934,plain,
% 70.49/70.53 (~P3(x19341,x19341)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(1939,plain,
% 70.49/70.53 (~P3(a2,a245)),
% 70.49/70.53 inference(scs_inference,[],[407,783,1886,441,1928,1934,458,51,43,1801,360,235,236,147,145,330,423,422,420,417,436,20,19,430,418,419,414])).
% 70.49/70.53 cnf(1960,plain,
% 70.49/70.53 (P3(a247,a2)),
% 70.49/70.53 inference(scs_inference,[],[808,50,458,51,1841,237,147,423,422,420,417])).
% 70.49/70.53 cnf(1964,plain,
% 70.49/70.53 (~E(a2,a245)),
% 70.49/70.53 inference(scs_inference,[],[808,1923,441,50,458,51,1841,361,237,147,312,423,422,420,417,436,20])).
% 70.49/70.53 cnf(1998,plain,
% 70.49/70.53 (P3(a249,a2)),
% 70.49/70.53 inference(scs_inference,[],[847,458,51,367,239,149,423,422,436,417])).
% 70.49/70.53 cnf(2000,plain,
% 70.49/70.53 (~E(a2,a247)),
% 70.49/70.53 inference(scs_inference,[],[847,1960,441,458,51,367,239,149,423,422,436,417,20])).
% 70.49/70.53 cnf(2001,plain,
% 70.49/70.53 (~P3(x20011,x20011)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(2005,plain,
% 70.49/70.53 (~P3(x20051,x20051)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(2012,plain,
% 70.49/70.53 (~P3(a2,a249)),
% 70.49/70.53 inference(scs_inference,[],[407,847,1960,441,2001,2005,458,51,367,239,240,151,149,423,422,436,417,20,19,418,430,419,414])).
% 70.49/70.53 cnf(2032,plain,
% 70.49/70.53 (P3(a252,a2)),
% 70.49/70.53 inference(scs_inference,[],[880,51,458,241,151,423,422,417])).
% 70.49/70.53 cnf(2036,plain,
% 70.49/70.53 (~E(a2,a249)),
% 70.49/70.53 inference(scs_inference,[],[880,1998,441,51,458,368,241,322,151,423,422,417,436,20])).
% 70.49/70.53 cnf(2072,plain,
% 70.49/70.53 (P3(a254,a2)),
% 70.49/70.53 inference(scs_inference,[],[913,51,458,369,243,349,153,423,422,436,417])).
% 70.49/70.53 cnf(2074,plain,
% 70.49/70.53 (~E(a2,a252)),
% 70.49/70.53 inference(scs_inference,[],[913,2032,441,51,458,369,243,349,153,423,422,436,417,20])).
% 70.49/70.53 cnf(2075,plain,
% 70.49/70.53 (~P3(x20751,x20751)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(2079,plain,
% 70.49/70.53 (~P3(x20791,x20791)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(2086,plain,
% 70.49/70.53 (~P3(a2,a254)),
% 70.49/70.53 inference(scs_inference,[],[407,913,2032,441,2075,2079,51,458,369,243,244,155,349,153,423,422,436,417,20,19,418,430,419,414])).
% 70.49/70.53 cnf(2107,plain,
% 70.49/70.53 (P3(a256,a2)),
% 70.49/70.53 inference(scs_inference,[],[952,51,458,245,155,423,422,417])).
% 70.49/70.53 cnf(2111,plain,
% 70.49/70.53 (~E(a2,a254)),
% 70.49/70.53 inference(scs_inference,[],[952,2072,441,51,458,370,245,358,155,423,422,417,436,20])).
% 70.49/70.53 cnf(2147,plain,
% 70.49/70.53 (P3(a258,a2)),
% 70.49/70.53 inference(scs_inference,[],[2107,51,458,377,247,157,423,422,436,417])).
% 70.49/70.53 cnf(2185,plain,
% 70.49/70.53 (P3(a260,a2)),
% 70.49/70.53 inference(scs_inference,[],[2147,51,458,378,249,350,159,423,422,436,417])).
% 70.49/70.53 cnf(2222,plain,
% 70.49/70.53 (P3(a156,a2)),
% 70.49/70.53 inference(scs_inference,[],[2185,51,458,379,297,359,269,423,422,436,417])).
% 70.49/70.53 cnf(2256,plain,
% 70.49/70.53 (P6(f3(a2),f3(a98),f3(a2),f3(a98))),
% 70.49/70.53 inference(scs_inference,[],[2222,458,387,296,268,423,422,436])).
% 70.49/70.53 cnf(2258,plain,
% 70.49/70.53 (P3(a155,a2)),
% 70.49/70.53 inference(scs_inference,[],[2222,51,458,387,296,268,423,422,436,417])).
% 70.49/70.53 cnf(2293,plain,
% 70.49/70.53 (P3(a154,a2)),
% 70.49/70.53 inference(scs_inference,[],[2258,51,458,388,295,351,267,423,422,436,417])).
% 70.49/70.53 cnf(2328,plain,
% 70.49/70.53 (P6(f3(a2),f3(a109),f3(a2),f3(a109))),
% 70.49/70.53 inference(scs_inference,[],[2293,458,397,284,256,423,422,436])).
% 70.49/70.53 cnf(2330,plain,
% 70.49/70.53 (P3(a142,a2)),
% 70.49/70.53 inference(scs_inference,[],[2293,51,458,397,284,256,423,422,436,417])).
% 70.49/70.53 cnf(2366,plain,
% 70.49/70.53 (P3(a164,a2)),
% 70.49/70.53 inference(scs_inference,[],[2330,51,458,304,352,276,320,423,422,436,417])).
% 70.49/70.53 cnf(2403,plain,
% 70.49/70.53 (P3(a152,a2)),
% 70.49/70.53 inference(scs_inference,[],[2366,51,458,293,360,265,348,423,422,436,417])).
% 70.49/70.53 cnf(2440,plain,
% 70.49/70.53 (P3(a140,a2)),
% 70.49/70.53 inference(scs_inference,[],[2403,51,458,282,361,254,357,423,422,436,417])).
% 70.49/70.53 cnf(2478,plain,
% 70.49/70.53 (P3(a162,a2)),
% 70.49/70.53 inference(scs_inference,[],[2440,51,458,302,367,368,274,423,422,436,417])).
% 70.49/70.53 cnf(2514,plain,
% 70.49/70.53 (P3(a150,a2)),
% 70.49/70.53 inference(scs_inference,[],[2478,51,458,291,369,263,340,423,422,436,417])).
% 70.49/70.53 cnf(2550,plain,
% 70.49/70.53 (P3(a138,a2)),
% 70.49/70.53 inference(scs_inference,[],[2514,51,458,280,370,252,313,423,422,436,417])).
% 70.49/70.53 cnf(2588,plain,
% 70.49/70.53 (P3(a160,a2)),
% 70.49/70.53 inference(scs_inference,[],[2550,51,458,300,377,378,272,423,422,436,417])).
% 70.49/70.53 cnf(2624,plain,
% 70.49/70.53 (P3(a148,a2)),
% 70.49/70.53 inference(scs_inference,[],[2588,51,458,289,379,261,314,423,422,436,417])).
% 70.49/70.53 cnf(2659,plain,
% 70.49/70.53 (P3(a136,a2)),
% 70.49/70.53 inference(scs_inference,[],[2624,51,458,278,387,388,250,423,422,436,417])).
% 70.49/70.53 cnf(2693,plain,
% 70.49/70.53 (P3(a158,a2)),
% 70.49/70.53 inference(scs_inference,[],[2659,51,458,298,270,342,328,423,422,436,417])).
% 70.49/70.53 cnf(2722,plain,
% 70.49/70.53 (P10(a43,a173,a2)),
% 70.49/70.53 inference(scs_inference,[],[2693,458,54,63,423,422])).
% 70.49/70.53 cnf(2726,plain,
% 70.49/70.53 (P3(a173,a2)),
% 70.49/70.53 inference(scs_inference,[],[2693,51,458,54,63,333,309,423,422,436,417])).
% 70.49/70.53 cnf(2732,plain,
% 70.49/70.53 (P10(a173,a43,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,2693,441,51,458,54,63,333,309,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(2751,plain,
% 70.49/70.53 (P10(a65,a195,a2)),
% 70.49/70.53 inference(scs_inference,[],[2726,458,56,65,423,422])).
% 70.49/70.53 cnf(2755,plain,
% 70.49/70.53 (P3(a195,a2)),
% 70.49/70.53 inference(scs_inference,[],[2726,51,458,56,65,332,327,423,422,436,417])).
% 70.49/70.53 cnf(2761,plain,
% 70.49/70.53 (P10(a195,a65,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,2726,441,51,458,56,65,332,327,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(2763,plain,
% 70.49/70.53 (~P3(a2,a195)),
% 70.49/70.53 inference(scs_inference,[],[407,2726,441,51,458,56,65,332,327,423,422,436,417,20,19,430,414])).
% 70.49/70.53 cnf(2786,plain,
% 70.49/70.53 (P3(a217,a2)),
% 70.49/70.53 inference(scs_inference,[],[2755,51,458,58,67,343,337,423,422,436,417])).
% 70.49/70.53 cnf(2790,plain,
% 70.49/70.53 (~E(a217,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,2755,441,51,458,58,67,343,337,423,422,436,417,20,19])).
% 70.49/70.53 cnf(2792,plain,
% 70.49/70.53 (P10(a217,a87,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,2755,441,51,458,58,67,343,337,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(2815,plain,
% 70.49/70.53 (P3(a239,a2)),
% 70.49/70.53 inference(scs_inference,[],[2786,51,458,60,69,349,329,423,422,436,417])).
% 70.49/70.53 cnf(2823,plain,
% 70.49/70.53 (~P3(a2,a239)),
% 70.49/70.53 inference(scs_inference,[],[407,2786,441,51,458,60,69,349,329,423,422,436,417,20,19,430,414])).
% 70.49/70.53 cnf(2845,plain,
% 70.49/70.53 (P3(a135,a2)),
% 70.49/70.53 inference(scs_inference,[],[2815,51,458,71,161,351,338,423,422,436,417])).
% 70.49/70.53 cnf(2849,plain,
% 70.49/70.53 (~E(a135,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,2815,441,51,458,71,161,351,338,423,422,436,417,20,19])).
% 70.49/70.53 cnf(2877,plain,
% 70.49/70.53 (P3(a167,a2)),
% 70.49/70.53 inference(scs_inference,[],[2845,51,458,74,164,350,347,423,422,436,417])).
% 70.49/70.53 cnf(2908,plain,
% 70.49/70.53 (P3(a170,a2)),
% 70.49/70.53 inference(scs_inference,[],[2877,51,458,77,167,358,321,423,422,436,417])).
% 70.49/70.53 cnf(2940,plain,
% 70.49/70.53 (P3(a171,a2)),
% 70.49/70.53 inference(scs_inference,[],[2908,51,458,78,168,359,339,423,422,436,417])).
% 70.49/70.53 cnf(2971,plain,
% 70.49/70.53 (P3(a174,a2)),
% 70.49/70.53 inference(scs_inference,[],[2940,51,458,80,170,361,330,423,422,436,417])).
% 70.49/70.53 cnf(3001,plain,
% 70.49/70.53 (P3(a176,a2)),
% 70.49/70.53 inference(scs_inference,[],[2971,51,458,82,172,360,312,423,422,436,417])).
% 70.49/70.53 cnf(3032,plain,
% 70.49/70.53 (P3(a178,a2)),
% 70.49/70.53 inference(scs_inference,[],[3001,51,458,84,174,322,369,423,422,436,417])).
% 70.49/70.53 cnf(3062,plain,
% 70.49/70.53 (P3(a180,a2)),
% 70.49/70.53 inference(scs_inference,[],[3032,51,458,86,176,367,370,423,422,436,417])).
% 70.49/70.53 cnf(3091,plain,
% 70.49/70.53 (P3(a182,a2)),
% 70.49/70.53 inference(scs_inference,[],[3062,51,458,88,178,368,331,423,422,436,417])).
% 70.49/70.53 cnf(3120,plain,
% 70.49/70.53 (P3(a185,a2)),
% 70.49/70.53 inference(scs_inference,[],[3091,51,458,90,180,377,379,423,422,436,417])).
% 70.49/70.53 cnf(3151,plain,
% 70.49/70.53 (P3(a187,a2)),
% 70.49/70.53 inference(scs_inference,[],[3120,51,458,92,182,378,323,423,422,436,417])).
% 70.49/70.53 cnf(3177,plain,
% 70.49/70.53 (P10(a59,a189,a2)),
% 70.49/70.53 inference(scs_inference,[],[3151,458,94,184,423,422])).
% 70.49/70.53 cnf(3181,plain,
% 70.49/70.53 (P3(a189,a2)),
% 70.49/70.53 inference(scs_inference,[],[3151,51,458,94,184,325,317,423,422,436,417])).
% 70.49/70.53 cnf(3185,plain,
% 70.49/70.53 (~E(a189,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3151,441,51,458,94,184,325,317,423,422,436,417,20,19])).
% 70.49/70.53 cnf(3187,plain,
% 70.49/70.53 (P10(a189,a59,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3151,441,51,458,94,184,325,317,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3209,plain,
% 70.49/70.53 (P3(a191,a2)),
% 70.49/70.53 inference(scs_inference,[],[3181,51,458,96,186,324,308,423,422,436,417])).
% 70.49/70.53 cnf(3232,plain,
% 70.49/70.53 (P3(a193,a2)),
% 70.49/70.53 inference(scs_inference,[],[3209,51,458,98,188,340,310,423,422,436,417])).
% 70.49/70.53 cnf(3258,plain,
% 70.49/70.53 (P10(a66,a196,a2)),
% 70.49/70.53 inference(scs_inference,[],[3232,458,100,190,423,422])).
% 70.49/70.53 cnf(3262,plain,
% 70.49/70.53 (P3(a196,a2)),
% 70.49/70.53 inference(scs_inference,[],[3232,51,458,100,190,342,319,423,422,436,417])).
% 70.49/70.53 cnf(3266,plain,
% 70.49/70.53 (~E(a196,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3232,441,51,458,100,190,342,319,423,422,436,417,20,19])).
% 70.49/70.53 cnf(3291,plain,
% 70.49/70.53 (P3(a198,a2)),
% 70.49/70.53 inference(scs_inference,[],[3262,51,458,102,192,332,318,423,422,436,417])).
% 70.49/70.53 cnf(3308,plain,
% 70.49/70.53 (P10(a70,a200,a2)),
% 70.49/70.53 inference(scs_inference,[],[3291,458,104,194,423,422])).
% 70.49/70.53 cnf(3312,plain,
% 70.49/70.53 (P3(a200,a2)),
% 70.49/70.53 inference(scs_inference,[],[3291,51,458,104,194,343,328,423,422,436,417])).
% 70.49/70.53 cnf(3318,plain,
% 70.49/70.53 (P10(a200,a70,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3291,441,51,458,104,194,343,328,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3336,plain,
% 70.49/70.53 (P10(a72,a202,a2)),
% 70.49/70.53 inference(scs_inference,[],[3312,458,106,196,423,422])).
% 70.49/70.53 cnf(3340,plain,
% 70.49/70.53 (P3(a202,a2)),
% 70.49/70.53 inference(scs_inference,[],[3312,51,458,106,196,348,311,423,422,436,417])).
% 70.49/70.53 cnf(3344,plain,
% 70.49/70.53 (~E(a202,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3312,441,51,458,106,196,348,311,423,422,436,417,20,19])).
% 70.49/70.53 cnf(3364,plain,
% 70.49/70.53 (P10(a74,a204,a2)),
% 70.49/70.53 inference(scs_inference,[],[3340,458,108,198,423,422])).
% 70.49/70.53 cnf(3368,plain,
% 70.49/70.53 (P3(a204,a2)),
% 70.49/70.53 inference(scs_inference,[],[3340,51,458,108,198,349,320,423,422,436,417])).
% 70.49/70.53 cnf(3372,plain,
% 70.49/70.53 (~E(a204,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3340,441,51,458,108,198,349,320,423,422,436,417,20,19])).
% 70.49/70.53 cnf(3374,plain,
% 70.49/70.53 (P10(a204,a74,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3340,441,51,458,108,198,349,320,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3392,plain,
% 70.49/70.53 (P10(a77,a207,a2)),
% 70.49/70.53 inference(scs_inference,[],[3368,458,110,200,423,422])).
% 70.49/70.53 cnf(3396,plain,
% 70.49/70.53 (P3(a207,a2)),
% 70.49/70.53 inference(scs_inference,[],[3368,51,458,110,200,352,329,423,422,436,417])).
% 70.49/70.53 cnf(3398,plain,
% 70.49/70.53 (~E(a207,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3368,51,458,110,200,352,329,423,422,436,417,19])).
% 70.49/70.53 cnf(3424,plain,
% 70.49/70.53 (P3(a209,a2)),
% 70.49/70.53 inference(scs_inference,[],[3396,51,458,112,202,352,338,423,422,436,417])).
% 70.49/70.53 cnf(3452,plain,
% 70.49/70.53 (P3(a211,a2)),
% 70.49/70.53 inference(scs_inference,[],[3424,51,458,114,204,357,358,423,422,436,417])).
% 70.49/70.53 cnf(3472,plain,
% 70.49/70.53 (P3(a213,a2)),
% 70.49/70.53 inference(scs_inference,[],[3452,51,458,116,206,359,321,423,422,436,417])).
% 70.49/70.53 cnf(3478,plain,
% 70.49/70.53 (P10(a213,a83,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3452,441,51,458,116,206,359,321,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3500,plain,
% 70.49/70.53 (P3(a215,a2)),
% 70.49/70.53 inference(scs_inference,[],[3472,51,458,118,208,360,339,423,422,436,417])).
% 70.49/70.53 cnf(3524,plain,
% 70.49/70.53 (P10(a88,a218,a2)),
% 70.49/70.53 inference(scs_inference,[],[3500,458,120,210,423,422])).
% 70.49/70.53 cnf(3528,plain,
% 70.49/70.53 (P3(a218,a2)),
% 70.49/70.53 inference(scs_inference,[],[3500,51,458,120,210,313,368,423,422,436,417])).
% 70.49/70.53 cnf(3532,plain,
% 70.49/70.53 (~E(a218,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3500,441,51,458,120,210,313,368,423,422,436,417,20,19])).
% 70.49/70.53 cnf(3534,plain,
% 70.49/70.53 (P10(a218,a88,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3500,441,51,458,120,210,313,368,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3557,plain,
% 70.49/70.53 (P3(a220,a2)),
% 70.49/70.53 inference(scs_inference,[],[3528,51,458,122,212,322,370,423,422,436,417])).
% 70.49/70.53 cnf(3563,plain,
% 70.49/70.53 (P10(a220,a90,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3528,441,51,458,122,212,322,370,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3585,plain,
% 70.49/70.53 (P3(a222,a2)),
% 70.49/70.53 inference(scs_inference,[],[3557,51,458,124,214,367,369,423,422,436,417])).
% 70.49/70.53 cnf(3613,plain,
% 70.49/70.53 (P3(a224,a2)),
% 70.49/70.53 inference(scs_inference,[],[3585,51,458,126,216,314,378,423,422,436,417])).
% 70.49/70.53 cnf(3617,plain,
% 70.49/70.53 (~E(a224,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,3585,441,51,458,126,216,314,378,423,422,436,417,20,19])).
% 70.49/70.53 cnf(3619,plain,
% 70.49/70.53 (P10(a224,a94,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3585,441,51,458,126,216,314,378,423,422,436,417,20,19,430])).
% 70.49/70.53 cnf(3643,plain,
% 70.49/70.53 (P3(a226,a2)),
% 70.49/70.53 inference(scs_inference,[],[3613,51,458,128,218,350,379,423,422,436,417])).
% 70.49/70.53 cnf(3649,plain,
% 70.49/70.53 (P10(a226,a96,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,3613,441,51,458,128,218,350,379,423,422,436,417,19,20,430])).
% 70.49/70.53 cnf(3672,plain,
% 70.49/70.53 (P3(a229,a2)),
% 70.49/70.53 inference(scs_inference,[],[3643,51,458,130,220,334,309,423,422,436,417])).
% 70.49/70.53 cnf(3699,plain,
% 70.49/70.53 (P6(f3(a76),f3(a1),f3(a2),f3(a87))),
% 70.49/70.53 inference(scs_inference,[],[3672,458,132,222,323,317,423,422,436])).
% 70.49/70.53 cnf(4139,plain,
% 70.49/70.53 (P3(a165,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,305,417])).
% 70.49/70.53 cnf(4170,plain,
% 70.49/70.53 (P10(a24,a153,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,266,294,417,422])).
% 70.49/70.53 cnf(4179,plain,
% 70.49/70.53 (~P3(x41791,x41791)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(4180,plain,
% 70.49/70.53 (P10(a153,a24,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,4139,441,51,458,266,294,313,369,417,422,423,436,19,20,430])).
% 70.49/70.53 cnf(4184,plain,
% 70.49/70.53 (P9(x41841,f120(f250(f3(a76),f250(f3(a1),f3(a1)))))+~E(a24,x41841)),
% 70.49/70.53 inference(scs_inference,[],[407,4139,441,51,458,266,294,313,369,417,422,423,436,19,20,430,414,26])).
% 70.49/70.53 cnf(4185,plain,
% 70.49/70.53 (~E(a24,a2)+~P8(f3(a2),f250(f3(a76),f250(f3(a1),f3(a1))))),
% 70.49/70.53 inference(scs_inference,[],[407,4139,441,4179,51,458,266,294,313,369,417,422,423,436,19,20,430,414,26,419])).
% 70.49/70.53 cnf(4271,plain,
% 70.49/70.53 (P3(a139,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,281,417])).
% 70.49/70.53 cnf(4306,plain,
% 70.49/70.53 (P10(a161,a32,a2)),
% 70.49/70.53 inference(scs_inference,[],[407,4271,441,51,458,273,301,342,337,422,417,423,436,19,20,430])).
% 70.49/70.53 cnf(4313,plain,
% 70.49/70.53 (P9(x43131,f120(f250(f3(a43),f250(f3(a4),f3(a1)))))+~E(a32,x43131)),
% 70.49/70.53 inference(scs_inference,[],[407,4271,441,51,458,273,301,3699,382,342,337,422,417,423,436,19,20,430,414,15,13,16,26])).
% 70.49/70.53 cnf(4396,plain,
% 70.49/70.53 (P3(a147,a2)),
% 70.49/70.53 inference(scs_inference,[],[51,288,417])).
% 70.49/70.53 cnf(4427,plain,
% 70.49/70.53 (P3(a166,a2)),
% 70.49/70.53 inference(scs_inference,[],[4396,51,458,306,423,417])).
% 70.49/70.53 cnf(4450,plain,
% 70.49/70.53 (P3(a133,a2)),
% 70.49/70.53 inference(scs_inference,[],[4427,51,458,62,423,417])).
% 70.49/70.53 cnf(4454,plain,
% 70.49/70.53 (~E(a2,a166)),
% 70.49/70.53 inference(scs_inference,[],[4427,441,51,458,62,312,359,423,417,436,20])).
% 70.49/70.53 cnf(4456,plain,
% 70.49/70.53 (~P3(a2,a133)),
% 70.49/70.53 inference(scs_inference,[],[4427,441,51,458,62,312,359,423,417,436,20,414])).
% 70.49/70.53 cnf(4476,plain,
% 70.49/70.53 (~P3(a4,a192)),
% 70.49/70.53 inference(scs_inference,[],[4450,441,187,53,339,328,417,436,20,414])).
% 70.49/70.53 cnf(4548,plain,
% 70.49/70.53 (P3(a208,a75)),
% 70.49/70.53 inference(scs_inference,[],[201,109,417])).
% 70.49/70.53 cnf(4573,plain,
% 70.49/70.53 (~E(a75,a208)),
% 70.49/70.53 inference(scs_inference,[],[4548,441,211,111,338,310,417,436,20])).
% 70.49/70.53 cnf(4586,plain,
% 70.49/70.53 (P3(a223,a89)),
% 70.49/70.53 inference(scs_inference,[],[215,121,417])).
% 70.49/70.53 cnf(4607,plain,
% 70.49/70.53 (P3(a225,a93)),
% 70.49/70.53 inference(scs_inference,[],[217,125,417])).
% 70.49/70.53 cnf(4611,plain,
% 70.49/70.53 (~E(a89,a223)),
% 70.49/70.53 inference(scs_inference,[],[4586,441,217,125,328,327,417,436,20])).
% 70.49/70.53 cnf(4627,plain,
% 70.49/70.53 (P3(a227,a95)),
% 70.49/70.53 inference(scs_inference,[],[219,127,417])).
% 70.49/70.53 cnf(4631,plain,
% 70.49/70.53 (~E(a93,a225)),
% 70.49/70.53 inference(scs_inference,[],[4607,441,219,127,330,318,417,436,20])).
% 70.49/70.53 cnf(4649,plain,
% 70.49/70.53 (P7(f3(a4))),
% 70.49/70.53 inference(scs_inference,[],[4627,34,412,410])).
% 70.49/70.53 cnf(4653,plain,
% 70.49/70.53 (P7(f250(f3(x46531),f250(f3(x46532),f3(a1))))),
% 70.49/70.53 inference(scs_inference,[],[1338,4627,34,1474,412,410,426,415])).
% 70.49/70.53 cnf(4655,plain,
% 70.49/70.53 (P8(f250(f3(x46551),f3(a87)),f250(f3(x46552),f3(a98)))),
% 70.49/70.53 inference(scs_inference,[],[1338,4627,34,1474,49,412,410,426,415,421])).
% 70.49/70.53 cnf(4657,plain,
% 70.49/70.53 (P8(f3(x46571),f250(f3(x46572),f250(f3(x46573),f3(a1))))),
% 70.49/70.53 inference(scs_inference,[],[1338,4627,34,1474,49,412,410,426,415,421,416])).
% 70.49/70.53 cnf(4659,plain,
% 70.49/70.53 (~E(a95,a227)),
% 70.49/70.53 inference(scs_inference,[],[1338,4627,34,1474,49,412,410,426,415,421,416,409])).
% 70.49/70.53 cnf(4661,plain,
% 70.49/70.53 (~E(a17,a184)),
% 70.49/70.53 inference(scs_inference,[],[527,1338,4627,34,1474,49,412,410,426,415,421,416,409,2])).
% 70.49/70.53 cnf(4662,plain,
% 70.49/70.53 (~P10(a223,a219,a2)),
% 70.49/70.53 inference(scs_inference,[],[527,1338,1475,4627,4611,34,1474,49,412,410,426,415,421,416,409,2,429])).
% 70.49/70.53 cnf(4672,plain,
% 70.49/70.53 (P8(f3(a76),f3(a98))),
% 70.49/70.53 inference(scs_inference,[],[469,527,1348,1338,1475,4627,4611,34,1474,113,49,48,412,410,426,415,421,416,409,2,429,428,427,424,422,420])).
% 70.49/70.53 cnf(4674,plain,
% 70.49/70.53 (P3(a184,a17)),
% 70.49/70.53 inference(scs_inference,[],[407,469,527,1348,1338,1475,4627,4611,34,1474,113,49,48,412,410,426,415,421,416,409,2,429,428,427,424,422,420,411])).
% 70.49/70.53 cnf(4680,plain,
% 70.49/70.53 (~P5(a4,a133)),
% 70.49/70.53 inference(scs_inference,[],[407,469,527,491,1348,1338,1475,4627,4611,34,515,503,1474,72,113,49,48,44,42,412,410,426,415,421,416,409,2,429,428,427,424,422,420,411,22,21,27,413])).
% 70.49/70.53 cnf(4682,plain,
% 70.49/70.53 (~E(a133,a4)),
% 70.49/70.53 inference(scs_inference,[],[407,469,527,491,1348,1338,1475,4627,4611,34,515,503,1474,72,113,49,48,44,42,440,412,410,426,415,421,416,409,2,429,428,427,424,422,420,411,22,21,27,413,28])).
% 70.49/70.53 cnf(4684,plain,
% 70.49/70.53 (~P9(a230,f120(x46841))),
% 70.49/70.53 inference(scs_inference,[],[407,469,527,491,1348,1338,1475,4627,4611,34,515,503,1474,72,113,221,49,48,44,42,440,441,412,410,426,415,421,416,409,2,429,428,427,424,422,420,411,22,21,27,413,28,417])).
% 70.49/70.53 cnf(4685,plain,
% 70.49/70.53 (~P3(x46851,x46851)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(4690,plain,
% 70.49/70.53 (P6(f3(a2),f3(a2),f3(a109),f3(a109))),
% 70.49/70.53 inference(scs_inference,[],[407,469,527,491,1348,1338,1475,1552,4627,4611,34,515,503,1474,663,316,397,52,72,113,221,49,48,44,42,440,441,412,410,426,415,421,416,409,2,429,428,427,424,422,420,411,22,21,27,413,28,417,24,26,23,436])).
% 70.49/70.53 cnf(4693,plain,
% 70.49/70.53 (~P3(x46931,x46931)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(4697,plain,
% 70.49/70.53 (~P3(x46971,x46971)),
% 70.49/70.53 inference(rename_variables,[],[441])).
% 70.49/70.53 cnf(4704,plain,
% 70.49/70.53 (P10(a1,a2,a1)),
% 70.49/70.53 inference(scs_inference,[],[407,469,527,491,1348,1338,1475,1552,4627,4611,34,515,503,1474,663,399,316,397,52,72,785,113,221,231,49,48,308,44,43,42,440,441,4685,4693,4697,51,412,410,426,415,421,416,409,2,429,428,427,424,422,420,411,22,21,27,413,28,417,24,26,23,436,19,437,419,418,423,431])).
% 70.49/70.53 cnf(4707,plain,
% 70.49/70.53 (~E(a24,a2)),
% 70.49/70.53 inference(scs_inference,[],[4657,4185])).
% 70.49/70.53 cnf(4709,plain,
% 70.49/70.53 (~P9(a230,f120(x47091))),
% 70.49/70.53 inference(rename_variables,[],[4684])).
% 70.49/70.53 cnf(4710,plain,
% 70.49/70.53 (~E(a24,a230)),
% 70.49/70.53 inference(scs_inference,[],[4684,4709,731,4184])).
% 70.49/70.53 cnf(4711,plain,
% 70.49/70.53 (~P9(a230,f120(x47111))),
% 70.49/70.53 inference(rename_variables,[],[4684])).
% 70.49/70.53 cnf(4712,plain,
% 70.49/70.53 (~E(a32,a230)),
% 70.49/70.53 inference(scs_inference,[],[4684,4709,4711,731,4184,4313])).
% 70.49/70.53 cnf(4716,plain,
% 70.49/70.53 (P8(f250(f3(x47161),f3(a76)),f250(f3(x47162),f3(a98)))),
% 70.49/70.53 inference(scs_inference,[],[4674,4672,4684,4709,4711,731,4184,4313,412,421])).
% 70.49/70.53 cnf(4718,plain,
% 70.49/70.54 (P7(f3(a43))),
% 70.49/70.54 inference(scs_inference,[],[4674,4672,4684,4709,4711,35,731,4184,4313,412,421,410])).
% 70.49/70.54 cnf(4722,plain,
% 70.49/70.54 (P7(f250(f3(x47221),f3(a4)))),
% 70.49/70.54 inference(scs_inference,[],[3177,4674,4649,4672,4684,4709,4711,35,731,4184,4313,412,421,410,426,415])).
% 70.49/70.54 cnf(4724,plain,
% 70.49/70.54 (P8(f3(x47241),f250(f3(x47242),f3(a4)))),
% 70.49/70.54 inference(scs_inference,[],[3177,4674,4649,4672,4684,4709,4711,35,731,4184,4313,412,421,410,426,415,416])).
% 70.49/70.54 cnf(4726,plain,
% 70.49/70.54 (~E(a17,a192)),
% 70.49/70.54 inference(scs_inference,[],[1087,3177,4674,4649,4672,4684,4709,4711,35,731,4184,4313,412,421,410,426,415,416,2])).
% 70.49/70.54 cnf(4727,plain,
% 70.49/70.54 (~P10(a2,a2,a1)),
% 70.49/70.54 inference(scs_inference,[],[481,1087,3177,4674,4704,4649,4672,4684,4709,4711,35,731,4184,4313,412,421,410,426,415,416,2,429])).
% 70.49/70.54 cnf(4731,plain,
% 70.49/70.54 (~P10(a1,a2,a2)),
% 70.49/70.54 inference(scs_inference,[],[481,1087,3177,4674,4704,4649,4672,4684,4709,4711,35,458,731,4184,4313,412,421,410,426,415,416,2,429,428,427])).
% 70.49/70.54 cnf(4733,plain,
% 70.49/70.54 (P8(f250(f3(a76),f3(a4)),f250(f3(a98),f3(a4)))),
% 70.49/70.54 inference(scs_inference,[],[481,1087,3177,4674,4704,4649,4672,4684,4709,4711,35,458,731,4184,4313,412,421,410,426,415,416,2,429,428,427,424])).
% 70.49/70.54 cnf(4737,plain,
% 70.49/70.54 (P3(a192,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,481,1087,3177,4662,4674,4704,4649,4672,4684,4709,4711,35,211,458,731,4184,4313,412,421,410,426,415,416,2,429,428,427,424,422,411])).
% 70.49/70.54 cnf(4738,plain,
% 70.49/70.54 (~P3(a17,x47381)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(4740,plain,
% 70.49/70.54 (P8(f3(a76),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,481,1087,3177,4662,4674,4704,4649,4672,4684,4709,4711,35,211,50,458,731,4184,4313,412,421,410,426,415,416,2,429,428,427,424,422,411,420])).
% 70.49/70.54 cnf(4743,plain,
% 70.49/70.54 (~P3(a17,x47431)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(4746,plain,
% 70.49/70.54 (~P3(a17,x47461)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(4757,plain,
% 70.49/70.54 (~P10(a2,a121,a2)),
% 70.49/70.54 inference(scs_inference,[],[407,4738,4743,4746,481,1087,3177,4661,4662,4674,4680,4704,4649,4672,4684,4709,4711,35,567,400,388,71,59,61,66,211,308,50,458,51,731,4184,4313,412,421,410,426,415,416,2,429,428,427,424,422,411,420,413,417,437,419,418,423,430])).
% 70.49/70.54 cnf(4765,plain,
% 70.49/70.54 (P7(f3(a54))),
% 70.49/70.54 inference(scs_inference,[],[4737,36,412,410])).
% 70.49/70.54 cnf(4769,plain,
% 70.49/70.54 (P7(f250(f3(x47691),f3(a43)))),
% 70.49/70.54 inference(scs_inference,[],[4737,4718,4740,36,412,410,421,415])).
% 70.49/70.54 cnf(4773,plain,
% 70.49/70.54 (P8(f3(x47731),f250(f3(x47732),f3(a43)))),
% 70.49/70.54 inference(scs_inference,[],[3258,4737,4718,4740,36,412,410,421,415,426,416])).
% 70.49/70.54 cnf(4776,plain,
% 70.49/70.54 (~P10(a66,a17,a2)),
% 70.49/70.54 inference(scs_inference,[],[4707,3266,3258,4737,4718,4740,36,412,410,421,415,426,416,2,428])).
% 70.49/70.54 cnf(4778,plain,
% 70.49/70.54 (~P10(a225,a223,a2)),
% 70.49/70.54 inference(scs_inference,[],[4707,3266,3258,1540,4631,4737,4718,4740,36,412,410,421,415,426,416,2,428,429])).
% 70.49/70.54 cnf(4782,plain,
% 70.49/70.54 (P8(f250(f3(a76),f3(a43)),f250(f3(a109),f3(a43)))),
% 70.49/70.54 inference(scs_inference,[],[4707,3266,657,3258,1540,4631,4737,4718,4740,36,412,410,421,415,426,416,2,428,429,427,424])).
% 70.49/70.54 cnf(4788,plain,
% 70.49/70.54 (P3(a206,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,4707,557,3266,657,3258,1540,4631,4731,4737,4718,4740,36,4450,52,458,412,410,421,415,426,416,2,428,429,427,424,422,423,411])).
% 70.49/70.54 cnf(4791,plain,
% 70.49/70.54 (P8(f3(a87),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,4707,557,3266,657,3258,1540,4631,4731,4737,4718,4740,36,4450,52,49,50,458,412,410,421,415,426,416,2,428,429,427,424,422,423,411,420])).
% 70.49/70.54 cnf(4795,plain,
% 70.49/70.54 (~P9(a232,f120(x47951))),
% 70.49/70.54 inference(scs_inference,[],[407,4707,557,3266,657,3258,1540,4631,4731,4737,4718,4740,36,671,4450,223,52,49,50,458,441,412,410,421,415,426,416,2,428,429,427,424,422,423,411,420,413,417])).
% 70.49/70.54 cnf(4796,plain,
% 70.49/70.54 (~P3(x47961,x47961)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(4801,plain,
% 70.49/70.54 (~P3(x48011,x48011)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(4806,plain,
% 70.49/70.54 (P10(a2,a109,a109)),
% 70.49/70.54 inference(scs_inference,[],[407,4707,557,3266,657,3258,1540,4631,4731,4737,4690,4718,4740,36,671,4450,402,60,57,223,351,52,69,49,317,50,458,441,4796,4801,51,412,410,421,415,426,416,2,428,429,427,424,422,423,411,420,413,417,437,419,418,431])).
% 70.49/70.54 cnf(4810,plain,
% 70.49/70.54 (~E(a17,a206)),
% 70.49/70.54 inference(scs_inference,[],[407,4707,557,3266,657,3258,1540,4631,4731,4737,4690,4718,4740,36,671,4450,402,60,57,223,351,52,69,49,317,50,458,441,4796,4801,51,412,410,421,415,426,416,2,428,429,427,424,422,423,411,420,413,417,437,419,418,431,540,731,409])).
% 70.49/70.54 cnf(4817,plain,
% 70.49/70.54 (~E(a24,a232)),
% 70.49/70.54 inference(scs_inference,[],[4795,4184])).
% 70.49/70.54 cnf(4818,plain,
% 70.49/70.54 (~P9(a232,f120(x48181))),
% 70.49/70.54 inference(rename_variables,[],[4795])).
% 70.49/70.54 cnf(4823,plain,
% 70.49/70.54 (P7(f3(a65))),
% 70.49/70.54 inference(scs_inference,[],[4788,4795,4818,37,4184,412,4313,410])).
% 70.49/70.54 cnf(4825,plain,
% 70.49/70.54 (P7(f250(f3(x48251),f3(a54)))),
% 70.49/70.54 inference(scs_inference,[],[4788,4765,4795,4818,37,4184,412,4313,410,415])).
% 70.49/70.54 cnf(4831,plain,
% 70.49/70.54 (P8(f3(x48311),f250(f3(x48312),f3(a54)))),
% 70.49/70.54 inference(scs_inference,[],[3308,4788,4765,4791,4795,4818,37,4184,412,4313,410,415,421,426,416])).
% 70.49/70.54 cnf(4833,plain,
% 70.49/70.54 (~E(a17,a228)),
% 70.49/70.54 inference(scs_inference,[],[594,3308,4788,4765,4791,4795,4818,37,4184,412,4313,410,415,421,426,416,2])).
% 70.49/70.54 cnf(4834,plain,
% 70.49/70.54 (~P10(a133,a1,a2)),
% 70.49/70.54 inference(scs_inference,[],[514,594,3308,4788,4765,4791,4795,4818,37,498,4184,412,4313,410,415,421,426,416,2,428])).
% 70.49/70.54 cnf(4836,plain,
% 70.49/70.54 (~P10(a1,a133,a2)),
% 70.49/70.54 inference(scs_inference,[],[514,594,3308,4788,4765,4791,4795,4818,37,498,486,4184,412,4313,410,415,421,426,416,2,428,429])).
% 70.49/70.54 cnf(4844,plain,
% 70.49/70.54 (P3(a228,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,514,594,3308,4757,4788,4765,4791,4795,4818,37,498,486,4704,51,4184,412,4313,410,415,421,426,416,2,428,429,427,424,422,411])).
% 70.49/70.54 cnf(4845,plain,
% 70.49/70.54 (~P3(a17,x48451)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(4847,plain,
% 70.49/70.54 (P8(f3(a65),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,514,594,3308,4757,4788,4765,4791,4795,4818,37,498,486,4704,4740,47,51,4184,412,4313,410,415,421,426,416,2,428,429,427,424,422,411,420])).
% 70.49/70.54 cnf(4852,plain,
% 70.49/70.54 (~P9(a234,f120(x48521))),
% 70.49/70.54 inference(scs_inference,[],[407,4845,514,594,3308,4726,4757,4788,4765,4791,4795,4818,37,498,486,4704,225,4740,47,441,51,4184,412,4313,410,415,421,426,416,2,428,429,427,424,422,411,420,413,417])).
% 70.49/70.54 cnf(4853,plain,
% 70.49/70.54 (~P3(x48531,x48531)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(4855,plain,
% 70.49/70.54 (P6(f3(a2),f3(a76),f3(a65),f250(f3(a1),f3(a1)))),
% 70.49/70.54 inference(scs_inference,[],[407,4845,514,594,3308,4726,4757,4788,4765,4791,4795,4818,37,498,486,372,4704,225,4740,47,317,441,51,4184,412,4313,410,415,421,426,416,2,428,429,427,424,422,411,420,413,417,437])).
% 70.49/70.54 cnf(4858,plain,
% 70.49/70.54 (~P3(x48581,x48581)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(4864,plain,
% 70.49/70.54 (P10(a109,a2,a109)),
% 70.49/70.54 inference(scs_inference,[],[407,4845,514,594,3308,4726,4757,4788,4765,4791,4795,4818,37,4733,4655,498,2328,486,372,86,4704,225,233,4740,60,47,317,441,4853,4858,51,4184,412,4313,410,415,421,426,416,2,428,429,427,424,422,411,420,413,417,437,418,419,431])).
% 70.49/70.54 cnf(4878,plain,
% 70.49/70.54 (~P9(a234,f120(x48781))),
% 70.49/70.54 inference(rename_variables,[],[4852])).
% 70.49/70.54 cnf(4879,plain,
% 70.49/70.54 (P7(f3(a76))),
% 70.49/70.54 inference(scs_inference,[],[4844,4852,38,412,4184,410])).
% 70.49/70.54 cnf(4883,plain,
% 70.49/70.54 (P7(f250(f3(x48831),f3(a65)))),
% 70.49/70.54 inference(scs_inference,[],[4844,4823,4847,4852,38,412,4184,410,421,415])).
% 70.49/70.54 cnf(4887,plain,
% 70.49/70.54 (P8(f3(x48871),f250(f3(x48872),f3(a65)))),
% 70.49/70.54 inference(scs_inference,[],[4844,4823,4847,4852,4878,38,412,4184,410,421,415,4313,416])).
% 70.49/70.54 cnf(4891,plain,
% 70.49/70.54 (~E(a17,a177)),
% 70.49/70.54 inference(scs_inference,[],[851,3336,4844,4823,4847,4852,4878,38,412,4184,410,421,415,4313,416,426,2])).
% 70.49/70.54 cnf(4894,plain,
% 70.49/70.54 (~P10(a227,a225,a2)),
% 70.49/70.54 inference(scs_inference,[],[851,3344,3336,1569,4659,4844,4823,4847,4852,4878,38,412,4184,410,421,415,4313,416,426,2,428,429])).
% 70.49/70.54 cnf(4902,plain,
% 70.49/70.54 (P3(a177,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,851,3344,715,3336,1569,4659,4836,4844,4823,4847,4852,4878,38,52,412,4184,410,421,415,4313,416,426,2,428,429,427,424,422,411])).
% 70.49/70.54 cnf(4903,plain,
% 70.49/70.54 (~P3(a17,x49031)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(4907,plain,
% 70.49/70.54 (P8(f3(a54),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,851,3344,715,3336,1569,4659,4836,4844,4823,4847,4852,4878,38,978,52,46,458,412,4184,410,421,415,4313,416,426,2,428,429,427,424,422,411,423,420])).
% 70.49/70.54 cnf(4911,plain,
% 70.49/70.54 (~P9(a236,f120(x49111))),
% 70.49/70.54 inference(scs_inference,[],[407,851,3344,715,3336,1569,4659,4836,4844,4823,4847,4852,4878,38,729,978,227,52,46,458,441,412,4184,410,421,415,4313,416,426,2,428,429,427,424,422,411,423,420,413,417])).
% 70.49/70.54 cnf(4926,plain,
% 70.49/70.54 (P10(a206,a195,a135)),
% 70.49/70.54 inference(scs_inference,[],[407,4903,544,851,3344,715,3336,1569,4659,4836,4844,4776,4823,4847,4852,4878,38,4855,2763,729,978,404,100,397,227,72,65,66,161,60,52,46,308,458,441,51,412,4184,410,421,415,4313,416,426,2,428,429,427,424,422,411,423,420,413,417,437,418,419,431,540,731,3,432])).
% 70.49/70.54 cnf(4932,plain,
% 70.49/70.54 (P7(f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[4902,39,412,410])).
% 70.49/70.54 cnf(4936,plain,
% 70.49/70.54 (P7(f250(f3(x49361),f3(a76)))),
% 70.49/70.54 inference(scs_inference,[],[4902,4879,4907,39,412,410,421,415])).
% 70.49/70.54 cnf(4939,plain,
% 70.49/70.54 (~P9(a236,f120(x49391))),
% 70.49/70.54 inference(rename_variables,[],[4911])).
% 70.49/70.54 cnf(4942,plain,
% 70.49/70.54 (P8(f3(x49421),f250(f3(x49422),f3(a76)))),
% 70.49/70.54 inference(scs_inference,[],[4902,4879,4907,4911,4939,39,412,410,421,415,4184,4313,416])).
% 70.49/70.54 cnf(4946,plain,
% 70.49/70.54 (~E(a17,a181)),
% 70.49/70.54 inference(scs_inference,[],[921,3364,4902,4879,4907,4911,4939,39,412,410,421,415,4184,4313,416,426,2])).
% 70.49/70.54 cnf(4949,plain,
% 70.49/70.54 (~P10(a43,a133,a2)),
% 70.49/70.54 inference(scs_inference,[],[581,921,3364,4902,4879,4907,4911,4939,39,498,486,412,410,421,415,4184,4313,416,426,2,428,429])).
% 70.49/70.54 cnf(4955,plain,
% 70.49/70.54 (P3(a181,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,581,973,921,3364,4778,4806,4902,4879,4907,4911,4939,39,498,486,215,412,410,421,415,4184,4313,416,426,2,428,429,427,422,411])).
% 70.49/70.54 cnf(4956,plain,
% 70.49/70.54 (~P3(a17,x49561)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(4960,plain,
% 70.49/70.54 (P8(f3(a43),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,581,973,921,3364,4778,4806,4902,4879,4907,4911,4939,39,498,486,215,45,412,410,421,415,4184,4313,416,426,2,428,429,427,422,411,424,420])).
% 70.49/70.54 cnf(4965,plain,
% 70.49/70.54 (~P9(a238,f120(x49651))),
% 70.49/70.54 inference(scs_inference,[],[407,4956,581,973,921,3364,4810,4778,4806,4902,4879,4907,4911,4939,39,498,486,229,215,45,441,412,410,421,415,4184,4313,416,426,2,428,429,427,422,411,424,420,413,417])).
% 70.49/70.54 cnf(4968,plain,
% 70.49/70.54 (P6(f3(a2),f3(a109),f3(a98),f250(f3(a87),f3(a1)))),
% 70.49/70.54 inference(scs_inference,[],[407,4956,581,973,921,3364,4810,4778,4806,4902,4879,4907,4911,4939,39,498,405,486,377,229,215,317,45,441,412,410,421,415,4184,4313,416,426,2,428,429,427,422,411,424,420,413,417,437])).
% 70.49/70.54 cnf(4990,plain,
% 70.49/70.54 (P7(f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[4955,4960,40,412,421,410])).
% 70.49/70.54 cnf(4992,plain,
% 70.49/70.54 (P7(f250(f3(x49921),f3(a87)))),
% 70.49/70.54 inference(scs_inference,[],[4955,4932,4960,40,412,421,410,415])).
% 70.49/70.54 cnf(4996,plain,
% 70.49/70.54 (P8(f3(x49961),f250(f3(x49962),f3(a87)))),
% 70.49/70.54 inference(scs_inference,[],[3392,4955,4932,4960,40,412,421,410,415,426,416])).
% 70.49/70.54 cnf(4999,plain,
% 70.49/70.54 (~P9(a238,f120(x49991))),
% 70.49/70.54 inference(rename_variables,[],[4965])).
% 70.49/70.54 cnf(5000,plain,
% 70.49/70.54 (~E(a17,a186)),
% 70.49/70.54 inference(scs_inference,[],[984,3392,4955,4932,4960,4965,40,412,421,410,415,426,416,4184,2])).
% 70.49/70.54 cnf(5001,plain,
% 70.49/70.54 (~P10(a77,a17,a2)),
% 70.49/70.54 inference(scs_inference,[],[984,3398,3392,4955,4932,4960,4965,40,412,421,410,415,426,416,4184,2,428])).
% 70.49/70.54 cnf(5003,plain,
% 70.49/70.54 (~P10(a230,a153,a2)),
% 70.49/70.54 inference(scs_inference,[],[984,3398,3392,4170,4710,4955,4932,4960,4965,40,412,421,410,415,426,416,4184,2,428,429])).
% 70.49/70.54 cnf(5007,plain,
% 70.49/70.54 (P3(a186,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4710,4955,4932,4960,4965,40,412,421,410,415,426,416,4184,2,428,429,427,411])).
% 70.49/70.54 cnf(5017,plain,
% 70.49/70.54 (P8(f3(a4),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4949,4710,4955,4932,4960,4965,4999,40,1011,54,229,44,458,412,421,410,415,426,416,4184,2,428,429,427,411,27,423,422,424,420])).
% 70.49/70.54 cnf(5027,plain,
% 70.49/70.54 (P6(f3(a2),f3(a1),f3(a87),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4949,4710,4955,4932,4960,4965,4999,40,4834,826,2722,1011,387,74,54,324,229,44,440,458,412,421,410,415,426,416,4184,2,428,429,427,411,27,423,422,424,420,413,24,28,26,23,436])).
% 70.49/70.54 cnf(5029,plain,
% 70.49/70.54 (~P9(a245,f120(x50291))),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4949,4710,4955,4932,4960,4965,4999,40,4834,826,2722,1011,387,74,54,235,324,229,44,440,458,441,412,421,410,415,426,416,4184,2,428,429,427,411,27,423,422,424,420,413,24,28,26,23,436,417])).
% 70.49/70.54 cnf(5030,plain,
% 70.49/70.54 (~P3(x50301,x50301)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5032,plain,
% 70.49/70.54 (P6(f3(a2),f3(a87),f3(a54),f250(f3(a1),f3(a1)))),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4949,4710,4955,4932,4960,4965,4999,40,4834,826,2722,1011,381,387,74,54,235,324,229,317,44,440,458,441,412,421,410,415,426,416,4184,2,428,429,427,411,27,423,422,424,420,413,24,28,26,23,436,417,437])).
% 70.49/70.54 cnf(5035,plain,
% 70.49/70.54 (~P3(x50351,x50351)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5041,plain,
% 70.49/70.54 (P10(a217,a184,a135)),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4949,4710,4955,4932,4960,4965,4999,40,4716,4834,826,2722,1011,381,387,74,90,54,235,324,64,229,67,161,317,44,440,458,441,5030,5035,412,421,410,415,426,416,4184,2,428,429,427,411,27,423,422,424,420,413,24,28,26,23,436,417,437,418,419,432])).
% 70.49/70.54 cnf(5043,plain,
% 70.49/70.54 (P10(a76,a65,a6)),
% 70.49/70.54 inference(scs_inference,[],[407,984,3398,814,3392,4170,4949,4710,4955,4932,4960,4965,4999,40,4716,4834,826,2722,4855,1011,381,387,74,90,54,56,71,235,324,57,64,229,67,161,317,44,440,458,441,5030,5035,412,421,410,415,426,416,4184,2,428,429,427,411,27,423,422,424,420,413,24,28,26,23,436,417,437,418,419,432,431])).
% 70.49/70.54 cnf(5059,plain,
% 70.49/70.54 (P7(f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[5007,5017,41,412,421,410])).
% 70.49/70.54 cnf(5063,plain,
% 70.49/70.54 (P7(f250(f3(x50631),f3(a98)))),
% 70.49/70.54 inference(scs_inference,[],[3524,5007,4990,5017,41,412,421,410,426,415])).
% 70.49/70.54 cnf(5065,plain,
% 70.49/70.54 (P8(f3(x50651),f250(f3(x50652),f3(a98)))),
% 70.49/70.54 inference(scs_inference,[],[3524,5007,4990,5017,41,412,421,410,426,415,416])).
% 70.49/70.54 cnf(5069,plain,
% 70.49/70.54 (~E(a17,a190)),
% 70.49/70.54 inference(scs_inference,[],[1053,3524,5007,4990,5017,5029,41,412,421,410,426,415,416,4184,2])).
% 70.49/70.54 cnf(5070,plain,
% 70.49/70.54 (~P10(a4,a173,a2)),
% 70.49/70.54 inference(scs_inference,[],[618,1053,3524,5007,4990,5017,5029,41,2722,412,421,410,426,415,416,4184,2,429])).
% 70.49/70.54 cnf(5072,plain,
% 70.49/70.54 (~P10(a173,a4,a2)),
% 70.49/70.54 inference(scs_inference,[],[618,1053,3524,5007,4990,5017,5029,41,2732,2722,412,421,410,426,415,416,4184,2,429,428])).
% 70.49/70.54 cnf(5076,plain,
% 70.49/70.54 (P3(a190,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,618,1008,1053,3524,4864,5007,4990,5017,5029,41,2732,2722,412,421,410,426,415,416,4184,2,429,428,427,411])).
% 70.49/70.54 cnf(5077,plain,
% 70.49/70.54 (~P3(a17,x50771)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5081,plain,
% 70.49/70.54 (P8(f3(a1),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,618,1008,1053,3524,4864,4894,5007,4990,5017,5029,41,2732,2722,217,43,412,421,410,426,415,416,4184,2,429,428,427,411,422,420])).
% 70.49/70.54 cnf(5086,plain,
% 70.49/70.54 (~P3(a17,x50861)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5098,plain,
% 70.49/70.54 (P10(a87,a54,a6)),
% 70.49/70.54 inference(scs_inference,[],[407,5077,5086,618,1008,1053,3524,4833,4864,4894,5007,4990,5017,5029,41,5032,2732,503,2722,392,387,58,237,55,71,62,217,60,308,43,441,412,421,410,426,415,416,4184,2,429,428,427,411,422,420,424,413,417,437,418,419,431])).
% 70.49/70.54 cnf(5111,plain,
% 70.49/70.54 (P7(f3(a1))),
% 70.49/70.54 inference(scs_inference,[],[5076,5081,33,421,412,410])).
% 70.49/70.54 cnf(5113,plain,
% 70.49/70.54 (P7(f250(f3(x51131),f3(a109)))),
% 70.49/70.54 inference(scs_inference,[],[5076,5059,5081,33,421,412,410,415])).
% 70.49/70.54 cnf(5119,plain,
% 70.49/70.54 (~E(a17,a194)),
% 70.49/70.54 inference(scs_inference,[],[1121,1293,5076,5059,5081,33,421,412,410,415,426,416,2])).
% 70.49/70.54 cnf(5120,plain,
% 70.49/70.54 (~P10(a205,a208,a2)),
% 70.49/70.54 inference(scs_inference,[],[1121,4573,1293,5076,5059,5081,33,421,412,410,415,426,416,2,428])).
% 70.49/70.54 cnf(5124,plain,
% 70.49/70.54 (~P10(a205,a75,a179)),
% 70.49/70.54 inference(scs_inference,[],[1121,1288,884,4573,1293,5076,5059,5081,33,421,412,410,415,426,416,2,428,429,427])).
% 70.49/70.54 cnf(5126,plain,
% 70.49/70.54 (P3(a194,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1121,1288,884,4573,1293,5076,5059,5081,33,421,412,410,415,426,416,2,428,429,427,411])).
% 70.49/70.54 cnf(5133,plain,
% 70.49/70.54 (P8(f3(a2),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,1121,1288,884,4573,1293,5076,5059,5081,33,72,42,421,412,410,415,426,416,2,428,429,427,411,422,424,420])).
% 70.49/70.54 cnf(5140,plain,
% 70.49/70.54 (~P3(x51401,x51401)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5145,plain,
% 70.49/70.54 (~P3(x51451,x51451)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5155,plain,
% 70.49/70.54 (P6(f3(a2),f3(a2),f250(f3(a2),f3(a109)),f250(f3(a2),f3(a109)))),
% 70.49/70.54 inference(scs_inference,[],[407,648,1121,1288,884,4573,1293,5001,5076,5059,5081,896,4690,33,1045,344,110,239,316,72,69,52,317,307,42,458,441,5140,5145,51,421,412,410,415,426,416,2,428,429,427,411,422,424,420,423,413,417,437,418,419,431,540,731,3,438])).
% 70.49/70.54 cnf(5157,plain,
% 70.49/70.54 (P6(f3(a2),f250(f3(a2),f3(a109)),f3(a2),f250(f3(a2),f3(a109)))),
% 70.49/70.54 inference(scs_inference,[],[407,648,1121,1288,884,4573,1293,5001,5076,5059,5081,896,4690,33,1045,344,110,239,316,72,69,52,317,307,42,458,441,5140,5145,51,421,412,410,415,426,416,2,428,429,427,411,422,424,420,423,413,417,437,418,419,431,540,731,3,438,435])).
% 70.49/70.54 cnf(5176,plain,
% 70.49/70.54 (P7(f250(f3(x51761),f250(f3(x51762),f3(a4))))),
% 70.49/70.54 inference(scs_inference,[],[1316,5126,5133,4722,412,421,426,415])).
% 70.49/70.54 cnf(5178,plain,
% 70.49/70.54 (P8(f3(x51781),f250(f3(x51782),f3(a1)))),
% 70.49/70.54 inference(scs_inference,[],[1316,5126,5111,5133,4722,412,421,426,415,416])).
% 70.49/70.54 cnf(5180,plain,
% 70.49/70.54 (~E(a17,a199)),
% 70.49/70.54 inference(scs_inference,[],[1189,1316,5126,5111,5133,4722,412,421,426,415,416,2])).
% 70.49/70.54 cnf(5181,plain,
% 70.49/70.54 (~P10(a87,a43,a6)),
% 70.49/70.54 inference(scs_inference,[],[677,1189,1316,5098,5126,5111,5133,4722,412,421,426,415,416,2,428])).
% 70.49/70.54 cnf(5183,plain,
% 70.49/70.54 (~P10(a43,a184,a2)),
% 70.49/70.54 inference(scs_inference,[],[677,1189,1316,5098,5126,5111,5133,4722,519,412,421,426,415,416,2,428,429])).
% 70.49/70.54 cnf(5187,plain,
% 70.49/70.54 (P3(a199,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,677,1189,2849,1316,4926,5098,5126,5111,5133,4722,519,412,421,426,415,416,2,428,429,427,411])).
% 70.49/70.54 cnf(5188,plain,
% 70.49/70.54 (~P3(a17,x51881)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5197,plain,
% 70.49/70.54 (~P9(a252,f120(x51971))),
% 70.49/70.54 inference(scs_inference,[],[407,5188,677,1189,2849,4891,1316,4926,5070,5098,5126,5111,5133,4722,519,241,53,441,412,421,426,415,416,2,428,429,427,411,422,424,413,417])).
% 70.49/70.54 cnf(5223,plain,
% 70.49/70.54 (P8(f250(f3(x52231),f3(x52232)),f250(f3(x52233),f250(f3(x52234),f3(a43))))),
% 70.49/70.54 inference(scs_inference,[],[5187,4773,412,421])).
% 70.49/70.54 cnf(5227,plain,
% 70.49/70.54 (P7(f250(f3(x52271),f250(f3(x52272),f3(a43))))),
% 70.49/70.54 inference(scs_inference,[],[1487,5187,4773,4769,412,421,426,415])).
% 70.49/70.54 cnf(5231,plain,
% 70.49/70.54 (~E(a17,a214)),
% 70.49/70.54 inference(scs_inference,[],[1416,1487,5187,4773,4769,412,421,426,415,416,2])).
% 70.49/70.54 cnf(5232,plain,
% 70.49/70.54 (~P10(a219,a223,a2)),
% 70.49/70.54 inference(scs_inference,[],[1416,1487,5187,4773,4769,4611,412,421,426,415,416,2,428])).
% 70.49/70.54 cnf(5234,plain,
% 70.49/70.54 (~P10(a17,a89,a2)),
% 70.49/70.54 inference(scs_inference,[],[1416,1485,1487,5187,4773,4769,4611,412,421,426,415,416,2,428,429])).
% 70.49/70.54 cnf(5238,plain,
% 70.49/70.54 (P3(a214,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1416,1485,954,1487,5187,4773,4769,4611,412,421,426,415,416,2,428,429,427,411])).
% 70.49/70.54 cnf(5239,plain,
% 70.49/70.54 (~P3(a17,x52391)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5254,plain,
% 70.49/70.54 (~P9(a2,f132(f250(f3(x52541),f3(a43))))),
% 70.49/70.54 inference(scs_inference,[],[407,1416,1485,954,1487,5183,5187,4773,4769,4456,966,4611,1079,391,4791,243,333,54,62,308,458,441,412,421,426,415,416,2,428,429,427,411,424,422,423,413,417,437,418])).
% 70.49/70.54 cnf(5255,plain,
% 70.49/70.54 (P8(f3(x52551),f250(f3(x52552),f3(a43)))),
% 70.49/70.54 inference(rename_variables,[],[4773])).
% 70.49/70.54 cnf(5257,plain,
% 70.49/70.54 (~P9(a17,f120(f3(x52571)))),
% 70.49/70.54 inference(scs_inference,[],[407,5239,1416,1485,954,1487,5183,5187,4773,5255,4769,4456,966,4611,1079,391,4791,92,243,333,54,62,308,458,441,412,421,426,415,416,2,428,429,427,411,424,422,423,413,417,437,418,419])).
% 70.49/70.54 cnf(5267,plain,
% 70.49/70.54 (~P9(a252,f120(x52671))),
% 70.49/70.54 inference(rename_variables,[],[5197])).
% 70.49/70.54 cnf(5273,plain,
% 70.49/70.54 (P10(a6,a206,a65)),
% 70.49/70.54 inference(scs_inference,[],[407,5239,1416,1485,954,1487,5041,5183,5187,5197,5267,4773,5255,5178,4769,5155,4456,966,4611,1079,391,4855,4791,92,150,243,333,54,56,71,62,64,66,308,458,441,51,412,421,426,415,416,2,428,429,427,411,424,422,423,413,417,437,418,419,431,999,574,540,4313,4184,731,430,433])).
% 70.49/70.54 cnf(5274,plain,
% 70.49/70.54 (P8(f3(x52741),f250(f3(x52742),f3(a1)))),
% 70.49/70.54 inference(rename_variables,[],[5178])).
% 70.49/70.54 cnf(5276,plain,
% 70.49/70.54 (P10(a109,a170,a228)),
% 70.49/70.54 inference(scs_inference,[],[407,5239,1416,1485,954,1487,5041,5183,5187,5197,5267,4773,5255,5178,5274,4769,4968,5155,4456,966,4611,1079,391,4855,4791,92,150,243,333,54,56,68,71,62,64,167,66,60,308,458,441,51,412,421,426,415,416,2,428,429,427,411,424,422,423,413,417,437,418,419,431,999,574,540,4313,4184,731,430,433,434])).
% 70.49/70.54 cnf(5282,plain,
% 70.49/70.54 (~P9(a2,f132(f250(f3(x52821),f3(a43))))),
% 70.49/70.54 inference(rename_variables,[],[5254])).
% 70.49/70.54 cnf(5291,plain,
% 70.49/70.54 (P7(f250(f3(x52911),f250(f3(x52912),f3(a54))))),
% 70.49/70.54 inference(scs_inference,[],[1581,5238,4831,4825,5254,5282,1065,1136,412,421,426,415])).
% 70.49/70.54 cnf(5297,plain,
% 70.49/70.54 (~E(a17,a216)),
% 70.49/70.54 inference(scs_inference,[],[1450,1581,5238,4831,4825,5257,5254,5282,1065,1136,412,421,426,415,416,731,2])).
% 70.49/70.54 cnf(5300,plain,
% 70.49/70.54 (~P10(a54,a195,a2)),
% 70.49/70.54 inference(scs_inference,[],[706,1450,1581,5043,5238,4831,4825,5257,5254,5282,2751,1065,1136,412,421,426,415,416,731,2,428,429])).
% 70.49/70.54 cnf(5305,plain,
% 70.49/70.54 (P8(f3(x53051),f250(f3(x53052),f3(a54)))),
% 70.49/70.54 inference(rename_variables,[],[4831])).
% 70.49/70.54 cnf(5307,plain,
% 70.49/70.54 (P3(a216,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,706,1450,1581,5043,5238,5273,4831,4825,5257,5254,5282,1081,2751,42,1065,1136,412,421,426,415,416,731,2,428,429,427,22,21,411])).
% 70.49/70.54 cnf(5308,plain,
% 70.49/70.54 (~P3(a17,x53081)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5317,plain,
% 70.49/70.54 (~P9(a166,f120(x53171))),
% 70.49/70.54 inference(scs_inference,[],[407,5308,706,1450,1581,4946,5043,5120,5238,5273,4831,4825,5257,5254,5282,1081,2751,5133,306,201,42,441,1065,1136,412,421,426,415,416,731,2,428,429,427,22,21,411,422,424,413,417])).
% 70.49/70.54 cnf(5318,plain,
% 70.49/70.54 (~P3(x53181,x53181)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5323,plain,
% 70.49/70.54 (P8(f3(x53231),f250(f3(x53232),f3(a54)))),
% 70.49/70.54 inference(rename_variables,[],[4831])).
% 70.49/70.54 cnf(5324,plain,
% 70.49/70.54 (~P3(x53241,x53241)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5330,plain,
% 70.49/70.54 (P10(a170,a109,a228)),
% 70.49/70.54 inference(scs_inference,[],[407,5308,706,1450,1581,4946,5043,5120,5238,5273,5276,4831,5305,5323,4825,5257,5254,5282,1081,2751,375,5133,58,306,191,201,352,167,60,317,42,441,5318,5324,1065,1136,412,421,426,415,416,731,2,428,429,427,22,21,411,422,424,413,417,437,418,419,430])).
% 70.49/70.54 cnf(5332,plain,
% 70.49/70.54 (P10(a122,a2,a122)),
% 70.49/70.54 inference(scs_inference,[],[407,5308,706,1450,1581,4946,5043,5120,5238,5273,5276,4831,5305,5323,4825,5257,5157,5254,5282,1081,2751,375,5133,58,150,306,191,201,352,167,60,317,42,441,5318,5324,51,1065,1136,412,421,426,415,416,731,2,428,429,427,22,21,411,422,424,413,417,437,418,419,430,431])).
% 70.49/70.54 cnf(5338,plain,
% 70.49/70.54 (P8(f250(f3(x53381),f3(x53382)),f250(f3(x53383),f250(f3(x53384),f3(a65))))),
% 70.49/70.54 inference(scs_inference,[],[4887,421])).
% 70.49/70.54 cnf(5344,plain,
% 70.49/70.54 (P7(f250(f3(x53441),f250(f3(x53442),f3(a65))))),
% 70.49/70.54 inference(scs_inference,[],[1614,5307,4887,4883,421,412,426,415])).
% 70.49/70.54 cnf(5349,plain,
% 70.49/70.54 (~P9(a166,f120(x53491))),
% 70.49/70.54 inference(rename_variables,[],[5317])).
% 70.49/70.54 cnf(5350,plain,
% 70.49/70.54 (~E(a17,a221)),
% 70.49/70.54 inference(scs_inference,[],[1516,1614,5307,5317,4887,4883,421,412,426,415,416,731,2])).
% 70.49/70.54 cnf(5351,plain,
% 70.49/70.54 (~P10(a153,a232,a2)),
% 70.49/70.54 inference(scs_inference,[],[1516,1614,4180,4817,5307,5317,4887,4883,421,412,426,415,416,731,2,428])).
% 70.49/70.54 cnf(5353,plain,
% 70.49/70.54 (~P10(a17,a97,a2)),
% 70.49/70.54 inference(scs_inference,[],[1516,1612,1614,4180,4817,5307,5317,4887,4883,421,412,426,415,416,731,2,428,429])).
% 70.49/70.54 cnf(5355,plain,
% 70.49/70.54 (~P10(a227,a97,a230)),
% 70.49/70.54 inference(scs_inference,[],[1516,1612,1688,1614,4180,4817,5307,5317,4887,4883,421,412,426,415,416,731,2,428,429,427])).
% 70.49/70.54 cnf(5358,plain,
% 70.49/70.54 (P3(a221,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1516,1612,1688,1614,4180,4817,5307,5317,5349,4887,4883,306,421,412,426,415,416,731,2,428,429,427,27,411])).
% 70.49/70.54 cnf(5372,plain,
% 70.49/70.54 (P6(f3(a2),f3(a1),f3(a98),f3(a109))),
% 70.49/70.54 inference(scs_inference,[],[407,1516,1612,1688,1614,4180,1653,4817,5003,5300,5307,5317,5349,4887,4883,1661,1113,78,4791,325,397,55,306,458,421,412,426,415,416,731,2,428,429,427,27,411,424,422,24,423,26,413,436])).
% 70.49/70.54 cnf(5375,plain,
% 70.49/70.54 (~P9(a186,f120(x53751))),
% 70.49/70.54 inference(scs_inference,[],[407,1516,1612,1688,1614,4180,1653,4817,5003,5072,5300,5307,5317,5349,4887,4883,1661,1113,78,498,4791,325,397,181,55,306,458,441,421,412,426,415,416,731,2,428,429,427,27,411,424,422,24,423,26,413,436,23,417])).
% 70.49/70.54 cnf(5376,plain,
% 70.49/70.54 (~P3(x53761,x53761)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5381,plain,
% 70.49/70.54 (~P3(x53811,x53811)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5394,plain,
% 70.49/70.54 (P10(a40,a239,a98)),
% 70.49/70.54 inference(scs_inference,[],[407,743,1516,1612,1688,1614,4180,1653,4817,5003,5072,5124,5181,5300,5307,5317,5349,4887,4883,5223,1661,5178,4968,1113,4773,78,498,336,4791,77,325,397,59,109,181,199,54,58,55,306,71,69,317,458,441,5376,5381,421,412,426,415,416,731,2,428,429,427,27,411,424,422,24,423,26,413,436,23,417,437,418,419,430,431,540,3,433])).
% 70.49/70.54 cnf(5404,plain,
% 70.49/70.54 (P7(f250(f3(x54041),f250(f3(x54042),f3(a76))))),
% 70.49/70.54 inference(scs_inference,[],[5358,4942,4936,421,412,415])).
% 70.49/70.54 cnf(5413,plain,
% 70.49/70.54 (~P10(a195,a76,a2)),
% 70.49/70.54 inference(scs_inference,[],[778,631,1692,5358,5375,4942,4936,2761,421,412,415,426,416,731,2,428])).
% 70.49/70.54 cnf(5415,plain,
% 70.49/70.54 (~P10(a76,a195,a2)),
% 70.49/70.54 inference(scs_inference,[],[778,631,1692,5358,5375,4942,4936,2761,2751,421,412,415,426,416,731,2,428,429])).
% 70.49/70.54 cnf(5421,plain,
% 70.49/70.54 (P3(a134,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,778,631,1692,5358,5375,4942,4936,2761,5273,2751,4960,421,412,415,426,416,731,2,428,429,427,424,411])).
% 70.49/70.54 cnf(5422,plain,
% 70.49/70.54 (~P3(a17,x54221)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5429,plain,
% 70.49/70.54 (~P9(a188,f120(x54291))),
% 70.49/70.54 inference(scs_inference,[],[407,5422,778,631,5000,1692,5232,5358,5375,4942,4936,2761,5273,2751,4960,183,215,441,421,412,415,426,416,731,2,428,429,427,424,411,422,413,417])).
% 70.49/70.54 cnf(5435,plain,
% 70.49/70.54 (P8(f3(x54351),f250(f3(x54352),f3(a76)))),
% 70.49/70.54 inference(rename_variables,[],[4942])).
% 70.49/70.54 cnf(5440,plain,
% 70.49/70.54 (P10(a239,a40,a98)),
% 70.49/70.54 inference(scs_inference,[],[407,5422,778,631,5000,1692,5232,5358,5394,5375,4942,5435,4936,4476,2823,2761,5273,393,2751,4960,378,77,183,215,53,69,308,441,421,412,415,426,416,731,2,428,429,427,424,411,422,413,417,437,418,419,430])).
% 70.49/70.54 cnf(5454,plain,
% 70.49/70.54 (P7(f250(f3(x54541),f250(f3(x54542),f3(a87))))),
% 70.49/70.54 inference(scs_inference,[],[5421,4996,4992,412,421,415])).
% 70.49/70.54 cnf(5461,plain,
% 70.49/70.54 (~P9(a188,f120(x54611))),
% 70.49/70.54 inference(rename_variables,[],[5429])).
% 70.49/70.54 cnf(5463,plain,
% 70.49/70.54 (~P10(a161,a230,a2)),
% 70.49/70.54 inference(scs_inference,[],[660,1732,4306,4712,5421,5429,4996,4992,412,421,415,426,416,731,2,428])).
% 70.49/70.54 cnf(5465,plain,
% 70.49/70.54 (~P10(a17,a104,a2)),
% 70.49/70.54 inference(scs_inference,[],[660,1730,1732,4306,4712,5421,5429,4996,4992,412,421,415,426,416,731,2,428,429])).
% 70.49/70.54 cnf(5469,plain,
% 70.49/70.54 (P3(a146,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,660,1730,1728,1732,4306,4712,5421,5429,4996,4992,412,421,415,426,416,731,2,428,429,427,411])).
% 70.49/70.54 cnf(5480,plain,
% 70.49/70.54 (~P9(a190,f120(x54801))),
% 70.49/70.54 inference(scs_inference,[],[407,660,1730,1728,1732,4306,4712,5415,5421,5429,4996,4992,1700,1147,5133,185,57,458,441,412,421,415,426,416,731,2,428,429,427,411,424,422,423,413,417])).
% 70.49/70.54 cnf(5481,plain,
% 70.49/70.54 (~P3(x54811,x54811)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5483,plain,
% 70.49/70.54 (P6(f3(a2),f3(a76),f3(a109),f250(f3(a65),f3(a1)))),
% 70.49/70.54 inference(scs_inference,[],[407,660,1730,1728,1732,4306,4712,5415,5421,5429,4996,4992,1700,1147,376,5133,185,357,57,317,458,441,412,421,415,426,416,731,2,428,429,427,411,424,422,423,413,417,437])).
% 70.49/70.54 cnf(5486,plain,
% 70.49/70.54 (P8(f3(x54861),f250(f3(x54862),f3(a87)))),
% 70.49/70.54 inference(rename_variables,[],[4996])).
% 70.49/70.54 cnf(5487,plain,
% 70.49/70.54 (~P3(x54871,x54871)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5495,plain,
% 70.49/70.54 (P10(a1,a87,a98)),
% 70.49/70.54 inference(scs_inference,[],[407,660,1730,1728,1732,4306,4712,5355,5415,5421,5027,5429,4996,5486,4992,1700,1147,376,5133,129,185,219,220,357,56,57,58,59,52,317,458,441,5481,5487,412,421,415,426,416,731,2,428,429,427,411,424,422,423,413,417,437,418,419,430,431])).
% 70.49/70.54 cnf(5499,plain,
% 70.49/70.54 (~P9(a188,f120(x54991))),
% 70.49/70.54 inference(rename_variables,[],[5429])).
% 70.49/70.54 cnf(5502,plain,
% 70.49/70.54 (P8(f3(a65),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[407,660,1730,1728,1732,4306,4712,5355,5415,5421,5027,5429,5461,5499,4996,5486,4992,1700,1147,376,5133,129,185,219,220,357,4672,56,57,58,59,52,47,317,458,441,5481,5487,412,421,415,426,416,731,2,428,429,427,411,424,422,423,413,417,437,418,419,430,431,540,4313,4184,420])).
% 70.49/70.54 cnf(5513,plain,
% 70.49/70.54 (P7(f250(f3(x55131),f250(f3(x55132),f3(a98))))),
% 70.49/70.54 inference(scs_inference,[],[5469,5502,5063,421,412,415])).
% 70.49/70.54 cnf(5522,plain,
% 70.49/70.54 (~P10(a206,a65,a2)),
% 70.49/70.54 inference(scs_inference,[],[805,688,1384,5469,5480,5502,5063,562,421,412,415,426,416,731,2,428])).
% 70.49/70.54 cnf(5528,plain,
% 70.49/70.54 (P8(f3(a54),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[805,910,688,1384,5440,5469,5480,5502,5063,5043,562,46,421,412,415,426,416,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5532,plain,
% 70.49/70.54 (P3(a157,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,805,910,688,1384,5440,5469,5480,5502,5063,5043,562,46,421,412,415,426,416,731,2,428,429,427,420,424,411])).
% 70.49/70.54 cnf(5533,plain,
% 70.49/70.54 (~P3(a17,x55331)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5540,plain,
% 70.49/70.54 (~P9(a212,f120(x55401))),
% 70.49/70.54 inference(scs_inference,[],[407,5533,805,910,688,5069,1384,5234,5440,5469,5480,5502,5063,5043,562,205,72,46,441,421,412,415,426,416,731,2,428,429,427,420,424,411,422,413,417])).
% 70.49/70.54 cnf(5561,plain,
% 70.49/70.54 (P7(f250(f3(x55611),f250(f3(x55612),f3(a109))))),
% 70.49/70.54 inference(scs_inference,[],[5113,415])).
% 70.49/70.54 cnf(5574,plain,
% 70.49/70.54 (~P10(a170,a98,a228)),
% 70.49/70.54 inference(scs_inference,[],[1223,1418,5330,5532,5528,5540,5113,1008,415,421,412,426,416,731,2,428])).
% 70.49/70.54 cnf(5576,plain,
% 70.49/70.54 (~P10(a17,a84,a2)),
% 70.49/70.54 inference(scs_inference,[],[1223,1418,5330,5532,5528,5540,5113,1008,1416,415,421,412,426,416,731,2,428,429])).
% 70.49/70.54 cnf(5580,plain,
% 70.49/70.54 (P8(f3(a43),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[1223,1767,1418,5330,5532,5528,5540,5113,1008,1416,45,415,421,412,426,416,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5586,plain,
% 70.49/70.54 (P3(a201,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1223,1767,1418,5330,5353,5532,5528,5540,5113,1008,1416,72,45,415,421,412,426,416,731,2,428,429,427,420,424,422,411])).
% 70.49/70.54 cnf(5593,plain,
% 70.49/70.54 (~P9(a214,f120(x55931))),
% 70.49/70.54 inference(scs_inference,[],[407,1223,1767,1418,5330,5353,5532,5528,5540,5113,1740,1008,1181,1416,207,72,45,458,441,415,421,412,426,416,731,2,428,429,427,420,424,422,411,413,423,417])).
% 70.49/70.54 cnf(5628,plain,
% 70.49/70.54 (~P10(a206,a87,a2)),
% 70.49/70.54 inference(scs_inference,[],[875,719,1518,5586,5580,5593,4653,4722,562,415,412,421,426,416,731,2,428])).
% 70.49/70.54 cnf(5637,plain,
% 70.49/70.54 (P8(f3(a4),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[875,945,719,1518,5495,5586,5580,5593,5065,4653,1308,4722,5043,562,44,42,415,412,421,426,416,731,2,428,429,427,21,22,420])).
% 70.49/70.54 cnf(5641,plain,
% 70.49/70.54 (P3(a168,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,875,945,719,1518,5495,5586,5580,5593,5065,4653,1308,4722,5043,562,44,42,415,412,421,426,416,731,2,428,429,427,21,22,420,424,411])).
% 70.49/70.54 cnf(5642,plain,
% 70.49/70.54 (~P3(a17,x56421)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5649,plain,
% 70.49/70.54 (~P9(a221,f120(x56491))),
% 70.49/70.54 inference(scs_inference,[],[407,5642,875,945,719,5119,1518,5351,5495,5586,5580,5593,5065,4653,1308,4722,5043,562,213,223,44,42,441,415,412,421,426,416,731,2,428,429,427,21,22,420,424,411,422,413,417])).
% 70.49/70.54 cnf(5677,plain,
% 70.49/70.54 (~P9(a221,f120(x56771))),
% 70.49/70.54 inference(rename_variables,[],[5649])).
% 70.49/70.54 cnf(5681,plain,
% 70.49/70.54 (~P10(a17,a59,a2)),
% 70.49/70.54 inference(scs_inference,[],[754,1807,3185,3187,5332,5641,5637,5649,5176,415,421,412,426,731,2,428,429])).
% 70.49/70.54 cnf(5686,plain,
% 70.49/70.54 (P8(f3(a1),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[754,1807,3185,3187,5332,5641,5637,5649,5677,5176,213,43,415,421,412,426,731,2,428,429,427,27,420])).
% 70.49/70.54 cnf(5688,plain,
% 70.49/70.54 (P3(a169,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5641,5637,5649,5677,5176,213,43,415,421,412,426,731,2,428,429,427,27,420,411])).
% 70.49/70.54 cnf(5694,plain,
% 70.49/70.54 (P6(f3(a2),f3(a4),f3(a65),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5465,5641,5637,5649,5677,5176,649,332,377,213,72,43,415,421,412,426,731,2,428,429,427,27,420,411,422,24,436])).
% 70.49/70.54 cnf(5697,plain,
% 70.49/70.54 (~P9(a221,f120(x56971))),
% 70.49/70.54 inference(rename_variables,[],[5649])).
% 70.49/70.54 cnf(5703,plain,
% 70.49/70.54 (~P9(a134,f120(x57031))),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5413,5465,5641,5637,5649,5677,5176,1779,1215,649,84,332,377,160,562,213,72,43,458,441,415,421,412,426,731,2,428,429,427,27,420,411,422,24,436,26,23,413,423,417])).
% 70.49/70.54 cnf(5704,plain,
% 70.49/70.54 (~P3(x57041,x57041)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5709,plain,
% 70.49/70.54 (~P3(x57091,x57091)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5716,plain,
% 70.49/70.54 (~P10(a65,a206,a2)),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5413,5465,5522,5641,5637,5649,5677,5176,5338,1779,1215,649,84,345,5178,332,377,160,562,213,56,66,72,317,43,458,441,5704,5709,415,421,412,426,731,2,428,429,427,27,420,411,422,24,436,26,23,413,423,417,437,418,419,430])).
% 70.49/70.54 cnf(5718,plain,
% 70.49/70.54 (P10(a121,a217,a228)),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5413,5465,5522,5641,5637,5649,5677,5176,5338,1779,5027,1215,649,84,345,5178,332,377,160,562,61,213,67,56,68,66,72,317,43,458,441,5704,5709,415,421,412,426,731,2,428,429,427,27,420,411,422,24,436,26,23,413,423,417,437,418,419,430,432])).
% 70.49/70.54 cnf(5720,plain,
% 70.49/70.54 (P10(a1,a98,a109)),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5413,5465,5522,5641,5372,5637,5649,5677,5176,5338,1779,5027,1215,649,84,345,5178,332,377,160,562,61,213,67,56,59,68,66,52,72,60,317,43,458,441,5704,5709,415,421,412,426,731,2,428,429,427,27,420,411,422,24,436,26,23,413,423,417,437,418,419,430,432,431])).
% 70.49/70.54 cnf(5724,plain,
% 70.49/70.54 (~P9(a221,f120(x57241))),
% 70.49/70.54 inference(rename_variables,[],[5649])).
% 70.49/70.54 cnf(5727,plain,
% 70.49/70.54 (P8(f250(f3(a4),f3(a1)),f250(f3(a98),f3(a1)))),
% 70.49/70.54 inference(scs_inference,[],[407,754,1807,3185,3187,5332,5413,5465,5522,5641,5372,5637,5649,5677,5697,5724,5176,5338,1779,5027,1215,5111,649,84,345,5178,332,377,160,562,61,213,67,56,59,68,66,52,72,60,317,43,458,441,5704,5709,415,421,412,426,731,2,428,429,427,27,420,411,422,24,436,26,23,413,423,417,437,418,419,430,432,431,540,4313,4184,424])).
% 70.49/70.54 cnf(5747,plain,
% 70.49/70.54 (~P10(a17,a42,a2)),
% 70.49/70.54 inference(scs_inference,[],[789,3318,5688,5686,5703,5227,779,791,415,421,412,426,731,2,428,429])).
% 70.49/70.54 cnf(5751,plain,
% 70.49/70.54 (P8(f3(a2),f3(a98))),
% 70.49/70.54 inference(scs_inference,[],[789,1847,3318,5688,5686,5703,5227,779,791,42,415,421,412,426,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5753,plain,
% 70.49/70.54 (P3(a172,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,789,1847,3318,5688,5686,5703,5227,779,791,42,415,421,412,426,731,2,428,429,427,420,411])).
% 70.49/70.54 cnf(5754,plain,
% 70.49/70.54 (~P3(a17,x57541)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5761,plain,
% 70.49/70.54 (~P9(a157,f120(x57611))),
% 70.49/70.54 inference(scs_inference,[],[407,5754,789,1847,5180,3318,5463,5688,5686,5703,5227,779,791,163,221,42,441,415,421,412,426,731,2,428,429,427,420,411,422,413,417])).
% 70.49/70.54 cnf(5762,plain,
% 70.49/70.54 (~P3(x57621,x57621)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5767,plain,
% 70.49/70.54 (~P3(x57671,x57671)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5772,plain,
% 70.49/70.54 (P10(a98,a2,a98)),
% 70.49/70.54 inference(scs_inference,[],[407,5754,789,1847,5180,3318,5463,5688,5686,5703,5227,2256,779,791,389,163,221,315,59,68,52,308,42,441,5762,5767,51,415,421,412,426,731,2,428,429,427,420,411,422,413,417,437,418,419,431])).
% 70.49/70.54 cnf(5796,plain,
% 70.49/70.54 (~P10(a17,a74,a2)),
% 70.49/70.54 inference(scs_inference,[],[1257,2790,3372,3374,5718,5753,5751,5761,5291,421,415,412,426,731,2,428,429])).
% 70.49/70.54 cnf(5800,plain,
% 70.49/70.54 (P8(f3(a65),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[1257,1964,2790,3372,3374,5718,5753,5751,5761,5291,48,47,421,415,412,426,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5802,plain,
% 70.49/70.54 (P3(a203,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1257,1964,2790,3372,3374,5718,5753,5751,5761,5291,48,47,421,415,412,426,731,2,428,429,427,420,411])).
% 70.49/70.54 cnf(5809,plain,
% 70.49/70.54 (~P9(a168,f120(x58091))),
% 70.49/70.54 inference(scs_inference,[],[407,1257,1964,2790,3372,3374,5716,5718,5753,5751,5761,5291,1939,165,56,48,47,441,421,415,412,426,731,2,428,429,427,420,411,422,413,417])).
% 70.49/70.54 cnf(5837,plain,
% 70.49/70.54 (~P10(a45,a17,a2)),
% 70.49/70.54 inference(scs_inference,[],[816,3478,5802,5800,5809,5344,806,421,415,412,426,731,2,428])).
% 70.49/70.54 cnf(5839,plain,
% 70.49/70.54 (~P10(a17,a45,a2)),
% 70.49/70.54 inference(scs_inference,[],[816,3478,5802,5800,5809,5344,821,806,421,415,412,426,731,2,428,429])).
% 70.49/70.54 cnf(5843,plain,
% 70.49/70.54 (P8(f3(a54),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[816,2000,3478,5802,5800,5809,5344,821,806,46,421,415,412,426,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5845,plain,
% 70.49/70.54 (P3(a175,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,816,2000,3478,5802,5800,5809,5344,821,806,46,421,415,412,426,731,2,428,429,427,420,411])).
% 70.49/70.54 cnf(5846,plain,
% 70.49/70.54 (~P3(a17,x58461)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5853,plain,
% 70.49/70.54 (~P9(a169,f120(x58531))),
% 70.49/70.54 inference(scs_inference,[],[407,5846,816,2000,5231,3478,5576,5802,5800,5809,5344,821,806,166,46,72,441,421,415,412,426,731,2,428,429,427,420,411,422,413,417])).
% 70.49/70.54 cnf(5885,plain,
% 70.49/70.54 (~P10(a17,a88,a2)),
% 70.49/70.54 inference(scs_inference,[],[886,3532,3534,5720,5845,5843,5853,5404,945,421,412,415,426,731,2,428,429])).
% 70.49/70.54 cnf(5889,plain,
% 70.49/70.54 (P8(f3(a43),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[886,2036,3532,3534,5720,5845,5843,5853,5404,945,45,421,412,415,426,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5891,plain,
% 70.49/70.54 (P3(a179,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,886,2036,3532,3534,5720,5845,5843,5853,5404,945,45,421,412,415,426,731,2,428,429,427,420,411])).
% 70.49/70.54 cnf(5900,plain,
% 70.49/70.54 (~P9(a172,f120(x59001))),
% 70.49/70.54 inference(scs_inference,[],[407,886,2036,3532,3534,5681,5720,5845,5843,5853,5404,2012,945,1280,169,45,72,458,441,421,412,415,426,731,2,428,429,427,420,411,422,423,413,417])).
% 70.49/70.54 cnf(5941,plain,
% 70.49/70.54 (P8(f3(a4),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[956,2074,3563,5891,5889,5900,5454,961,946,44,421,412,415,426,731,2,428,429,427,420])).
% 70.49/70.54 cnf(5943,plain,
% 70.49/70.54 (P3(a183,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,956,2074,3563,5891,5889,5900,5454,961,946,44,421,412,415,426,731,2,428,429,427,420,411])).
% 70.49/70.54 cnf(5944,plain,
% 70.49/70.54 (~P3(a17,x59441)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(5951,plain,
% 70.49/70.54 (~P9(a175,f120(x59511))),
% 70.49/70.54 inference(scs_inference,[],[407,5944,956,2074,5297,3563,5891,5747,5889,5900,5454,961,946,171,72,44,441,421,412,415,426,731,2,428,429,427,420,411,422,413,417])).
% 70.49/70.54 cnf(5952,plain,
% 70.49/70.54 (~P3(x59521,x59521)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5957,plain,
% 70.49/70.54 (~P3(x59571,x59571)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(5964,plain,
% 70.49/70.54 (P10(a38,a206,a109)),
% 70.49/70.54 inference(scs_inference,[],[407,5944,956,2074,5297,3563,5891,5747,5889,5900,5483,5454,4727,961,946,450,373,75,171,333,5178,54,67,66,60,72,44,317,441,5952,5957,51,421,412,415,426,731,2,428,429,427,420,411,422,413,417,437,418,419,431,433])).
% 70.49/70.54 cnf(5982,plain,
% 70.49/70.54 (~P9(a175,f120(x59821))),
% 70.49/70.54 inference(rename_variables,[],[5951])).
% 70.49/70.54 cnf(5993,plain,
% 70.49/70.54 (P8(f3(a1),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[1314,2111,3617,3619,5772,5943,5941,5951,5982,5513,4823,171,43,412,421,415,426,731,2,428,27,429,427,424,420])).
% 70.49/70.54 cnf(6001,plain,
% 70.49/70.54 (P3(a208,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1314,2111,3617,3619,5772,5628,5796,5943,5941,5951,5982,5513,2792,96,649,4823,379,397,171,43,412,421,415,426,731,2,428,27,429,427,424,420,436,24,26,23,411])).
% 70.49/70.54 cnf(6010,plain,
% 70.49/70.54 (~P9(a183,f120(x60101))),
% 70.49/70.54 inference(scs_inference,[],[407,1314,2111,3617,3619,5772,5628,5796,5943,5941,5951,5982,5513,2086,2792,1306,96,649,4823,379,179,397,171,72,43,458,441,412,421,415,426,731,2,428,27,429,427,424,420,436,24,26,23,411,422,423,413,417])).
% 70.49/70.54 cnf(6011,plain,
% 70.49/70.54 (~P3(x60111,x60111)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(6016,plain,
% 70.49/70.54 (~P3(x60161,x60161)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(6026,plain,
% 70.49/70.54 (P10(a87,a133,a65)),
% 70.49/70.54 inference(scs_inference,[],[407,1314,2111,3617,3619,5772,5628,5796,5837,5943,5964,5694,5941,5951,5982,4782,5513,2086,2792,1306,4724,96,399,649,4823,81,379,75,179,397,171,62,56,58,66,72,317,43,458,441,6011,6016,51,412,421,415,426,731,2,428,27,429,427,424,420,436,24,26,23,411,422,423,413,417,437,418,419,430,431,433])).
% 70.49/70.54 cnf(6053,plain,
% 70.49/70.54 (P8(f3(a2),f3(a87))),
% 70.49/70.54 inference(scs_inference,[],[1019,4454,3649,6001,5993,6010,5561,1024,1009,42,421,412,415,426,731,2,428,429,427,420])).
% 70.49/70.54 cnf(6055,plain,
% 70.49/70.54 (P3(a188,a17)),
% 70.49/70.54 inference(scs_inference,[],[407,1019,4454,3649,6001,5993,6010,5561,1024,1009,42,421,412,415,426,731,2,428,429,427,420,411])).
% 70.49/70.54 cnf(6056,plain,
% 70.49/70.54 (~P3(a17,x60561)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(6063,plain,
% 70.49/70.54 (~P9(a189,f120(x60631))),
% 70.49/70.54 inference(scs_inference,[],[407,6056,1019,4454,5350,3649,5839,6001,5993,6010,5561,1024,1009,184,72,42,441,421,412,415,426,731,2,428,429,427,420,411,422,413,417])).
% 70.49/70.54 cnf(6105,plain,
% 70.49/70.54 (~P3(a17,x61051)),
% 70.49/70.54 inference(rename_variables,[],[407])).
% 70.49/70.54 cnf(6114,plain,
% 70.49/70.54 (~P3(x61141,x61141)),
% 70.49/70.54 inference(rename_variables,[],[441])).
% 70.49/70.54 cnf(6123,plain,
% 70.49/70.54 ($false),
% 70.49/70.54 inference(scs_inference,[],[407,6105,1155,1017,1769,4682,1771,5574,5885,6026,6055,6053,6063,5727,994,1340,371,78,187,316,167,67,59,47,46,72,317,458,441,6114,412,421,426,731,2,428,429,427,420,411,422,423,413,417,437,418,430,419]),
% 70.49/70.54 ['proof']).
% 70.49/70.54 % SZS output end Proof
% 70.49/70.54 % Total time :69.800000s
%------------------------------------------------------------------------------