%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN420-1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Thu May 7 07:39:46 PM UTC 2026
% Result : Satisfiable 5.08s 1.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN420-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n014.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 13:42:22 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 SPASS-SCL-FOL version:
% 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.08/1.72 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.08/1.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.08/1.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.08/1.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.08/1.72 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.08/1.72 Execution lmodel_grow ended with status: satisfiable
% 5.08/1.72 Used heuristic: lmodel_grow
% 5.08/1.72
% 5.08/1.72 Input Clauses:
% 5.08/1.72
% 5.08/1.72 Predicates: ndr1_0 c10_0 c7_0 c3_0 ssSkC10 c5_0 c4_0 c9_0 c6_0 ssSkC38 ssSkC37 ssSkC36 ssSkC33 ssSkC32 ssSkC31 ssSkC28 ssSkC27 ssSkC24 ssSkC21 ssSkC20 ssSkC19 ssSkC18 ssSkC17 ssSkC16 ssSkC14 ssSkC13 ssSkC11 ssSkC9 ssSkC7 ssSkC6 ssSkC5 ssSkC4 ssSkC3 ssSkC2 ssSkC1 ssSkC0 c8_0 c2_0 ssSkC29 ssSkC26 ssSkC23 ndr1_1 c10_1 c2_1 ssSkC8 c8_1 c5_1 ssSkP7 c7_1 c1_1 ssSkP6 c3_1 ssSkP5 ssSkP4 ssSkP3 c9_1 ssSkP2 c6_1 ssSkP1 c4_1 ssSkP0 ssSkC15 c6_2 c7_2 c2_2 c1_2 c1_0 c10_2 c9_2 c4_2 c3_2 c5_2 c8_2 ssSkC35 ssSkC25 ssSkC12 ssSkC22 ssSkC34 ssSkC30
% 5.08/1.72 Fol Constants: a352 a350 a348 a307 a272 a442 a434 a422 a414 a403 a394 a386 a371 a367 a356 a345 a339 a333 a330 a323 a313 a310 a308 a300 a297 a296 a283 a448 a436 a408 a405 a398 a395 a374 a361 a353 a351 a349 a343 a332 a329 a315 a282 a273 a446 a435 a427 a415 a412 a406 a404 a392 a389 a379 a368 a362 a360 a357 a346 a341 a340 a335 a334 a331 a324 a311 a309 a301 a298 a285 a281 a445 a437 a432 a424 a416 a410 a409 a396 a384 a344 a325 a319 a291 a278 a277 a423 a391 a373 a372 a314 a284 a274 a425 a420 a418 a417 a385 a381 a355 a326 a305 a293 a292 a279 a271 a433 a421 a382 a306 a431 a318 a287 a399 a393 a312 a299 a380 a290 a289 a288 a430 a407 a354 a337 a440 a429 a294 a426 a402 a388 a444 a413 a390 a387 a342 a336 a328 a295 a275 a443 a338 a441 a280 a438 a286 a276 a364 a428 a411 a447 a400 a316 a317 a365 a302 a363 a419 a366 a327 a303 a401 a383 a358 a439 a369 a359 a347 a370 a304 a269 a270 a375 a320 a376 a321 a377 a322
% 5.08/1.72 Fol Functions:
% 5.08/1.72 Problem Properties:
% 5.08/1.72 This is a Bernays Schoenfinkel problem.
% 5.08/1.72
% 5.08/1.72 After reduction: Problem Properties:
% 5.08/1.72 This is a Bernays Schoenfinkel problem.
% 5.08/1.72
% 5.08/1.72
% 5.08/1.72 Reduced Input Clauses:
% 5.08/1.72 606:1:0:[26.1,4.0]:: -> ndr1_0
% 5.08/1.72 607:2:0:[51.0,36.1]:: -> ndr1_0,c2_0
% 5.08/1.72 856:15:5:[3.0,605.5]:TopTopTopTopTop: c2_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c10_1(x0),c1_1(x0),c5_2(x2,x3),c6_2(x2,x3),c9_2(x2,x3),ndr1_1(x2),c8_2(x2,x4),c2_2(x2,x4) -> c10_2(x0,x1),c7_2(x2,x4),c4_1(x2),c3_0
% 5.08/1.72 855:15:5:[606.1,604.6]:TopTopTopTopTop: c5_2(x0,x1),c4_2(x0,x1),c6_2(x0,x1),ndr1_1(x0),c4_1(x0),c1_1(x0),ndr1_1(x2),c2_2(x2,x3),c9_1(x2) -> c10_2(x2,x4),c4_2(x2,x4),c3_2(x2,x4),c8_2(x2,x3),c1_2(x2,x3),c2_0
% 5.08/1.72 854:12:4:[606.1,603.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_2(x2,x3),c8_2(x2,x3),ndr1_1(x2),c9_1(x2),c10_1(x2),c6_2(a320,a321) -> c1_2(x0,x1),c8_2(x0,x1),c5_2(x2,x3)
% 5.08/1.72 853:12:4:[606.1,602.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_2(x2,x3),c8_2(x2,x3),ndr1_1(x2),c9_1(x2),c10_1(x2),c2_2(a320,a322) -> c1_2(x0,x1),c8_2(x0,x1),c5_2(x2,x3)
% 5.08/1.72 852:12:4:[606.1,601.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_2(x2,x3),c8_2(x2,x3),ndr1_1(x2),c9_1(x2),c10_1(x2),c7_2(a320,a322) -> c1_2(x0,x1),c8_2(x0,x1),c5_2(x2,x3)
% 5.08/1.72 851:13:4:[606.1,600.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2),c2_2(a375,a376) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3)
% 5.08/1.72 850:13:4:[606.1,599.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2),c6_2(a375,a377) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3)
% 5.08/1.72 849:13:4:[606.1,598.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2),c8_2(a375,a377) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3)
% 5.08/1.72 848:12:4:[606.1,597.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_2(x2,x3),c8_2(x2,x3),ndr1_1(x2),c9_1(x2),c10_1(x2) -> c1_2(x0,x1),c8_2(x0,x1),c5_2(x2,x3),c2_2(a320,a321)
% 5.08/1.72 847:13:4:[606.1,596.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3),c1_2(a375,a376)
% 5.08/1.72 846:13:4:[606.1,595.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3),c7_2(a375,a376)
% 5.08/1.72 845:12:4:[606.1,594.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_2(x2,x3),c8_2(x2,x3),ndr1_1(x2),c9_1(x2),c10_1(x2) -> c1_2(x0,x1),c8_2(x0,x1),c5_2(x2,x3),c6_1(a320)
% 5.08/1.72 844:12:4:[606.1,593.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_2(x2,x3),c8_2(x2,x3),ndr1_1(x2),c9_1(x2),c10_1(x2) -> c1_2(x0,x1),c8_2(x0,x1),c5_2(x2,x3),ndr1_1(a320)
% 5.08/1.72 843:11:3:[606.1,592.6]:TopTopTop: c2_2(x0,x1),c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c4_1(x0),c2_1(x0),c5_2(a327,x2),ndr1_1(a327) -> c7_2(a327,x2),c6_2(a327,x2),c5_0
% 5.08/1.72 842:13:4:[606.1,591.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3),c8_1(a375)
% 5.08/1.72 841:13:4:[606.1,590.3]:TopTopTopTop: c6_2(x0,x1),ndr1_1(x0),c9_1(x0),ndr1_1(x2),c1_1(x2),c3_1(x2) -> c9_2(x0,x1),c2_2(x0,x1),c3_1(x0),c9_2(x2,x3),c3_2(x2,x3),c5_2(x2,x3),ndr1_1(a375)
% 5.08/1.72 840:12:4:[606.1,589.2]:TopTopTopTop: c3_2(x0,x1),ndr1_1(x0),c3_2(x2,x3),c10_2(x2,x3),c2_2(x2,x3),ndr1_1(x2),c10_1(x2),c4_1(x2) -> c7_2(x0,x1),c6_2(x0,x1),c4_1(x0),c1_0
% 5.08/1.72 839:12:4:[606.1,588.2]:TopTopTopTop: ndr1_1(x0),c10_2(x0,x1),c2_2(a317,x2),ndr1_1(a317) -> c9_2(x0,x3),c7_2(x0,x3),c4_2(x0,x3),c4_2(x0,x1),c3_1(x0),c6_2(a317,x2),c10_2(a317,x2),c8_0
% 5.08/1.72 838:10:3:[606.1,587.6]:TopTopTop: c7_2(x0,x1),c2_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c7_2(x0,x2),c7_2(a269,a270) -> c3_2(x0,x2),c6_1(x0),c9_0
% 5.08/1.72 608:2:0:[7.1,240.1]:: c10_0 -> c9_0
% 5.08/1.72 837:10:3:[606.1,586.6]:TopTopTop: c7_2(x0,x1),c2_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c7_2(x0,x2),c3_2(a269,a270) -> c3_2(x0,x2),c6_1(x0),c9_0
% 5.08/1.72 609:2:0:[608.2,291.1]:: c10_0 -> ndr1_1(a420)
% 5.08/1.72 610:2:0:[608.2,292.1]:: c10_0 -> c7_1(a420)
% 5.08/1.72 611:3:1:[606.1,320.0]:Top: -> ndr1_1(x0),c5_1(x0),ssSkC8
% 5.08/1.72 836:10:3:[606.1,585.6]:TopTopTop: c7_2(x0,x1),c2_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c7_2(x0,x2) -> c3_2(x0,x2),c6_1(x0),c9_2(a269,a270),c9_0
% 5.08/1.72 835:10:3:[606.1,584.6]:TopTopTop: c7_2(x0,x1),c2_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c7_2(x0,x2) -> c3_2(x0,x2),c6_1(x0),c4_1(a269),c9_0
% 5.08/1.72 834:10:3:[606.1,583.6]:TopTopTop: c7_2(x0,x1),c2_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c7_2(x0,x2) -> c3_2(x0,x2),c6_1(x0),c2_1(a269),c9_0
% 5.08/1.72 612:2:0:[608.2,325.1]:: c10_0 -> c7_2(a420,a421)
% 5.08/1.72 613:2:0:[608.2,326.1]:: c10_0 -> c10_2(a420,a421)
% 5.08/1.72 614:2:0:[608.2,327.2]:: c8_1(a420),c10_0 ->
% 5.08/1.72 615:3:1:[606.1,338.0]:Top: c10_0 -> c7_1(x0),c4_1(x0)
% 5.08/1.72 616:3:1:[606.1,339.2]:Top: ssSkC35,c10_1(x0) -> c2_1(a431)
% 5.08/1.72 617:3:1:[606.1,340.2]:Top: ssSkC35,c10_1(x0) -> c6_1(a431)
% 5.08/1.72 618:3:1:[606.1,341.0]:Top: -> c10_2(x0,a318),c5_1(x0),ssSkC8
% 5.08/1.72 619:3:1:[606.1,342.0]:Top: -> c7_2(x0,a318),c5_1(x0),ssSkC8
% 5.08/1.72 620:3:1:[606.1,343.0]:Top: -> c3_2(x0,a318),c5_1(x0),ssSkC8
% 5.08/1.72 621:2:0:[608.2,344.2]:: c3_2(a420,a421),c10_0 ->
% 5.08/1.72 623:3:1:[70.1,347.0,606.1,622.1]:Top: c4_0 -> ndr1_1(x0),c8_0
% 5.08/1.72 624:4:1:[606.1,349.0]:Top: -> ndr1_1(x0),c9_1(x0),c3_1(x0),ssSkC25
% 5.08/1.72 627:2:1:[66.1,350.0,65.1,625.1,606.1,626.2]:Top: -> ndr1_1(x0),ssSkC23
% 5.08/1.72 628:4:1:[606.1,351.0]:Top: -> ndr1_1(x0),c8_1(x0),c7_1(x0),ssSkC12
% 5.08/1.72 629:3:1:[606.1,352.2]:Top: ssSkC35,c10_1(x0),c4_1(a431) ->
% 5.08/1.72 630:5:1:[606.1,353.2]:Top: ssSkC5,ssSkC6 -> ndr1_1(x0),c3_1(x0),c7_1(x0)
% 5.08/1.72 631:5:1:[606.1,354.2]:Top: ssSkC2,ssSkC3 -> ndr1_1(x0),c9_1(x0),c8_1(x0)
% 5.08/1.72 632:4:1:[606.1,355.1]:Top: c2_1(x0) -> c8_1(x0),ndr1_1(a287),c2_0
% 5.08/1.72 633:4:1:[606.1,356.1]:Top: c4_1(x0) -> ndr1_1(x0),c5_1(x0),ssSkC35
% 5.08/1.72 634:4:1:[606.1,357.1]:Top: c2_1(x0) -> ndr1_1(x0),c9_1(x0),ssSkC29
% 5.08/1.72 635:4:1:[606.1,358.0]:Top: -> c8_2(x0,a399),c9_1(x0),c3_1(x0),ssSkC25
% 5.08/1.72 636:4:1:[606.1,359.0]:Top: -> c3_2(x0,a399),c9_1(x0),c3_1(x0),ssSkC25
% 5.08/1.72 637:4:1:[606.1,360.2]:Top: ssSkP4(x0),ssSkP5(x0) -> c6_2(x0,a393),ssSkC23
% 5.08/1.72 638:4:1:[606.1,361.1]:Top: c9_1(x0) -> ndr1_1(x0),c3_1(x0),ssSkC22
% 5.08/1.72 639:4:1:[606.1,362.1]:Top: c1_1(x0) -> ndr1_1(x0),c7_1(x0),ssSkC15
% 5.08/1.72 640:4:1:[606.1,363.1]:Top: c9_1(x0),c7_0 -> ndr1_1(x0),c10_1(x0)
% 5.08/1.72 641:5:1:[606.1,364.3]:Top: ssSkC33,ssSkC34,c9_1(x0) -> ndr1_1(x0),c1_1(x0)
% 5.08/1.72 642:5:1:[606.1,365.2]:Top: ssSkC5,ssSkC6 -> c5_2(x0,a312),c3_1(x0),c7_1(x0)
% 5.08/1.72 643:5:1:[606.1,366.2]:Top: ssSkC5,ssSkC6 -> c2_2(x0,a312),c3_1(x0),c7_1(x0)
% 5.08/1.72 644:5:1:[606.1,367.2]:Top: ssSkC2,ssSkC3 -> c9_2(x0,a299),c9_1(x0),c8_1(x0)
% 5.08/1.72 645:5:1:[606.1,368.2]:Top: ssSkC2,ssSkC3 -> c8_2(x0,a299),c9_1(x0),c8_1(x0)
% 5.08/1.72 647:4:1:[93.1,369.0,2.0,646.1]:Top: c1_0 -> ndr1_1(x0),c1_1(x0),c7_0
% 5.08/1.72 648:4:1:[606.1,370.1]:Top: c3_1(x0),c2_0,c8_0 -> ndr1_1(x0)
% 5.08/1.72 649:4:1:[606.1,371.2]:Top: ssSkP2(x0),c2_2(x0,a380),c4_0 -> c8_0
% 5.08/1.72 650:4:1:[606.1,372.2]:Top: ssSkP2(x0),c1_2(x0,a380),c4_0 -> c8_0
% 5.08/1.72 651:4:1:[606.1,373.2]:Top: ssSkP2(x0),c4_2(x0,a380),c4_0 -> c8_0
% 5.08/1.72 652:4:1:[606.1,374.1]:Top: c2_1(x0) -> c8_1(x0),c5_2(a287,a290),c2_0
% 5.08/1.72 653:4:1:[606.1,375.1]:Top: c2_1(x0) -> c8_1(x0),c8_2(a287,a289),c2_0
% 5.08/1.72 654:4:1:[606.1,376.1]:Top: c2_1(x0) -> c8_1(x0),c4_2(a287,a288),c2_0
% 5.08/1.72 655:3:1:[52.0,377.1]:Top: c6_2(a272,x0) -> c1_2(a272,x0),c4_0
% 5.08/1.72 656:4:1:[606.1,378.1]:Top: c4_1(x0) -> c6_2(x0,a430),c5_1(x0),ssSkC35
% 5.08/1.72 657:4:1:[606.1,379.1]:Top: c4_1(x0) -> c2_2(x0,a430),c5_1(x0),ssSkC35
% 5.08/1.72 658:4:1:[606.1,380.1]:Top: c2_1(x0) -> c10_2(x0,a407),c9_1(x0),ssSkC29
% 5.08/1.72 659:4:1:[606.1,381.1]:Top: c2_1(x0) -> c5_2(x0,a407),c9_1(x0),ssSkC29
% 5.08/1.72 660:4:1:[606.1,382.2]:Top: c10_1(x0),c2_1(x0) -> ndr1_1(x0),ssSkC26
% 5.08/1.72 661:4:1:[606.1,383.1]:Top: c9_2(x0,a399) -> c9_1(x0),c3_1(x0),ssSkC25
% 5.08/1.72 662:4:1:[606.1,384.3]:Top: ssSkP4(x0),ssSkP5(x0),c8_2(x0,a393) -> ssSkC23
% 5.08/1.72 663:4:1:[606.1,385.3]:Top: ssSkP4(x0),ssSkP5(x0),c3_2(x0,a393) -> ssSkC23
% 5.08/1.72 664:4:1:[606.1,386.1]:Top: c1_1(x0) -> c5_2(x0,a354),c7_1(x0),ssSkC15
% 5.08/1.72 665:4:1:[606.1,387.1]:Top: c1_1(x0) -> c9_2(x0,a354),c7_1(x0),ssSkC15
% 5.08/1.72 666:4:1:[606.1,388.1]:Top: c1_1(x0) -> c4_2(x0,a354),c7_1(x0),ssSkC15
% 5.08/1.72 667:4:1:[606.1,389.1]:Top: c8_2(x0,a337) -> c8_1(x0),c7_1(x0),ssSkC12
% 5.08/1.72 668:4:1:[606.1,390.1]:Top: c4_2(x0,a337) -> c8_1(x0),c7_1(x0),ssSkC12
% 5.08/1.72 669:4:1:[606.1,391.1]:Top: c9_1(x0),c7_0 -> c1_2(x0,a440),c10_1(x0)
% 5.08/1.72 670:4:1:[606.1,392.1]:Top: c9_1(x0),c7_0 -> c6_2(x0,a440),c10_1(x0)
% 5.08/1.72 671:5:1:[606.1,393.3]:Top: ssSkC33,ssSkC34,c9_1(x0) -> c7_2(x0,a429),c1_1(x0)
% 5.08/1.72 673:4:1:[61.1,394.0,606.1,672.3]:Top: ssSkC30,c5_1(x0),c10_0 -> ndr1_1(x0)
% 5.08/1.72 675:4:1:[67.1,395.0,606.1,674.3]:Top: ssSkC22,c6_1(x0),c4_0 -> ndr1_1(x0)
% 5.08/1.72 676:5:1:[606.1,396.2]:Top: ssSkC21,c10_1(x0),c2_0 -> ndr1_1(x0),c5_1(x0)
% 5.08/1.72 677:5:1:[606.1,397.2]:Top: ssSkC13,c7_1(x0),c6_0 -> ndr1_1(x0),c9_1(x0)
% 5.08/1.72 678:5:1:[1.0,398.3]:Top: ssSkC12,c4_1(x0),c10_1(x0) -> ndr1_1(x0),c10_0
% 5.08/1.72 679:5:1:[2.0,399.3]:Top: ssSkC11,c10_1(x0),c1_1(x0) -> ndr1_1(x0),c7_0
% 5.08/1.72 680:5:1:[606.1,400.0]:Top: c7_0,c4_0 -> ndr1_1(x0),c3_1(x0),c6_1(x0)
% 5.08/1.72 681:5:1:[606.1,401.3]:Top: ssSkC5,ssSkC6,c4_2(x0,a312) -> c3_1(x0),c7_1(x0)
% 5.08/1.72 682:5:1:[606.1,402.3]:Top: ssSkC2,ssSkC3,c3_2(x0,a299) -> c9_1(x0),c8_1(x0)
% 5.08/1.72 683:5:1:[606.1,403.1]:Top: c2_1(x0) -> c3_1(x0),c8_1(x0),ndr1_1(a294),c6_0
% 5.08/1.72 684:4:1:[606.1,404.1]:Top: c3_1(x0),c2_0,c8_0 -> c9_2(x0,a426)
% 5.08/1.72 685:4:1:[606.1,405.1]:Top: c3_1(x0),c2_0,c8_0 -> c4_2(x0,a426)
% 5.08/1.72 686:4:1:[606.1,409.1]:Top: c2_1(x0),c3_2(a287,a290) -> c8_1(x0),c2_0
% 5.08/1.72 687:4:1:[606.1,410.1]:Top: c2_1(x0),c9_2(a287,a290) -> c8_1(x0),c2_0
% 5.08/1.72 688:4:1:[606.1,411.1]:Top: c2_1(x0),c6_2(a287,a289) -> c8_1(x0),c2_0
% 5.08/1.72 689:4:1:[606.1,412.1]:Top: c2_1(x0),c6_2(a287,a288) -> c8_1(x0),c2_0
% 5.08/1.72 690:4:1:[606.1,414.2]:Top: c10_2(x0,a430),c4_1(x0) -> c5_1(x0),ssSkC35
% 5.08/1.72 691:4:1:[606.1,415.2]:Top: c2_2(x0,a407),c2_1(x0) -> c9_1(x0),ssSkC29
% 5.08/1.72 692:4:1:[606.1,416.2]:Top: c10_1(x0),c2_1(x0) -> c7_2(x0,a402),ssSkC26
% 5.08/1.72 693:4:1:[606.1,417.2]:Top: c7_2(x0,a388),c9_1(x0) -> c3_1(x0),ssSkC22
% 5.08/1.72 694:4:1:[606.1,418.2]:Top: c9_2(x0,a388),c9_1(x0) -> c3_1(x0),ssSkC22
% 5.08/1.72 695:4:1:[606.1,419.2]:Top: c4_2(x0,a388),c9_1(x0) -> c3_1(x0),ssSkC22
% 5.08/1.72 696:5:1:[606.1,420.2]:Top: c1_1(x0),c7_1(x0) -> c8_1(x0),c8_1(a444),c8_0
% 5.08/1.72 697:4:1:[606.1,421.2]:Top: c5_2(x0,a440),c9_1(x0),c7_0 -> c10_1(x0)
% 5.08/1.72 698:5:1:[606.1,422.4]:Top: ssSkC33,ssSkC34,c8_2(x0,a429),c9_1(x0) -> c1_1(x0)
% 5.08/1.72 699:5:1:[606.1,423.4]:Top: ssSkC33,ssSkC34,c5_2(x0,a429),c9_1(x0) -> c1_1(x0)
% 5.08/1.72 700:5:1:[606.1,424.3]:Top: ssSkP6(x0),ssSkC30,c5_1(x0),c10_0 -> c3_2(x0,a413)
% 5.08/1.72 701:5:1:[606.1,425.3]:Top: ssSkP3(x0),ssSkC22,c6_1(x0),c4_0 -> c9_2(x0,a390)
% 5.08/1.72 702:5:1:[606.1,426.2]:Top: ssSkC21,c10_1(x0),c2_0 -> c2_2(x0,a387),c5_1(x0)
% 5.08/1.72 703:5:1:[606.1,427.2]:Top: ssSkC13,c7_1(x0),c6_0 -> c1_2(x0,a342),c9_1(x0)
% 5.08/1.72 704:5:1:[606.1,428.2]:Top: ssSkC13,c7_1(x0),c6_0 -> c7_2(x0,a342),c9_1(x0)
% 5.08/1.72 705:5:1:[2.0,429.3]:Top: ssSkC11,c10_1(x0),c1_1(x0) -> c8_2(x0,a336),c7_0
% 5.08/1.72 706:5:1:[606.1,430.0]:Top: c7_0,c4_0 -> c8_2(x0,a328),c3_1(x0),c6_1(x0)
% 5.08/1.72 707:5:1:[606.1,431.0]:Top: c7_0,c4_0 -> c2_2(x0,a328),c3_1(x0),c6_1(x0)
% 5.08/1.72 708:5:1:[606.1,432.1]:Top: c2_1(x0) -> c3_1(x0),c8_1(x0),c3_2(a294,a295),c6_0
% 5.08/1.72 709:5:1:[606.1,433.1]:Top: c2_1(x0),c4_1(a294) -> c3_1(x0),c8_1(x0),c6_0
% 5.08/1.72 710:5:1:[2.0,434.2]:Top: ssSkP0(x0),c2_2(x0,a275),c1_0 -> c1_1(x0),c7_0
% 5.08/1.72 711:5:1:[2.0,435.2]:Top: ssSkP0(x0),c10_2(x0,a275),c1_0 -> c1_1(x0),c7_0
% 5.08/1.72 712:5:1:[2.0,436.2]:Top: ssSkP0(x0),c6_2(x0,a275),c1_0 -> c1_1(x0),c7_0
% 5.08/1.72 713:5:1:[3.0,437.2]:Top: c9_1(x0),c10_1(x0),c1_0 -> c7_1(x0),c3_0
% 5.08/1.72 714:4:1:[606.1,439.2]:Top: c3_2(x0,a426),c3_1(x0),c2_0,c8_0 ->
% 5.08/1.72 715:4:1:[606.1,440.3]:Top: c9_2(x0,a402),c10_1(x0),c2_1(x0) -> ssSkC26
% 5.08/1.72 716:4:1:[606.1,441.3]:Top: c2_2(x0,a402),c10_1(x0),c2_1(x0) -> ssSkC26
% 5.08/1.72 717:5:1:[606.1,442.4]:Top: ssSkP6(x0),ssSkC30,c4_2(x0,a413),c5_1(x0),c10_0 ->
% 5.08/1.72 718:5:1:[606.1,443.4]:Top: ssSkP6(x0),ssSkC30,c1_2(x0,a413),c5_1(x0),c10_0 ->
% 5.08/1.72 719:5:1:[606.1,444.4]:Top: ssSkP3(x0),ssSkC22,c5_2(x0,a390),c6_1(x0),c4_0 ->
% 5.08/1.72 720:5:1:[606.1,445.4]:Top: ssSkP3(x0),ssSkC22,c1_2(x0,a390),c6_1(x0),c4_0 ->
% 5.08/1.72 721:5:1:[606.1,446.3]:Top: ssSkC21,c6_2(x0,a387),c10_1(x0),c2_0 -> c5_1(x0)
% 5.08/1.72 722:5:1:[606.1,447.3]:Top: ssSkC21,c1_2(x0,a387),c10_1(x0),c2_0 -> c5_1(x0)
% 5.08/1.72 723:5:1:[606.1,448.3]:Top: ssSkC13,c2_2(x0,a342),c7_1(x0),c6_0 -> c9_1(x0)
% 5.08/1.72 724:5:1:[1.0,449.4]:Top: ssSkC12,c7_2(x0,a338),c4_1(x0),c10_1(x0) -> c10_0
% 5.08/1.72 725:5:1:[1.0,450.4]:Top: ssSkC12,c8_2(x0,a338),c4_1(x0),c10_1(x0) -> c10_0
% 5.08/1.72 726:5:1:[1.0,451.4]:Top: ssSkC12,c10_2(x0,a338),c4_1(x0),c10_1(x0) -> c10_0
% 5.08/1.72 727:5:1:[2.0,452.4]:Top: ssSkC11,c1_2(x0,a336),c10_1(x0),c1_1(x0) -> c7_0
% 5.08/1.72 728:5:1:[606.1,453.1]:Top: c1_2(x0,a328),c7_0,c4_0 -> c3_1(x0),c6_1(x0)
% 5.08/1.72 729:5:1:[606.1,455.1]:Top: c2_1(x0),c2_2(a294,a295) -> c3_1(x0),c8_1(x0),c6_0
% 5.08/1.72 730:5:1:[606.1,456.1]:Top: c2_1(x0),c1_2(a294,a295) -> c3_1(x0),c8_1(x0),c6_0
% 5.08/1.72 731:4:1:[60.0,459.1]:Top: c3_2(a414,x0) -> c7_2(a414,x0),c1_2(a414,x0),ssSkC31
% 5.08/1.72 732:4:1:[81.0,461.1]:Top: c1_2(a330,x0) -> c3_2(a330,x0),c2_2(a330,x0),ssSkC10
% 5.08/1.72 733:5:1:[99.2,465.3]:Top: ssSkC28,ssSkC29,c7_2(a408,x0) -> c8_2(a408,x0),c3_2(a408,x0)
% 5.08/1.72 734:5:1:[219.1,467.0]:Top: c9_0 -> c4_2(a384,x0),c8_2(a384,x0),c3_2(a384,x0),c4_0
% 5.08/1.72 736:5:2:[606.1,472.1,683.4,735.2]:TopTop: c2_1(x0) -> c3_1(x0),c8_1(x0),c7_2(a294,x1),c6_0
% 5.08/1.72 738:6:2:[90.1,473.0,606.1,737.4]:TopTop: ssSkC1,c1_1(x0),c4_1(x0) -> c7_1(x0),ndr1_1(x1),c9_1(x1)
% 5.08/1.72 739:4:1:[58.0,478.2]:Top: c9_2(a422,x0),c7_2(a422,x0) -> c5_2(a422,x0),ssSkC32
% 5.08/1.72 740:4:1:[73.0,479.2]:Top: c7_2(a367,x0),c1_2(a367,x0) -> c10_2(a367,x0),ssSkC19
% 5.08/1.72 741:4:1:[76.0,482.2]:Top: c2_2(a345,x0),c4_2(a345,x0) -> c6_2(a345,x0),ssSkC14
% 5.08/1.72 742:4:1:[86.0,483.2]:Top: c2_2(a300,x0),c7_2(a300,x0) -> c4_2(a300,x0),ssSkC4
% 5.08/1.72 743:5:1:[95.1,488.3]:Top: ssSkC36,c9_2(a436,x0),c3_2(a436,x0) -> c1_2(a436,x0),c8_0
% 5.08/1.72 744:5:1:[219.1,489.1]:Top: c5_2(a384,x0),c9_0 -> c2_2(a384,x0),c6_2(a384,x0),c4_0
% 5.08/1.72 745:7:2:[606.1,494.4]:TopTop: ssSkP1(x0),ssSkC1,c1_1(x1),c4_1(x1) -> c7_1(x1),c6_2(x0,a286),c9_1(x0)
% 5.08/1.72 746:4:1:[62.0,495.3]:Top: c10_2(a403,x0),c6_2(a403,x0),c4_2(a403,x0) -> ssSkC27
% 5.08/1.72 747:4:1:[83.0,496.3]:Top: c7_2(a313,x0),c4_2(a313,x0),c3_2(a313,x0) -> ssSkC7
% 5.08/1.72 748:5:1:[210.2,497.3]:Top: ssSkC31,c1_2(a416,x0),c5_2(a416,x0),c3_0 -> c4_2(a416,x0)
% 5.08/1.72 749:5:1:[230.2,498.3]:Top: ssSkC9,c6_2(a325,x0),c2_2(a325,x0),c5_0 -> c4_2(a325,x0)
% 5.08/1.72 750:5:1:[236.1,499.2]:Top: c7_2(a278,x0),c2_2(a278,x0),c7_0 -> c4_2(a278,x0),c6_0
% 5.08/1.72 751:7:2:[606.1,500.4]:TopTop: ssSkP1(x0),ssSkC1,c1_1(x1),c4_1(x1),c8_2(x0,a286) -> c7_1(x1),c9_1(x0)
% 5.08/1.72 752:7:2:[606.1,501.4]:TopTop: ssSkP1(x0),ssSkC1,c1_1(x1),c4_1(x1),c7_2(x0,a286) -> c7_1(x1),c9_1(x0)
% 5.08/1.72 753:5:1:[300.2,502.2]:Top: c9_2(a381,x0),c10_2(a381,x0),c4_0,c5_0 -> c8_2(a381,x0)
% 5.08/1.72 754:7:2:[606.1,503.1]:TopTop: ndr1_1(x0),c5_0,c4_0 -> c3_2(x0,x1),c5_2(x0,x1),c2_2(x0,a276),c6_1(x0)
% 5.08/1.72 755:7:2:[606.1,504.1]:TopTop: ndr1_1(x0),c5_0,c4_0 -> c3_2(x0,x1),c5_2(x0,x1),c8_2(x0,a276),c6_1(x0)
% 5.08/1.72 756:7:2:[606.1,505.2]:TopTop: c7_1(x0),c9_1(x0),c10_1(x1),c2_1(x1),c4_0 -> c10_1(x0),c3_1(x1)
% 5.08/1.72 757:5:1:[309.2,506.3]:Top: c8_2(a305,x0),c4_2(a305,x0),c10_2(a305,x0),c1_0,c9_0 ->
% 5.08/1.72 758:7:2:[606.1,507.2]:TopTop: ndr1_1(x0),c4_2(x0,a276),c5_0,c4_0 -> c3_2(x0,x1),c5_2(x0,x1),c6_1(x0)
% 5.08/1.72 759:7:2:[606.1,508.3]:TopTop: c4_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_0 -> c7_2(x0,x1),c6_2(x0,x1),c8_1(a364)
% 5.08/1.72 760:7:2:[606.1,509.3]:TopTop: c4_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_0 -> c7_2(x0,x1),c6_2(x0,x1),c9_1(a364)
% 5.08/1.72 761:7:2:[606.1,510.3]:TopTop: c10_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c10_0,c4_0 -> c4_2(x0,x1),c9_1(x0)
% 5.08/1.72 762:7:2:[606.1,511.3]:TopTop: c2_2(x0,x1),ndr1_1(x0),c10_2(x0,a428) -> c7_2(x0,x1),c1_2(x0,x1),c6_1(x0),ssSkC34
% 5.08/1.72 763:7:2:[606.1,512.3]:TopTop: c2_2(x0,x1),ndr1_1(x0),c1_2(x0,a428) -> c7_2(x0,x1),c1_2(x0,x1),c6_1(x0),ssSkC34
% 5.08/1.72 764:7:2:[606.1,513.3]:TopTop: c2_2(x0,x1),ndr1_1(x0),c8_2(x0,a428) -> c7_2(x0,x1),c1_2(x0,x1),c6_1(x0),ssSkC34
% 5.08/1.72 765:7:2:[606.1,514.3]:TopTop: c10_2(x0,x1),ndr1_1(x0),c1_1(x0) -> c6_2(x0,x1),c4_2(x0,x1),c3_2(x0,a411),ssSkC30
% 5.08/1.72 766:8:2:[606.1,515.3]:TopTop: c7_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c9_0 -> c9_2(x0,x1),c3_1(x0),c9_1(x0),c1_0
% 5.08/1.72 767:7:2:[606.1,516.4]:TopTop: c10_2(x0,x1),ndr1_1(x0),c7_2(x0,a411),c1_1(x0) -> c6_2(x0,x1),c4_2(x0,x1),ssSkC30
% 5.08/1.72 768:7:2:[606.1,517.4]:TopTop: c10_2(x0,x1),ndr1_1(x0),c2_2(x0,a411),c1_1(x0) -> c6_2(x0,x1),c4_2(x0,x1),ssSkC30
% 5.08/1.72 769:8:2:[606.1,518.4]:TopTop: ssSkP7(x0),c3_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c5_0 -> c10_2(x0,x1),c7_2(x0,a447),c4_0
% 5.08/1.72 770:8:2:[606.1,519.4]:TopTop: ssSkP7(x0),c3_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c5_0 -> c10_2(x0,x1),c3_2(x0,a447),c4_0
% 5.08/1.72 771:8:2:[606.1,520.4]:TopTop: ssSkC25,c7_2(x0,x1),ndr1_1(x0),c3_1(x0),c7_0 -> c5_2(x0,x1),c2_2(x0,x1),c2_2(x0,a400)
% 5.08/1.72 772:8:2:[3.0,521.3]:TopTop: c1_2(x0,x1),ndr1_1(x0),c3_1(x0),c7_0 -> c7_2(x0,x1),c6_2(x0,x1),c8_2(x0,a316),c3_0
% 5.08/1.72 773:8:2:[2.0,522.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c10_1(x0),c2_1(x0),c8_0 -> c10_2(x0,x1),c6_2(x0,x1),c7_0
% 5.08/1.72 774:8:2:[606.1,523.2]:TopTop: c1_1(x0),c7_1(x0),ndr1_1(a444) -> c8_1(x0),c10_2(a444,x1),c4_2(a444,x1),c2_2(a444,x1),c8_0
% 5.08/1.72 775:10:3:[606.1,524.2]:TopTopTop: ssSkC18,ndr1_1(x0),c10_1(x1) -> c2_2(x0,x2),c7_2(x0,x2),c10_2(x0,x2),c2_1(x0),c5_1(x0),ndr1_1(x1),c6_1(x1)
% 5.08/1.72 776:9:3:[606.1,525.2]:TopTopTop: ndr1_1(x0),c10_2(x0,x1) -> c9_2(x0,x2),c7_2(x0,x2),c4_2(x0,x2),c4_2(x0,x1),c3_1(x0),c5_1(a317),c8_0
% 5.08/1.72 777:9:3:[606.1,526.2]:TopTopTop: ndr1_1(x0),c10_2(x0,x1) -> c9_2(x0,x2),c7_2(x0,x2),c4_2(x0,x2),c4_2(x0,x1),c3_1(x0),c4_1(a317),c8_0
% 5.08/1.72 778:8:2:[606.1,527.5]:TopTop: ssSkP7(x0),c3_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c10_2(x0,a447),c5_0 -> c10_2(x0,x1),c4_0
% 5.08/1.72 779:8:2:[606.1,528.5]:TopTop: ssSkC25,c7_2(x0,x1),ndr1_1(x0),c8_2(x0,a400),c3_1(x0),c7_0 -> c5_2(x0,x1),c2_2(x0,x1)
% 5.08/1.72 780:8:2:[606.1,529.5]:TopTop: ssSkC25,c7_2(x0,x1),ndr1_1(x0),c7_2(x0,a400),c3_1(x0),c7_0 -> c5_2(x0,x1),c2_2(x0,x1)
% 5.08/1.72 781:9:3:[606.1,530.1]:TopTopTop: c5_1(x0),c2_2(x1,x2),ndr1_1(x1) -> c3_1(x0),c5_2(x1,x2),c3_2(x1,x2),c3_1(x1),c1_1(x1),ndr1_1(a365)
% 5.08/1.72 782:9:3:[606.1,531.1]:TopTopTop: c5_1(x0),c2_2(x1,x2),ndr1_1(x1) -> c3_1(x0),c5_2(x1,x2),c3_2(x1,x2),c3_1(x1),c1_1(x1),c7_1(a365)
% 5.08/1.72 783:9:3:[606.1,532.1]:TopTopTop: c5_1(x0),c2_2(x1,x2),ndr1_1(x1) -> c3_1(x0),c5_2(x1,x2),c3_2(x1,x2),c3_1(x1),c1_1(x1),c3_1(a365)
% 5.08/1.72 784:8:2:[3.0,533.4]:TopTop: c1_2(x0,x1),ndr1_1(x0),c3_2(x0,a316),c3_1(x0),c7_0 -> c7_2(x0,x1),c6_2(x0,x1),c3_0
% 5.08/1.72 785:8:2:[3.0,534.4]:TopTop: c1_2(x0,x1),ndr1_1(x0),c5_2(x0,a316),c3_1(x0),c7_0 -> c7_2(x0,x1),c6_2(x0,x1),c3_0
% 5.08/1.72 786:8:2:[606.1,535.6]:TopTop: ssSkC4,c8_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_1(x0) -> c9_2(x0,x1),ndr1_1(a302)
% 5.08/1.72 787:8:2:[606.1,536.6]:TopTop: ssSkC4,c8_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_1(x0) -> c9_2(x0,x1),c10_1(a302)
% 5.08/1.72 788:10:3:[606.1,537.2]:TopTopTop: ssSkC18,ndr1_1(x0),c10_1(x1) -> c2_2(x0,x2),c7_2(x0,x2),c10_2(x0,x2),c2_1(x0),c5_1(x0),c5_2(x1,a363),c6_1(x1)
% 5.08/1.72 789:10:3:[606.1,538.2]:TopTopTop: ssSkC18,ndr1_1(x0),c10_1(x1) -> c2_2(x0,x2),c7_2(x0,x2),c10_2(x0,x2),c2_1(x0),c5_1(x0),c4_2(x1,a363),c6_1(x1)
% 5.08/1.72 790:8:2:[606.1,539.4]:TopTop: c5_2(x0,x1),ndr1_1(x0),c5_2(x0,a419),c9_1(x0),c8_0,c4_0 -> c1_2(x0,x1),c6_2(x0,x1)
% 5.08/1.72 791:8:2:[606.1,540.4]:TopTop: c5_2(x0,x1),ndr1_1(x0),c1_2(x0,a419),c9_1(x0),c8_0,c4_0 -> c1_2(x0,x1),c6_2(x0,x1)
% 5.08/1.72 792:9:3:[606.1,541.1]:TopTopTop: c5_1(x0),c2_2(x1,x2),ndr1_1(x1) -> c3_1(x0),c5_2(x1,x2),c3_2(x1,x2),c3_1(x1),c1_1(x1),c1_2(a365,a366)
% 5.08/1.72 793:9:3:[606.1,542.1]:TopTopTop: c5_1(x0),c2_2(x1,x2),ndr1_1(x1) -> c3_1(x0),c5_2(x1,x2),c3_2(x1,x2),c3_1(x1),c1_1(x1),c4_2(a365,a366)
% 5.08/1.72 794:8:2:[606.1,543.6]:TopTop: c2_2(x0,x1),c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c4_1(x0),c2_1(x0) -> c2_1(a327),c5_0
% 5.08/1.72 795:8:2:[606.1,544.6]:TopTop: ssSkC4,c8_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_1(x0) -> c9_2(x0,x1),c6_2(a302,a303)
% 5.08/1.72 796:8:2:[606.1,545.6]:TopTop: ssSkC4,c8_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_1(x0),c7_1(a302) -> c9_2(x0,x1)
% 5.08/1.72 797:8:2:[606.1,546.2]:TopTop: c1_1(x0),c7_1(x0),c5_2(a444,x1),c10_2(a444,x1),ndr1_1(a444) -> c8_1(x0),c9_2(a444,x1),c8_0
% 5.08/1.72 798:9:3:[606.1,547.1]:TopTopTop: c5_1(x0),c2_2(x1,x2),ndr1_1(x1),c8_2(a365,a366) -> c3_1(x0),c5_2(x1,x2),c3_2(x1,x2),c3_1(x1),c1_1(x1)
% 5.08/1.72 799:8:2:[606.1,548.6]:TopTop: c2_2(x0,x1),c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c4_1(x0),c2_1(x0),c5_1(a327) -> c5_0
% 5.08/1.72 800:8:2:[606.1,549.6]:TopTop: ssSkC4,c8_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_1(x0),c5_2(a302,a303) -> c9_2(x0,x1)
% 5.08/1.72 801:9:3:[606.1,550.2]:TopTopTop: c4_1(x0),c8_1(x0),c4_2(x1,x2),ndr1_1(x1),c9_1(x1),c6_1(x1) -> c1_2(x1,x2),c6_2(x1,x2),c1_0
% 5.08/1.72 802:10:3:[606.1,551.4]:TopTopTop: c1_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c4_1(x0),c9_1(x2) -> c4_2(x0,x1),c1_1(x0),ndr1_1(x2),c1_1(x2),c6_0
% 5.08/1.72 803:9:3:[606.1,552.5]:TopTopTop: c10_2(x0,x1),ndr1_1(x0),c6_2(x0,x2),c9_2(x0,x2),c4_1(x0) -> c6_2(x0,x1),c1_2(x0,x2),c1_1(a401),c4_0
% 5.08/1.72 804:9:3:[3.0,553.5]:TopTopTop: c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2) -> c9_2(x0,x2),c8_2(x0,a383),c9_0,c3_0
% 5.08/1.72 805:10:3:[606.1,554.4]:TopTopTop: ssSkC16,c8_2(x0,x1),ndr1_1(x0),c1_2(x0,x2) -> c6_2(x0,x1),c5_2(x0,x1),c3_2(x0,x2),c7_2(x0,x2),c10_1(x0),ndr1_1(a358)
% 5.08/1.72 806:10:4:[606.1,555.4]:TopTopTopTop: ssSkC14,c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x2) -> c5_2(x0,x3),c1_2(x0,x3),c8_2(x0,x3),c9_1(x0),ndr1_1(x2)
% 5.08/1.72 807:10:3:[606.1,556.4]:TopTopTop: c1_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c4_1(x0),c9_1(x2) -> c4_2(x0,x1),c1_1(x0),c7_2(x2,a439),c1_1(x2),c6_0
% 5.08/1.72 808:9:3:[606.1,557.5]:TopTopTop: c10_2(x0,x1),ndr1_1(x0),c6_2(x0,x2),c9_2(x0,x2),c4_1(x0),c6_1(a401) -> c6_2(x0,x1),c1_2(x0,x2),c4_0
% 5.08/1.72 809:9:3:[3.0,558.6]:TopTopTop: c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c3_2(x0,a383) -> c9_2(x0,x2),c9_0,c3_0
% 5.08/1.72 810:9:3:[3.0,559.6]:TopTopTop: c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c9_2(x0,a383) -> c9_2(x0,x2),c9_0,c3_0
% 5.08/1.72 811:10:3:[606.1,560.5]:TopTopTop: ssSkC19,c6_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c7_2(x0,x2) -> c1_2(x0,x1),c4_2(x0,x2),c5_2(x0,x2),c6_1(x0),ndr1_1(a369)
% 5.08/1.72 812:9:3:[606.1,561.3]:TopTopTop: c4_2(x0,x1),ndr1_1(x0),c3_1(x0),ndr1_1(a364),c6_0 -> c7_2(x0,x1),c6_2(x0,x1),c4_2(a364,x2),c2_2(a364,x2)
% 5.08/1.72 813:10:3:[606.1,562.4]:TopTopTop: ssSkC16,c8_2(x0,x1),ndr1_1(x0),c1_2(x0,x2) -> c6_2(x0,x1),c5_2(x0,x1),c3_2(x0,x2),c7_2(x0,x2),c10_1(x0),c5_2(a358,a359)
% 5.08/1.72 814:10:3:[606.1,563.4]:TopTopTop: ssSkC16,c8_2(x0,x1),ndr1_1(x0),c1_2(x0,x2) -> c6_2(x0,x1),c5_2(x0,x1),c3_2(x0,x2),c7_2(x0,x2),c10_1(x0),c10_2(a358,a359)
% 5.08/1.72 815:10:3:[606.1,564.4]:TopTopTop: ssSkC16,c8_2(x0,x1),ndr1_1(x0),c1_2(x0,x2),c3_1(a358) -> c6_2(x0,x1),c5_2(x0,x1),c3_2(x0,x2),c7_2(x0,x2),c10_1(x0)
% 5.08/1.72 816:10:3:[606.1,565.4]:TopTopTop: ssSkC16,c8_2(x0,x1),ndr1_1(x0),c1_2(x0,x2),c8_1(a358) -> c6_2(x0,x1),c5_2(x0,x1),c3_2(x0,x2),c7_2(x0,x2),c10_1(x0)
% 5.08/1.72 817:10:4:[606.1,566.4]:TopTopTopTop: ssSkC14,c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x2) -> c5_2(x0,x3),c1_2(x0,x3),c8_2(x0,x3),c9_1(x0),c10_2(x2,a347)
% 5.08/1.72 818:10:4:[606.1,567.4]:TopTopTopTop: ssSkC14,c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x2) -> c5_2(x0,x3),c1_2(x0,x3),c8_2(x0,x3),c9_1(x0),c7_2(x2,a347)
% 5.08/1.72 819:10:3:[606.1,568.4]:TopTopTop: c9_2(x0,x1),ndr1_1(x0),c8_1(x0),c1_1(x0),c5_1(x2),c1_0 -> c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x2),c10_1(x2)
% 5.08/1.72 820:10:3:[606.1,569.3]:TopTopTop: c10_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c6_0,c4_0 -> c3_2(x0,x1),c7_2(x0,x2),c10_2(x0,x2),c2_2(x0,x2),c8_1(x0)
% 5.08/1.72 821:10:3:[606.1,570.4]:TopTopTop: c1_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c4_1(x0),c5_2(x2,a439),c9_1(x2) -> c4_2(x0,x1),c1_1(x0),c1_1(x2),c6_0
% 5.08/1.72 822:10:3:[606.1,571.5]:TopTopTop: ssSkC19,c6_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c7_2(x0,x2) -> c1_2(x0,x1),c4_2(x0,x2),c5_2(x0,x2),c6_1(x0),c3_2(a369,a370)
% 5.08/1.72 823:10:3:[606.1,572.5]:TopTopTop: ssSkC19,c6_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c2_1(a369) -> c1_2(x0,x1),c4_2(x0,x2),c5_2(x0,x2),c6_1(x0)
% 5.08/1.72 824:10:3:[606.1,573.5]:TopTopTop: ssSkC19,c6_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c1_1(a369) -> c1_2(x0,x1),c4_2(x0,x2),c5_2(x0,x2),c6_1(x0)
% 5.08/1.72 825:10:3:[606.1,574.4]:TopTopTop: ssSkC16,c8_2(x0,x1),ndr1_1(x0),c1_2(x0,x2),c2_2(a358,a359) -> c6_2(x0,x1),c5_2(x0,x1),c3_2(x0,x2),c7_2(x0,x2),c10_1(x0)
% 5.08/1.72 826:10:4:[606.1,575.4]:TopTopTopTop: ssSkC14,c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c1_2(x2,a347),c4_1(x2) -> c5_2(x0,x3),c1_2(x0,x3),c8_2(x0,x3),c9_1(x0)
% 5.08/1.72 827:10:3:[606.1,576.4]:TopTopTop: c9_2(x0,x1),ndr1_1(x0),c8_1(x0),c1_1(x0),c5_1(x2),c1_0 -> c5_2(x0,x1),c3_2(x0,x1),c2_2(x2,a304),c10_1(x2)
% 5.08/1.72 828:10:3:[606.1,577.4]:TopTopTop: c9_2(x0,x1),ndr1_1(x0),c8_1(x0),c1_1(x0),c5_1(x2),c1_0 -> c5_2(x0,x1),c3_2(x0,x1),c6_2(x2,a304),c10_1(x2)
% 5.08/1.72 829:10:3:[606.1,578.4]:TopTopTop: c7_2(x0,x1),ndr1_1(x0),c5_2(x0,x2),c8_1(x0),c6_0,c8_0 -> c10_2(x0,x1),c2_2(x0,x1),c2_2(x0,x2),c9_2(x0,x2)
% 5.08/1.72 830:10:3:[606.1,579.5]:TopTopTop: ssSkC19,c6_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c4_2(a369,a370) -> c1_2(x0,x1),c4_2(x0,x2),c5_2(x0,x2),c6_1(x0)
% 5.08/1.72 831:10:3:[606.1,580.5]:TopTopTop: ssSkC19,c6_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c9_2(a369,a370) -> c1_2(x0,x1),c4_2(x0,x2),c5_2(x0,x2),c6_1(x0)
% 5.08/1.72 832:10:3:[606.1,581.4]:TopTopTop: c9_2(x0,x1),ndr1_1(x0),c8_1(x0),c1_1(x0),c4_2(x2,a304),c5_1(x2),c1_0 -> c5_2(x0,x1),c3_2(x0,x1),c10_1(x2)
% 5.08/1.72 833:10:3:[606.1,582.6]:TopTopTop: c7_2(x0,x1),c2_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c7_2(x0,x2) -> c3_2(x0,x2),c6_1(x0),ndr1_1(a269),c9_0
% 5.08/1.72
% 5.08/1.72 Most General Atoms: ndr1_0 c10_0 c7_0 c3_0 c5_0 c4_0 c9_0 c6_0 ssSkC38 ssSkC37 ssSkC36 ssSkC33 ssSkC32 ssSkC31 ssSkC28 ssSkC27 ssSkC24 ssSkC21 ssSkC20 ssSkC19 ssSkC18 ssSkC17 ssSkC16 ssSkC14 ssSkC13 ssSkC11 ssSkC10 ssSkC9 ssSkC7 ssSkC6 ssSkC5 ssSkC4 ssSkC3 ssSkC2 ssSkC1 ssSkC0 c2_0 ssSkP7(x0) ssSkP6(x0) ssSkP5(x0) ssSkP4(x0) ssSkP3(x0) ssSkP2(x0) ssSkP1(x0) ssSkP0(x0) c8_0 ssSkC29 ssSkC26 ssSkC23 c1_0 ssSkC8 c10_2(x0,x2) c7_2(x0,x2) ssSkC15 ssSkC35 ssSkC25 c8_1(x0) ssSkC12 ssSkC22 ssSkC34 ssSkC30 ndr1_1(x1) c9_1(x1) c1_1(x1) c4_1(x1) c7_1(x1) c10_1(x1) c2_1(x1) c3_1(x1) c6_1(x1) c9_2(x0,x2) c2_2(x1,x2) c3_2(x1,x2) c4_2(x1,x2) c6_2(x0,x2) c1_2(x0,x3) c8_2(x0,x3) c5_2(x0,x2) c5_1(x2)
% 5.08/1.72
% 5.08/1.72 === Starting SPASS-SCL-FOL A Little Less Naive, considering 685 atoms initially, heuristics mode: lmodel_grow ===
% 5.08/1.72
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 749
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 801
% 5.08/1.72 === Conflict found: 624:4:1:[606.1,349.0]:Top: -> ndr1_1(x0),c9_1(x0),c3_1(x0),ssSkC25 {x0 -> a329}
% 5.08/1.72 === Backtracking. Learning clause 857:4:1:[624.2,638.1]:Top: -> ssSkC25,ndr1_1(x0),c3_1(x0),ssSkC22
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 828
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 845
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 863
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 875
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 886
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 891
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 896
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 899
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 901
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 903
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 906
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 908
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 909
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 912
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 914
% 5.08/1.72 === Clause set with instances from active satisfied. Growing active. New size: 916
% 5.08/1.72
% 5.08/1.72 Linear Model Building succeeded.
% 5.08/1.72 SZS status Satisfiable
% 5.08/1.72
% 5.08/1.72 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.08/1.72
% 5.08/1.72 SPASS-SCL-FOL Statistics:
% 5.08/1.72 Number of learned clauses: 1
% 5.08/1.72 Number of propagations: 188
% 5.08/1.72 Number of decisions: 1212
% 5.08/1.72 Number of resolutions: 1
% 5.08/1.72 Number of condensations: 0
% 5.08/1.72 Number of sub resolutions: 251
% 5.08/1.72 Number of input literals (deduplicated): 685
% 5.08/1.72 Number of grows: 18
% 5.08/1.72 Number of considered ground atoms: 916
% 5.08/1.72
% 5.08/1.72 Needed: 0:00:01.17
% 5.08/1.72
%------------------------------------------------------------------------------