%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN422-1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 61.72s 12.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN422-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n007.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:41:09 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 61.72/12.86 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/12.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/12.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/12.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/12.86 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/12.86 Execution lmodel_grow ended with status: satisfiable
% 61.72/12.86 Used heuristic: lmodel_grow
% 61.72/12.86
% 61.72/12.86 Input Clauses:
% 61.72/12.86
% 61.72/12.86 Predicates: ndr1_0 c7_0 c2_0 c9_0 c3_0 c5_0 c8_0 ssSkC35 ssSkC31 ssSkC30 ssSkC29 ssSkC27 ssSkC21 ssSkC20 ssSkC19 ssSkC18 ssSkC17 ssSkC16 ssSkC15 ssSkC14 ssSkC13 ssSkC12 ssSkC11 ssSkC10 ssSkC9 ssSkC8 ssSkC7 ssSkC6 ssSkC3 ssSkC2 ssSkC1 ssSkC0 c1_0 c6_1 ssSkC33 ssSkC34 c10_0 ssSkC23 ssSkC24 ssSkC4 c4_0 c6_0 c5_1 c10_1 ndr1_1 ssSkP11 ssSkP10 ssSkP9 c1_1 ssSkP8 ssSkP7 ssSkP6 c8_1 c4_1 ssSkP5 ssSkP4 ssSkP3 ssSkP2 c9_1 c7_1 ssSkP1 c2_1 ssSkP0 c3_1 ssSkC28 ssSkC25 ssSkC5 c7_2 c6_2 c10_2 c2_2 c1_2 c3_2 c9_2 c8_2 c5_2 c4_2 ssSkC22 ssSkC32 ssSkC26
% 61.72/12.86 Fol Constants: a756 a757 a741 a734 a728 a707 a703 a692 a670 a663 a660 a655 a649 a641 a631 a621 a617 a611 a758 a753 a740 a721 a697 a695 a658 a645 a630 a625 a749 a742 a739 a736 a735 a731 a715 a712 a705 a700 a696 a693 a684 a682 a676 a675 a668 a665 a661 a651 a642 a635 a632 a609 a759 a754 a745 a737 a729 a724 a723 a708 a701 a698 a686 a679 a672 a669 a656 a647 a628 a626 a622 a618 a614 a608 a743 a718 a694 a644 a643 a612 a760 a746 a738 a733 a730 a725 a702 a699 a688 a687 a681 a680 a657 a646 a629 a623 a616 a615 a713 a720 a624 a690 a662 a752 a732 a719 a666 a613 a706 a691 a685 a677 a650 a627 a683 a637 a748 a722 a747 a744 a678 a654 a638 a751 a726 a671 a648 a750 a717 a714 a673 a633 a755 a674 a634 a619 a659 a664 a652 a667 a653 a727 a610 a709 a639 a704 a710 a640 a716 a636 a711 a620
% 61.72/12.86 Fol Functions:
% 61.72/12.86 Problem Properties:
% 61.72/12.86 This is a Bernays Schoenfinkel problem.
% 61.72/12.86
% 61.72/12.86 After reduction: Problem Properties:
% 61.72/12.86 This is a Bernays Schoenfinkel problem.
% 61.72/12.86
% 61.72/12.86
% 61.72/12.86 Reduced Input Clauses:
% 61.72/12.86 530:2:0:[5.1,30.0]:: -> ndr1_0,c1_0
% 61.72/12.86 531:2:0:[7.1,33.0]:: -> ndr1_0,c10_0
% 61.72/12.86 532:2:0:[10.1,35.0]:: -> ndr1_0,c2_0
% 61.72/12.86 533:2:0:[14.1,36.0]:: -> ndr1_0,c3_0
% 61.72/12.86 751:14:5:[538.1,529.6]:TopTopTopTopTop: c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c10_2(x0,x2),c5_1(x0),c3_2(x3,x4),ndr1_1(x3),c4_2(x3,a620) -> c7_2(x0,x1),c9_2(x0,x2),c1_2(x3,x4),c6_2(x3,x4),c9_0
% 61.72/12.86 534:2:0:[17.1,38.0]:: -> ndr1_0,c5_0
% 61.72/12.86 750:14:5:[538.1,528.6]:TopTopTopTopTop: c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c10_2(x0,x2),c5_1(x0),c3_2(x3,x4),ndr1_1(x3) -> c7_2(x0,x1),c9_2(x0,x2),c1_2(x3,x4),c6_2(x3,x4),c5_2(x3,a620),c9_0
% 61.72/12.86 535:2:0:[39.0,41.1]:: -> ndr1_0,c2_0
% 61.72/12.86 536:2:0:[39.0,42.2]:: ssSkC4 -> ndr1_0
% 61.72/12.86 538:1:0:[1.1,87.0,39.0,537.2]:: -> ndr1_0
% 61.72/12.86 540:1:0:[8.1,89.0,1.1,539.1]:: -> ndr1_0
% 61.72/12.86 749:14:5:[538.1,527.6]:TopTopTopTopTop: c6_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c10_2(x0,x2),c5_1(x0),c3_2(x3,x4),ndr1_1(x3) -> c7_2(x0,x1),c9_2(x0,x2),c1_2(x3,x4),c6_2(x3,x4),c1_2(x3,a620),c9_0
% 61.72/12.86 748:12:4:[538.1,526.7]:TopTopTopTop: c7_2(x0,x1),c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c5_2(x0,x2),c2_2(x0,x2),c2_2(x3,a711),c7_1(x3),c5_0 -> c8_1(x0),c5_1(x3)
% 61.72/12.86 747:12:4:[538.1,525.7]:TopTopTopTop: c7_2(x0,x1),c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c5_2(x0,x2),c2_2(x0,x2),c10_2(x3,a711),c7_1(x3),c5_0 -> c8_1(x0),c5_1(x3)
% 61.72/12.86 746:13:4:[533.1,524.6]:TopTopTopTop: ssSkP0(x0),c9_2(x1,x2),c8_2(x1,x2),ndr1_1(x1),c4_1(x1),c3_1(x1),c10_2(x0,x3),ndr1_1(x0),c4_2(x0,a636) -> c2_2(x1,x2),c5_2(x0,x3),c8_2(x0,x3),c3_0
% 61.72/12.86 745:12:4:[538.1,523.7]:TopTopTopTop: c7_2(x0,x1),c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c5_2(x0,x2),c2_2(x0,x2),c7_1(x3),c5_0 -> c8_1(x0),c8_2(x3,a711),c5_1(x3)
% 61.72/12.86 744:13:4:[533.1,522.6]:TopTopTopTop: ssSkP0(x0),c9_2(x1,x2),c8_2(x1,x2),ndr1_1(x1),c4_1(x1),c3_1(x1),c10_2(x0,x3),ndr1_1(x0) -> c2_2(x1,x2),c5_2(x0,x3),c8_2(x0,x3),c8_2(x0,a636),c3_0
% 61.72/12.86 743:13:4:[533.1,521.6]:TopTopTopTop: ssSkP0(x0),c9_2(x1,x2),c8_2(x1,x2),ndr1_1(x1),c4_1(x1),c3_1(x1),c10_2(x0,x3),ndr1_1(x0) -> c2_2(x1,x2),c5_2(x0,x3),c8_2(x0,x3),c10_2(x0,a636),c3_0
% 61.72/12.86 742:12:4:[538.1,520.7]:TopTopTopTop: c7_2(x0,x1),c2_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c5_2(x0,x2),c2_2(x0,x2),c7_1(x3),c5_0 -> c8_1(x0),ndr1_1(x3),c5_1(x3)
% 61.72/12.86 741:10:3:[538.1,519.4,674.7,740.7]:TopTopTop: c2_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_1(x0),c6_2(a673,x2),c3_2(a673,x2) -> c3_2(x0,x1),c6_2(x0,x1),c4_2(a673,x2),c9_0
% 61.72/12.86 739:11:3:[538.1,518.3]:TopTopTop: c10_2(x0,x1),ndr1_1(x0),c5_1(x0),c8_2(a755,x2),c7_2(a755,x2),ndr1_1(a755),c10_0 -> c1_2(x0,x1),c3_2(x0,x1),c10_1(x0),c6_2(a755,x2)
% 61.72/12.86 738:10:3:[532.1,517.7]:TopTopTop: c10_2(x0,x1),c3_2(x0,x1),c9_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c8_2(x0,x2),c1_2(a639,a640) -> c10_1(x0),c2_0
% 61.72/12.86 737:10:3:[532.1,516.7]:TopTopTop: c10_2(x0,x1),c3_2(x0,x1),c9_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c8_2(x0,x2),c3_2(a639,a640) -> c10_1(x0),c2_0
% 61.72/12.86 736:10:3:[538.1,515.6]:TopTopTop: c7_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c9_2(x0,x2),c8_1(x0),c6_2(a709,a710),c1_0 -> c4_2(x0,x1),c1_2(x0,x2)
% 61.72/12.86 541:2:0:[45.0,113.1]:: c9_0 -> c8_0
% 61.72/12.86 542:2:0:[2.0,217.0]:: -> ndr1_1(a614),c9_0
% 61.72/12.86 543:2:0:[115.0,223.2]:: c2_0,c7_0 ->
% 61.72/12.86 544:2:0:[2.0,294.0]:: -> c9_2(a614,a616),c9_0
% 61.72/12.86 545:2:0:[2.0,295.0]:: -> c10_2(a614,a616),c9_0
% 61.72/12.86 546:2:0:[2.0,296.0]:: -> c3_2(a614,a615),c9_0
% 61.72/12.86 548:2:1:[58.1,298.0,538.1,547.1]:Top: -> ndr1_1(x0),ssSkC22
% 61.72/12.86 549:2:0:[2.0,314.1]:: c1_2(a614,a616) -> c9_0
% 61.72/12.86 550:2:0:[2.0,315.1]:: c5_2(a614,a615) -> c9_0
% 61.72/12.86 551:3:1:[538.1,316.1]:Top: ssSkP6(x0) -> c9_2(x0,a713),ssSkC22
% 61.72/12.86 552:4:1:[538.1,317.0]:Top: -> ndr1_1(x0),c10_1(x0),c3_1(x0),ssSkC34
% 61.72/12.86 553:4:1:[538.1,318.0]:Top: -> ndr1_1(x0),c3_1(x0),c6_1(x0),ssSkC24
% 61.72/12.86 554:4:1:[538.1,319.0]:Top: -> ndr1_1(x0),c4_1(x0),c2_1(x0),ssSkC4
% 61.72/12.86 556:3:1:[70.1,320.0,538.1,555.3]:Top: ssSkC11,c8_1(x0) -> ndr1_1(x0)
% 61.72/12.86 557:3:1:[538.1,321.2]:Top: ssSkP6(x0),c6_2(x0,a713) -> ssSkC22
% 61.72/12.86 558:3:1:[538.1,322.2]:Top: ssSkP6(x0),c10_2(x0,a713) -> ssSkC22
% 61.72/12.86 560:3:1:[53.1,323.0,538.1,559.2]:Top: c9_1(x0) -> ndr1_1(x0),ssSkC28
% 61.72/12.86 561:4:1:[538.1,324.0]:Top: -> c3_2(x0,a720),c3_1(x0),c6_1(x0),ssSkC24
% 61.72/12.86 563:3:1:[56.1,325.0,538.1,562.2]:Top: c10_1(x0) -> ndr1_1(x0),ssSkC23
% 61.72/12.86 564:4:1:[538.1,326.0]:Top: -> c5_2(x0,a624),c4_1(x0),c2_1(x0),ssSkC4
% 61.72/12.86 565:5:1:[538.1,328.0]:Top: -> c2_1(x0),c5_1(x0),c3_1(x0),ndr1_1(a690),c4_0
% 61.72/12.86 566:5:1:[538.1,329.0]:Top: -> c2_1(x0),c5_1(x0),c3_1(x0),c2_1(a690),c4_0
% 61.72/12.86 567:5:1:[538.1,330.2]:Top: ssSkC13,c3_1(x0) -> ndr1_1(x0),c7_1(x0),c6_0
% 61.72/12.86 568:4:1:[538.1,331.3]:Top: ssSkP1(x0),ssSkC11,c8_1(x0) -> c10_2(x0,a662)
% 61.72/12.86 569:5:1:[538.1,332.1]:Top: ssSkC1,c5_0 -> ndr1_1(x0),c2_1(x0),c10_1(x0)
% 61.72/12.86 570:4:1:[538.1,335.1]:Top: c2_1(x0),c10_0,c1_0 -> c9_1(x0)
% 61.72/12.86 571:4:1:[538.1,336.1]:Top: c4_2(x0,a752) -> c10_1(x0),c3_1(x0),ssSkC34
% 61.72/12.86 572:4:1:[538.1,337.1]:Top: c7_2(x0,a752) -> c10_1(x0),c3_1(x0),ssSkC34
% 61.72/12.86 573:4:1:[538.1,338.2]:Top: ssSkP9(x0),c9_1(x0) -> c4_2(x0,a732),ssSkC28
% 61.72/12.86 574:4:1:[538.1,339.1]:Top: c10_2(x0,a720) -> c3_1(x0),c6_1(x0),ssSkC24
% 61.72/12.86 575:4:1:[538.1,340.2]:Top: ssSkP8(x0),c10_1(x0) -> c2_2(x0,a719),ssSkC23
% 61.72/12.86 576:4:1:[538.1,341.2]:Top: c8_1(x0),c7_1(x0) -> ndr1_1(x0),ssSkC5
% 61.72/12.86 577:4:1:[538.1,342.1]:Top: c9_2(x0,a624) -> c4_1(x0),c2_1(x0),ssSkC4
% 61.72/12.86 578:5:1:[538.1,343.3]:Top: ssSkC20,c9_1(x0),c1_1(x0) -> ndr1_1(x0),c6_0
% 61.72/12.86 580:4:1:[62.1,344.0,1.0,579.2]:Top: c8_1(x0),c6_0 -> ndr1_1(x0),c7_0
% 61.72/12.86 583:3:1:[65.1,345.0,64.1,581.1,538.1,582.2]:Top: c9_0,c7_0 -> ndr1_1(x0)
% 61.72/12.86 584:5:1:[538.1,346.2]:Top: ssSkC13,c3_1(x0) -> c8_2(x0,a666),c7_1(x0),c6_0
% 61.72/12.86 585:5:1:[538.1,347.2]:Top: ssSkC13,c3_1(x0) -> c3_2(x0,a666),c7_1(x0),c6_0
% 61.72/12.86 586:4:1:[538.1,348.4]:Top: ssSkP1(x0),ssSkC11,c6_2(x0,a662),c8_1(x0) ->
% 61.72/12.86 587:4:1:[538.1,349.4]:Top: ssSkP1(x0),ssSkC11,c2_2(x0,a662),c8_1(x0) ->
% 61.72/12.86 588:5:1:[538.1,350.2]:Top: ssSkC8,c1_1(x0),c5_0 -> ndr1_1(x0),c7_1(x0)
% 61.72/12.86 589:5:1:[538.1,351.1]:Top: ssSkC1,c5_0 -> c9_2(x0,a613),c2_1(x0),c10_1(x0)
% 61.72/12.86 735:10:3:[538.1,514.6]:TopTopTop: c7_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c9_2(x0,x2),c8_1(x0),c8_2(a709,a710),c1_0 -> c4_2(x0,x1),c1_2(x0,x2)
% 61.72/12.86 590:3:1:[81.0,354.1]:Top: c8_2(a611,x0) -> c3_2(a611,x0),ssSkC1
% 61.72/12.86 591:4:1:[185.1,356.0]:Top: c7_0 -> c4_2(a724,x0),c2_2(a724,x0),c9_0
% 61.72/12.86 593:3:1:[542.1,357.0,2.0,592.1]:Top: -> c9_2(a614,x0),c7_2(a614,x0),c9_0
% 61.72/12.86 594:4:1:[538.1,358.3]:Top: ssSkP9(x0),c3_2(x0,a732),c9_1(x0) -> ssSkC28
% 61.72/12.86 595:4:1:[538.1,359.3]:Top: ssSkP8(x0),c7_2(x0,a719),c10_1(x0) -> ssSkC23
% 61.72/12.86 596:4:1:[538.1,360.3]:Top: ssSkP8(x0),c4_2(x0,a719),c10_1(x0) -> ssSkC23
% 61.72/12.86 597:5:1:[538.1,361.3]:Top: ssSkC20,c9_1(x0),c1_1(x0) -> c6_2(x0,a706),c6_0
% 61.72/12.86 598:5:1:[538.1,362.3]:Top: ssSkC20,c9_1(x0),c1_1(x0) -> c5_2(x0,a706),c6_0
% 61.72/12.86 599:5:1:[538.1,363.0]:Top: c5_2(a690,a691) -> c2_1(x0),c5_1(x0),c3_1(x0),c4_0
% 61.72/12.86 600:5:1:[538.1,364.0]:Top: c9_2(a690,a691) -> c2_1(x0),c5_1(x0),c3_1(x0),c4_0
% 61.72/12.86 601:5:1:[538.1,365.0]:Top: c10_2(a690,a691) -> c2_1(x0),c5_1(x0),c3_1(x0),c4_0
% 61.72/12.86 602:5:1:[1.0,366.2]:Top: ssSkP5(x0),c8_1(x0),c6_0 -> c10_2(x0,a685),c7_0
% 61.72/12.86 603:5:1:[1.0,367.2]:Top: ssSkP5(x0),c8_1(x0),c6_0 -> c3_2(x0,a685),c7_0
% 61.72/12.86 604:5:1:[538.1,368.2]:Top: ssSkP2(x0),ssSkP3(x0),c9_0,c7_0 -> c5_2(x0,a677)
% 61.72/12.86 605:5:1:[538.1,369.2]:Top: ssSkP2(x0),ssSkP3(x0),c9_0,c7_0 -> c2_2(x0,a677)
% 61.72/12.86 606:5:1:[538.1,370.3]:Top: ssSkC13,c7_2(x0,a666),c3_1(x0) -> c7_1(x0),c6_0
% 61.72/12.86 607:5:1:[538.1,371.2]:Top: ssSkC8,c1_1(x0),c5_0 -> c7_2(x0,a650),c7_1(x0)
% 61.72/12.86 608:5:1:[538.1,372.2]:Top: ssSkC8,c1_1(x0),c5_0 -> c1_2(x0,a650),c7_1(x0)
% 61.72/12.86 609:5:1:[538.1,373.2]:Top: ssSkC8,c1_1(x0),c5_0 -> c5_2(x0,a650),c7_1(x0)
% 61.72/12.86 610:5:1:[538.1,374.2]:Top: ssSkC1,c2_2(x0,a613),c5_0 -> c2_1(x0),c10_1(x0)
% 61.72/12.86 611:4:1:[86.2,375.4]:Top: ssSkC33,ssSkC34,c4_2(a753,x0),c3_2(a753,x0) ->
% 61.72/12.86 612:4:1:[538.1,377.3]:Top: c10_2(x0,a627),c8_1(x0),c7_1(x0) -> ssSkC5
% 61.72/12.86 613:4:1:[538.1,378.3]:Top: c5_2(x0,a627),c8_1(x0),c7_1(x0) -> ssSkC5
% 61.72/12.86 614:4:1:[538.1,379.3]:Top: c2_2(x0,a627),c8_1(x0),c7_1(x0) -> ssSkC5
% 61.72/12.86 615:5:1:[538.1,381.4]:Top: ssSkC20,c9_2(x0,a706),c9_1(x0),c1_1(x0) -> c6_0
% 61.72/12.86 616:5:1:[1.0,382.3]:Top: ssSkP5(x0),c6_2(x0,a685),c8_1(x0),c6_0 -> c7_0
% 61.72/12.86 618:5:2:[63.1,383.0,533.1,617.2]:TopTop: c4_1(x0),c9_1(x1) -> c7_1(x0),ndr1_1(x1),c3_0
% 61.72/12.86 619:5:1:[538.1,384.3]:Top: ssSkP2(x0),ssSkP3(x0),c9_2(x0,a677),c9_0,c7_0 ->
% 61.72/12.86 620:5:1:[538.1,386.2]:Top: c8_1(x0),c3_1(x0),c9_0,c5_0 -> c1_1(x0)
% 61.72/12.86 622:4:1:[538.1,387.2,44.1,621.3]:Top: c6_1(x0),c2_1(x0),c10_0 -> c3_1(x0)
% 61.72/12.86 623:6:2:[533.1,392.2]:TopTop: ssSkP4(x0),c4_1(x1),c9_1(x0) -> c7_1(x1),c6_2(x0,a683),c3_0
% 61.72/12.86 624:6:2:[533.1,393.2]:TopTop: ssSkP4(x0),c4_1(x1),c9_1(x0) -> c7_1(x1),c5_2(x0,a683),c3_0
% 61.72/12.86 625:5:1:[538.1,394.3]:Top: c4_1(x0),c5_1(x0),c6_1(x0),c2_0 -> c8_1(a637)
% 61.72/12.86 626:5:1:[538.1,395.3]:Top: c4_1(x0),c5_1(x0),c6_1(x0),c2_0 -> c5_1(a637)
% 61.72/12.86 627:5:1:[538.1,396.3]:Top: c4_1(x0),c5_1(x0),c6_1(x0),c2_0 -> c3_1(a637)
% 61.72/12.86 628:4:1:[76.0,401.2]:Top: c1_2(a631,x0),c6_2(a631,x0) -> c7_2(a631,x0),ssSkC6
% 61.72/12.86 629:5:1:[175.1,402.1]:Top: c6_2(a759,x0),c1_0 -> c7_2(a759,x0),c8_2(a759,x0),c7_0
% 61.72/12.86 630:6:2:[533.1,404.2]:TopTop: ssSkP4(x0),c4_1(x1),c4_2(x0,a683),c9_1(x0) -> c7_1(x1),c3_0
% 61.72/12.86 631:5:1:[201.1,405.1]:Top: c9_2(a679,x0),c4_0 -> c10_2(a679,x0),c4_2(a679,x0),c8_0
% 61.72/12.86 632:5:1:[178.1,408.2]:Top: c3_2(a745,x0),c1_2(a745,x0),c7_0 -> c9_2(a745,x0),c8_0
% 61.72/12.86 633:5:1:[185.1,410.2]:Top: c8_2(a724,x0),c9_2(a724,x0),c7_0 -> c6_2(a724,x0),c9_0
% 61.72/12.86 634:5:1:[192.2,411.3]:Top: ssSkC18,c1_2(a701,x0),c6_2(a701,x0),c1_0 -> c5_2(a701,x0)
% 61.72/12.86 635:5:1:[103.1,413.4]:Top: ssSkC7,c2_2(a645,x0),c5_2(a645,x0),c9_2(a645,x0) -> c10_0
% 61.72/12.86 636:7:2:[538.1,415.2]:TopTop: c10_2(x0,x1),ndr1_1(x0),c3_0 -> c1_2(x0,x1),c5_2(x0,x1),c8_1(x0),c9_0
% 61.72/12.86 637:7:2:[538.1,416.1]:TopTop: ndr1_1(x0) -> c3_2(x0,x1),c5_2(x0,x1),c10_2(x0,x1),c1_2(x0,a748),c8_1(x0),ssSkC32
% 61.72/12.86 638:7:2:[538.1,417.1]:TopTop: ndr1_1(x0) -> c3_2(x0,x1),c5_2(x0,x1),c10_2(x0,x1),c10_2(x0,a748),c8_1(x0),ssSkC32
% 61.72/12.86 639:7:2:[538.1,418.2]:TopTop: ndr1_1(x0),c4_2(x0,a748) -> c3_2(x0,x1),c5_2(x0,x1),c10_2(x0,x1),c8_1(x0),ssSkC32
% 61.72/12.86 640:7:2:[538.1,419.2]:TopTop: c2_2(x0,x1),ndr1_1(x0) -> c5_2(x0,x1),c4_2(x0,x1),c8_2(x0,a722),c6_1(x0),ssSkC25
% 61.72/12.86 641:7:2:[538.1,420.3]:TopTop: c1_2(x0,x1),ndr1_1(x0),c2_1(x0) -> c3_2(x0,x1),c5_2(x0,x1),c5_2(x0,a747),c6_0
% 61.72/12.86 642:7:2:[538.1,421.3]:TopTop: c1_2(x0,x1),ndr1_1(x0),c2_1(x0) -> c3_2(x0,x1),c5_2(x0,x1),c9_2(x0,a747),c6_0
% 61.72/12.86 643:7:2:[538.1,422.5]:TopTop: ssSkP10(x0),ssSkC31,c1_2(x0,x1),c3_2(x0,x1),ndr1_1(x0) -> c6_2(x0,x1),c9_2(x0,a744)
% 61.72/12.86 644:7:2:[538.1,423.5]:TopTop: ssSkP10(x0),ssSkC31,c1_2(x0,x1),c3_2(x0,x1),ndr1_1(x0) -> c6_2(x0,x1),c6_2(x0,a744)
% 61.72/12.86 645:7:2:[538.1,424.5]:TopTop: ssSkP10(x0),ssSkC31,c1_2(x0,x1),c3_2(x0,x1),ndr1_1(x0) -> c6_2(x0,x1),c8_2(x0,a744)
% 61.72/12.86 646:7:2:[533.1,425.3]:TopTop: c8_2(x0,x1),c2_2(x0,x1),ndr1_1(x0) -> c1_2(x0,x1),c1_2(x0,a678),c7_1(x0),c3_0
% 61.72/12.86 647:7:2:[538.1,426.3]:TopTop: c2_2(x0,x1),ndr1_1(x0),c4_1(x0) -> c10_2(x0,x1),c6_2(x0,x1),c1_2(x0,a654),c9_0
% 61.72/12.86 649:6:2:[538.1,427.3,115.0,648.7]:TopTop: c3_2(x0,x1),ndr1_1(x0),c1_1(x0),c2_0 -> c6_2(x0,x1),c1_2(x0,a638)
% 61.72/12.86 650:8:2:[1.0,428.3]:TopTop: c3_2(x0,x1),c6_2(x0,x1),ndr1_1(x0) -> c5_2(x0,x1),c10_1(x0),c3_1(x0),c7_0,c2_0
% 61.72/12.86 651:8:2:[538.1,429.2]:TopTop: c5_2(x0,x1),ndr1_1(x0),c2_0 -> c3_2(x0,x1),c10_2(x0,x1),c1_1(x0),c5_1(x0),c6_0
% 61.72/12.86 653:7:2:[538.1,430.0,565.4,652.1]:TopTop: -> c2_1(x0),c5_1(x0),c3_1(x0),c7_2(a690,x1),c2_2(a690,x1),c4_2(a690,x1),c4_0
% 61.72/12.86 654:7:2:[538.1,431.3]:TopTop: c6_2(x0,x1),c8_2(x0,x1),ndr1_1(x0) -> c9_2(x0,x1),c3_2(x0,a751),c7_1(x0),ssSkC33
% 61.72/12.86 655:7:2:[538.1,432.3]:TopTop: c6_2(x0,x1),c8_2(x0,x1),ndr1_1(x0) -> c9_2(x0,x1),c2_2(x0,a751),c7_1(x0),ssSkC33
% 61.72/12.86 656:7:2:[538.1,433.3]:TopTop: c9_2(x0,x1),ndr1_1(x0),c4_2(x0,a726) -> c1_2(x0,x1),c10_2(x0,x1),c3_1(x0),ssSkC26
% 61.72/12.86 657:7:2:[538.1,434.3]:TopTop: c9_2(x0,x1),ndr1_1(x0),c3_2(x0,a726) -> c1_2(x0,x1),c10_2(x0,x1),c3_1(x0),ssSkC26
% 61.72/12.86 658:7:2:[538.1,435.3]:TopTop: c2_2(x0,x1),ndr1_1(x0),c5_2(x0,a722) -> c5_2(x0,x1),c4_2(x0,x1),c6_1(x0),ssSkC25
% 61.72/12.86 659:7:2:[538.1,436.3]:TopTop: c2_2(x0,x1),ndr1_1(x0),c9_2(x0,a722) -> c5_2(x0,x1),c4_2(x0,x1),c6_1(x0),ssSkC25
% 61.72/12.86 660:7:2:[538.1,437.4]:TopTop: c1_2(x0,x1),ndr1_1(x0),c1_2(x0,a747),c2_1(x0) -> c3_2(x0,x1),c5_2(x0,x1),c6_0
% 61.72/12.86 661:7:2:[533.1,438.4]:TopTop: c8_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c8_2(x0,a678) -> c1_2(x0,x1),c7_1(x0),c3_0
% 61.72/12.86 662:7:2:[533.1,439.4]:TopTop: c8_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c6_2(x0,a678) -> c1_2(x0,x1),c7_1(x0),c3_0
% 61.72/12.86 663:8:2:[538.1,440.3]:TopTop: ssSkC15,ndr1_1(x0),c3_1(x0),c9_0 -> c10_2(x0,x1),c7_2(x0,x1),c3_2(x0,x1),c8_2(x0,a671)
% 61.72/12.86 664:8:2:[538.1,441.3]:TopTop: ssSkC15,ndr1_1(x0),c3_1(x0),c9_0 -> c10_2(x0,x1),c7_2(x0,x1),c3_2(x0,x1),c2_2(x0,a671)
% 61.72/12.86 665:7:2:[538.1,442.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c9_2(x0,a654),c4_1(x0) -> c10_2(x0,x1),c6_2(x0,x1),c9_0
% 61.72/12.86 666:7:2:[538.1,443.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c4_2(x0,a654),c4_1(x0) -> c10_2(x0,x1),c6_2(x0,x1),c9_0
% 61.72/12.86 667:8:2:[538.1,444.3]:TopTop: c10_2(x0,x1),ndr1_1(x0),c9_1(x0) -> c5_2(x0,x1),c2_2(x0,x1),c2_1(x0),c3_1(a648),c6_0
% 61.72/12.86 669:6:2:[538.1,445.4,115.0,668.7]:TopTop: c3_2(x0,x1),ndr1_1(x0),c2_2(x0,a638),c1_1(x0),c2_0 -> c6_2(x0,x1)
% 61.72/12.86 670:7:2:[538.1,446.5]:TopTop: c9_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c8_1(x0),c3_1(x0) -> c6_2(x0,x1),c6_0
% 61.72/12.86 671:8:2:[538.1,447.5]:TopTop: ssSkP11(x0),ssSkC32,c2_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_0 -> c9_2(x0,x1),c2_2(x0,a750)
% 61.72/12.86 734:11:4:[538.1,513.5]:TopTopTopTop: ssSkP7(x0),c5_2(x1,x2),ndr1_1(x1),c1_1(x1),c6_1(x1),c7_2(x0,x3),c3_2(x0,x3),ndr1_1(x0),c7_0 -> c7_2(x1,x2),c1_2(x0,a716)
% 61.72/12.86 733:11:4:[538.1,512.5]:TopTopTopTop: ssSkP7(x0),c5_2(x1,x2),ndr1_1(x1),c1_1(x1),c6_1(x1),c7_2(x0,x3),c3_2(x0,x3),ndr1_1(x0),c7_0 -> c7_2(x1,x2),c3_2(x0,a716)
% 61.72/12.86 732:11:4:[538.1,511.5]:TopTopTopTop: ssSkP7(x0),c5_2(x1,x2),ndr1_1(x1),c1_1(x1),c6_1(x1),c7_2(x0,x3),c3_2(x0,x3),ndr1_1(x0),c7_0 -> c7_2(x1,x2),c2_2(x0,a716)
% 61.72/12.86 672:8:2:[538.1,451.4]:TopTop: ssSkC22,c7_2(x0,x1),ndr1_1(x0),c8_1(x0),c6_0 -> c6_2(x0,x1),c8_2(x0,x1),c3_2(x0,a714)
% 61.72/12.86 673:8:2:[538.1,452.4]:TopTop: ssSkC22,c7_2(x0,x1),ndr1_1(x0),c8_1(x0),c6_0 -> c6_2(x0,x1),c8_2(x0,x1),c7_2(x0,a714)
% 61.72/12.86 674:8:2:[538.1,453.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_1(x0) -> c3_2(x0,x1),c6_2(x0,x1),ndr1_1(a673),c9_0
% 61.72/12.86 675:8:2:[538.1,454.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_1(x0) -> c3_2(x0,x1),c6_2(x0,x1),c9_1(a673),c9_0
% 61.72/12.86 676:8:2:[538.1,455.4]:TopTop: ssSkC15,ndr1_1(x0),c1_2(x0,a671),c3_1(x0),c9_0 -> c10_2(x0,x1),c7_2(x0,x1),c3_2(x0,x1)
% 61.72/12.86 677:8:2:[538.1,456.3]:TopTop: c10_2(x0,x1),ndr1_1(x0),c9_1(x0),c7_1(a648) -> c5_2(x0,x1),c2_2(x0,x1),c2_1(x0),c6_0
% 61.72/12.86 678:8:2:[538.1,457.5]:TopTop: ssSkC6,c8_2(x0,x1),ndr1_1(x0),c6_1(x0),c8_1(x0) -> c4_2(x0,x1),c1_2(x0,x1),ndr1_1(a633)
% 61.72/12.86 679:8:2:[538.1,458.5]:TopTop: ssSkC6,c8_2(x0,x1),ndr1_1(x0),c6_1(x0),c8_1(x0) -> c4_2(x0,x1),c1_2(x0,x1),c10_1(a633)
% 61.72/12.86 680:8:2:[530.1,459.5]:TopTop: c8_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c10_1(x0),c8_1(x0) -> c5_2(x0,x1),c2_0,c1_0
% 61.72/12.86 681:8:2:[538.1,460.3]:TopTop: c10_2(x0,x1),ndr1_1(x0),c5_1(x0),c7_1(a755),c10_0 -> c1_2(x0,x1),c3_2(x0,x1),c10_1(x0)
% 61.72/12.86 682:8:2:[538.1,461.3]:TopTop: c10_2(x0,x1),ndr1_1(x0),c5_1(x0),c6_1(a755),c10_0 -> c1_2(x0,x1),c3_2(x0,x1),c10_1(x0)
% 61.72/12.86 683:8:2:[538.1,462.6]:TopTop: ssSkP11(x0),ssSkC32,c2_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c8_2(x0,a750),c4_0 -> c9_2(x0,x1)
% 61.72/12.86 684:8:2:[538.1,463.6]:TopTop: ssSkP11(x0),ssSkC32,c2_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c10_2(x0,a750),c4_0 -> c9_2(x0,x1)
% 61.72/12.86 685:8:2:[538.1,464.5]:TopTop: ssSkC22,c7_2(x0,x1),ndr1_1(x0),c5_2(x0,a714),c8_1(x0),c6_0 -> c6_2(x0,x1),c8_2(x0,x1)
% 61.72/12.86 686:8:2:[538.1,465.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_1(x0) -> c3_2(x0,x1),c6_2(x0,x1),c3_2(a673,a674),c9_0
% 61.72/12.86 687:8:2:[538.1,466.5]:TopTop: ssSkC6,c8_2(x0,x1),ndr1_1(x0),c6_1(x0),c8_1(x0) -> c4_2(x0,x1),c1_2(x0,x1),c9_2(a633,a634)
% 61.72/12.86 688:8:2:[538.1,467.5]:TopTop: ssSkC6,c8_2(x0,x1),ndr1_1(x0),c6_1(x0),c8_1(x0),c2_1(a633) -> c4_2(x0,x1),c1_2(x0,x1)
% 61.72/12.86 689:10:3:[538.1,468.2]:TopTopTop: ndr1_1(x0),c1_1(x0),c4_1(x1) -> c8_2(x0,x2),c6_2(x0,x2),c4_2(x0,x2),c5_1(x0),ndr1_1(x1),c7_1(x1),c6_0
% 61.72/12.86 690:9:3:[533.1,469.2]:TopTopTop: c9_1(x0),c5_1(x0),c9_2(x1,x2),ndr1_1(x1) -> c2_1(x0),c4_2(x1,x2),c7_2(x1,a619),c7_1(x1),c3_0
% 61.72/12.86 691:8:2:[538.1,470.4]:TopTop: c2_2(x0,x1),ndr1_1(x0),c3_1(x0),c6_1(x0),c4_2(a673,a674) -> c3_2(x0,x1),c6_2(x0,x1),c9_0
% 61.72/12.86 692:8:2:[538.1,471.5]:TopTop: ssSkC6,c8_2(x0,x1),ndr1_1(x0),c6_1(x0),c8_1(x0),c10_2(a633,a634) -> c4_2(x0,x1),c1_2(x0,x1)
% 61.72/12.86 693:8:2:[538.1,472.5]:TopTop: c9_2(x0,x1),c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c6_1(x0),c4_0,c3_0 -> c2_1(x0)
% 61.72/12.86 694:9:3:[533.1,473.2]:TopTopTop: c9_1(x0),c5_1(x0),c9_2(x1,x2),ndr1_1(x1),c3_2(x1,a619) -> c2_1(x0),c4_2(x1,x2),c7_1(x1),c3_0
% 61.72/12.86 695:9:3:[538.1,474.6]:TopTopTop: ssSkC12,c7_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c10_1(x0),c9_1(x0),c9_1(x2) -> c1_2(x0,x1),ndr1_1(x2)
% 61.72/12.86 696:10:3:[538.1,475.2]:TopTopTop: ndr1_1(x0),c1_1(x0),c8_2(x1,a659),c4_1(x1) -> c8_2(x0,x2),c6_2(x0,x2),c4_2(x0,x2),c5_1(x0),c7_1(x1),c6_0
% 61.72/12.86 697:10:3:[538.1,476.2]:TopTopTop: ndr1_1(x0),c1_1(x0),c5_2(x1,a659),c4_1(x1) -> c8_2(x0,x2),c6_2(x0,x2),c4_2(x0,x2),c5_1(x0),c7_1(x1),c6_0
% 61.72/12.86 698:10:3:[538.1,477.2]:TopTopTop: ndr1_1(x0),c1_1(x0),c7_2(x1,a659),c4_1(x1) -> c8_2(x0,x2),c6_2(x0,x2),c4_2(x0,x2),c5_1(x0),c7_1(x1),c6_0
% 61.72/12.86 699:9:3:[538.1,478.6]:TopTopTop: ssSkC12,c7_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c10_1(x0),c9_1(x0),c9_1(x2) -> c1_2(x0,x1),c5_2(x2,a664)
% 61.72/12.86 700:9:3:[538.1,479.6]:TopTopTop: ssSkC12,c7_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c10_1(x0),c9_1(x0),c9_1(x2) -> c1_2(x0,x1),c2_2(x2,a664)
% 61.72/12.86 701:9:3:[538.1,480.6]:TopTopTop: ssSkC12,c7_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c10_1(x0),c9_1(x0),c9_1(x2) -> c1_2(x0,x1),c7_2(x2,a664)
% 61.72/12.86 702:10:3:[538.1,481.5]:TopTopTop: ssSkC9,c3_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c3_2(x0,x2) -> c6_2(x0,x1),c4_2(x0,x1),c8_2(x0,x2),c8_1(x0),ndr1_1(a652)
% 61.72/12.86 703:10:3:[538.1,482.6]:TopTopTop: ssSkC26,c8_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x0),c10_1(x0),c7_1(x2),c4_1(x2) -> c3_2(x0,x1),ndr1_1(x2)
% 61.72/12.86 704:10:3:[538.1,483.3]:TopTopTop: c8_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c4_0,c5_0 -> c1_2(x0,x1),c5_2(x0,x1),c8_2(x0,x2),c3_2(x0,x2),c1_2(x0,a667)
% 61.72/12.86 705:10:3:[538.1,484.3]:TopTopTop: c8_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c4_0,c5_0 -> c1_2(x0,x1),c5_2(x0,x1),c8_2(x0,x2),c3_2(x0,x2),c6_2(x0,a667)
% 61.72/12.86 706:10:3:[538.1,485.5]:TopTopTop: ssSkC9,c3_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c3_2(x0,x2) -> c6_2(x0,x1),c4_2(x0,x1),c8_2(x0,x2),c8_1(x0),c1_2(a652,a653)
% 61.72/12.86 707:10:3:[538.1,486.5]:TopTopTop: ssSkC9,c3_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c3_2(x0,x2),c2_1(a652) -> c6_2(x0,x1),c4_2(x0,x1),c8_2(x0,x2),c8_1(x0)
% 61.72/12.86 708:10:3:[538.1,487.5]:TopTopTop: ssSkC9,c3_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c3_2(x0,x2),c8_1(a652) -> c6_2(x0,x1),c4_2(x0,x1),c8_2(x0,x2),c8_1(x0)
% 61.72/12.86 709:10:3:[538.1,488.5]:TopTopTop: c4_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c9_2(x0,x2),c4_1(x0),c10_0 -> c5_2(x0,x1),c6_2(x0,x2),c8_2(x0,x2),c9_0
% 61.72/12.86 710:10:3:[538.1,489.6]:TopTopTop: ssSkC26,c8_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x0),c10_1(x0),c7_1(x2),c4_1(x2) -> c3_2(x0,x1),c9_2(x2,a727)
% 61.72/12.86 711:10:3:[538.1,490.4]:TopTopTop: c8_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c10_2(x0,a667),c4_0,c5_0 -> c1_2(x0,x1),c5_2(x0,x1),c8_2(x0,x2),c3_2(x0,x2)
% 61.72/12.86 712:10:3:[538.1,491.5]:TopTopTop: ssSkC9,c3_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c3_2(x0,x2),c5_2(a652,a653) -> c6_2(x0,x1),c4_2(x0,x1),c8_2(x0,x2),c8_1(x0)
% 61.72/12.86 713:10:3:[538.1,492.5]:TopTopTop: ssSkC9,c3_2(x0,x1),ndr1_1(x0),c10_2(x0,x2),c3_2(x0,x2),c10_2(a652,a653) -> c6_2(x0,x1),c4_2(x0,x1),c8_2(x0,x2),c8_1(x0)
% 61.72/12.86 714:10:3:[39.1,493.6]:TopTopTop: ssSkC0,c1_2(x0,x1),ndr1_1(x0),c5_2(x0,x2),c2_2(x0,x2),c4_2(x0,x2),c8_0 -> c9_2(x0,x1),c6_2(x0,x1),c3_2(x0,a610)
% 61.72/12.86 715:10:3:[39.1,494.6]:TopTopTop: ssSkC0,c1_2(x0,x1),ndr1_1(x0),c5_2(x0,x2),c2_2(x0,x2),c4_2(x0,x2),c8_0 -> c9_2(x0,x1),c6_2(x0,x1),c4_2(x0,a610)
% 61.72/12.86 716:10:3:[39.1,495.6]:TopTopTop: ssSkC0,c1_2(x0,x1),ndr1_1(x0),c5_2(x0,x2),c2_2(x0,x2),c4_2(x0,x2),c8_0 -> c9_2(x0,x1),c6_2(x0,x1),c9_2(x0,a610)
% 61.72/12.86 717:12:4:[538.1,496.4]:TopTopTopTop: ssSkC19,c1_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c7_1(x3) -> c4_2(x0,x1),c10_2(x0,x1),c6_2(x0,x2),c4_2(x0,x2),c1_1(x0),ndr1_1(x3),c4_1(x3)
% 61.72/12.86 718:10:3:[538.1,497.3]:TopTopTop: c10_2(x0,x1),ndr1_1(x0),c9_1(x0),c7_2(a648,x2),c3_2(a648,x2),ndr1_1(a648) -> c5_2(x0,x1),c2_2(x0,x1),c2_1(x0),c6_0
% 61.72/12.86 719:10:3:[538.1,498.6]:TopTopTop: ssSkC26,c8_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x0),c10_1(x0),c7_2(x2,a727),c7_1(x2),c4_1(x2) -> c3_2(x0,x1)
% 61.72/12.86 720:10:3:[538.1,499.6]:TopTopTop: ssSkC26,c8_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c4_1(x0),c10_1(x0),c6_2(x2,a727),c7_1(x2),c4_1(x2) -> c3_2(x0,x1)
% 61.72/12.86 721:10:3:[538.1,500.6]:TopTopTop: c7_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c9_2(x0,x2),c8_1(x0),c1_0 -> c4_2(x0,x1),c1_2(x0,x2),ndr1_1(a709)
% 61.72/12.86 722:10:3:[538.1,501.6]:TopTopTop: c7_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c9_2(x0,x2),c8_1(x0),c1_0 -> c4_2(x0,x1),c1_2(x0,x2),c8_1(a709)
% 61.72/12.86 723:10:3:[532.1,502.7]:TopTopTop: c10_2(x0,x1),c3_2(x0,x1),c9_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c8_2(x0,x2) -> c10_1(x0),ndr1_1(a639),c2_0
% 61.72/12.86 724:12:4:[538.1,503.4]:TopTopTopTop: ssSkC19,c1_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c7_1(x3) -> c4_2(x0,x1),c10_2(x0,x1),c6_2(x0,x2),c4_2(x0,x2),c1_1(x0),c9_2(x3,a704),c4_1(x3)
% 61.72/12.86 725:10:3:[538.1,504.6]:TopTopTop: c7_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c9_2(x0,x2),c8_1(x0),c1_0 -> c4_2(x0,x1),c1_2(x0,x2),c9_2(a709,a710)
% 61.72/12.86 726:10:3:[538.1,505.6]:TopTopTop: c7_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c9_2(x0,x2),c8_1(x0),c9_1(a709),c1_0 -> c4_2(x0,x1),c1_2(x0,x2)
% 61.72/12.86 727:10:3:[532.1,506.7]:TopTopTop: c10_2(x0,x1),c3_2(x0,x1),c9_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c8_2(x0,x2) -> c10_1(x0),c8_2(a639,a640),c2_0
% 61.72/12.86 728:10:3:[532.1,507.7]:TopTopTop: c10_2(x0,x1),c3_2(x0,x1),c9_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c8_2(x0,x2),c2_1(a639) -> c10_1(x0),c2_0
% 61.72/12.86 729:10:3:[532.1,508.7]:TopTopTop: c10_2(x0,x1),c3_2(x0,x1),c9_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c6_2(x0,x2),c8_2(x0,x2),c8_1(a639) -> c10_1(x0),c2_0
% 61.72/12.86 730:12:4:[538.1,509.4]:TopTopTopTop: ssSkC19,c1_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c5_2(x3,a704),c7_1(x3) -> c4_2(x0,x1),c10_2(x0,x1),c6_2(x0,x2),c4_2(x0,x2),c1_1(x0),c4_1(x3)
% 61.72/12.86 731:12:4:[538.1,510.4]:TopTopTopTop: ssSkC19,c1_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c3_2(x3,a704),c7_1(x3) -> c4_2(x0,x1),c10_2(x0,x1),c6_2(x0,x2),c4_2(x0,x2),c1_1(x0),c4_1(x3)
% 61.72/12.86
% 61.72/12.86 Most General Atoms: ndr1_0 c7_0 c2_0 c9_0 c3_0 c5_0 c8_0 ssSkC35 ssSkC31 ssSkC30 ssSkC29 ssSkC27 ssSkC21 ssSkC20 ssSkC19 ssSkC18 ssSkC17 ssSkC16 ssSkC15 ssSkC14 ssSkC13 ssSkC12 ssSkC11 ssSkC10 ssSkC9 ssSkC8 ssSkC7 ssSkC6 ssSkC3 ssSkC2 ssSkC1 ssSkC0 c1_0 ssSkC33 ssSkC34 c10_0 ssSkC23 ssSkC24 ssSkC4 c4_0 c6_0 ssSkP11(x0) ssSkP10(x0) ssSkP9(x0) ssSkP8(x0) ssSkP7(x0) ssSkP6(x0) ssSkP5(x0) ssSkP4(x0) ssSkP3(x0) ssSkP2(x0) ssSkP1(x0) ssSkP0(x0) c8_1(x0) c5_1(x3) c10_2(x0,x3) c2_2(x1,x2) c3_1(x0) c10_1(x0) c9_2(x0,x1) c6_2(x0,x2) c1_2(x0,x2) ssSkC25 ssSkC5 ssSkC28 ssSkC22 c2_1(x0) ssSkC32 c8_2(x0,x1) ssSkC26 c5_2(x1,x2) c1_1(x1) c6_1(x1) c3_2(x0,x3) c7_2(x1,x2) c4_2(x1,x2) c9_1(x2) ndr1_1(x2) c7_1(x2) c4_1(x3)
% 61.72/12.86
% 61.72/12.86 === Starting SPASS-SCL-FOL A Little Less Naive, considering 574 atoms initially, heuristics mode: lmodel_grow ===
% 61.72/12.86
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 623
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 660
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 680
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 713
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 746
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 776
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 806
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 834
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 862
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 880
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 898
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 914
% 61.72/12.86 === Conflict found: 622:4:1:[538.1,387.2,44.1,621.3]:Top: c6_1(x0),c2_1(x0),c10_0 -> c3_1(x0) {x0 -> a610}
% 61.72/12.86 === Backtracking. Learning clause 752:5:1:[622.1,553.3]:Top: c2_1(x0),c10_0 -> ndr1_1(x0),c3_1(x0),ssSkC24
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 952
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 993
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1017
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1046
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1070
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1091
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1106
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1118
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1130
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1148
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1166
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1178
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1193
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1206
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1220
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1232
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1244
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1256
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1268
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1280
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1292
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1307
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1314
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1326
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1340
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1352
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1364
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1376
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1394
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1415
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1437
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1449
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1461
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1474
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1488
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1500
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1515
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1528
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1542
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1554
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1569
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1575
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1587
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1600
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1612
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1624
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1636
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1647
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1658
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1670
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1682
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1693
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1705
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1717
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1729
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1743
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1755
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1767
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1779
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1794
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1806
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1818
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1830
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1846
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1865
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1888
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1893
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1902
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1910
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1918
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1930
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1940
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1951
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1959
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1967
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 1977
% 61.72/12.86 === Conflict found: 570:4:1:[538.1,335.1]:Top: c2_1(x0),c10_0,c1_0 -> c9_1(x0) {x0 -> a737}
% 61.72/12.86 === Backtracking. Learning clause 753:6:1:[570.1,554.3]:Top: c10_0,c1_0 -> c9_1(x0),ndr1_1(x0),c4_1(x0),ssSkC4
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2001
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2017
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2031
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2042
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2058
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2067
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2074
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2079
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2084
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2091
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2098
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2103
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2108
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2112
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2119
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2124
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2129
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2134
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2139
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2143
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2148
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2153
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2157
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2164
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2169
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2174
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2179
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2186
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2191
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2196
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2201
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2208
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2214
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2221
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2226
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2233
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2238
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2245
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2248
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2251
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2254
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2259
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2262
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2265
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2270
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2273
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2278
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2283
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2286
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2291
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2294
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2297
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2300
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2305
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2310
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2315
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2320
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2325
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2328
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2331
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2334
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2337
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2340
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2343
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2348
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2353
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2356
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2359
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2362
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2365
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2368
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2373
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2376
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2379
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2382
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2385
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2388
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2391
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2394
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2397
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2402
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2405
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2408
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2411
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2414
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2417
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2420
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2423
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2426
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2429
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2432
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2437
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2440
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2445
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2448
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2451
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2454
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2459
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2462
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2465
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2468
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2473
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2476
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2481
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2484
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2487
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2490
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2495
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2498
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2501
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2504
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2507
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2510
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2515
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2518
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2521
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2526
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2529
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2532
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2535
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2538
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2543
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2548
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2551
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2554
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2557
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2560
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2563
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2568
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2573
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2578
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2581
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2584
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2589
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2592
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2595
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2598
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2601
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2604
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2607
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2614
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2621
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2628
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2634
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2641
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2649
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2656
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2663
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2676
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2693
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2697
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2704
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2711
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2720
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2727
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2734
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2744
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2754
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2762
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2769
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2778
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2785
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2795
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2797
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2804
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2813
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2820
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2827
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2837
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2838
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2845
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2853
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2862
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2869
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2883
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2893
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2904
% 61.72/12.86 === Clause set with instances from active satisfied. Growing active. New size: 2906
% 61.72/12.86
% 61.72/12.86 Linear Model Building succeeded.
% 61.72/12.86 SZS status Satisfiable
% 61.72/12.86
% 61.72/12.86 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/12.86
% 61.72/12.86 SPASS-SCL-FOL Statistics:
% 61.72/12.86 Number of learned clauses: 2
% 61.72/12.86 Number of propagations: 659
% 61.72/12.86 Number of decisions: 4436
% 61.72/12.86 Number of resolutions: 2
% 61.72/12.86 Number of condensations: 0
% 61.72/12.86 Number of sub resolutions: 222
% 61.72/12.86 Number of input literals (deduplicated): 574
% 61.72/12.86 Number of grows: 266
% 61.72/12.86 Number of considered ground atoms: 2906
% 61.72/12.86
% 61.72/12.86 Needed: 0:0:12.30
% 61.72/12.86
%------------------------------------------------------------------------------