%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN418-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 : n018.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:45 PM UTC 2026
% Result : Satisfiable 117.52s 24.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN418-1 : TPTP v9.2.1. Released v2.1.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n018.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:02 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 117.52/24.12 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.52/24.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.52/24.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.52/24.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.52/24.12 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.52/24.12 Execution lmodel_grow ended with status: satisfiable
% 117.52/24.12 Used heuristic: lmodel_grow
% 117.52/24.12
% 117.52/24.12 Input Clauses:
% 117.52/24.12
% 117.52/24.12 Predicates: ssSkC1 ndr1_0 c5_0 c10_0 c2_0 ssSkC26 ssSkC25 ssSkC22 ssSkC21 ssSkC20 ssSkC19 ssSkC18 ssSkC17 ssSkC16 ssSkC15 ssSkC12 ssSkC11 ssSkC10 ssSkC8 ssSkC7 ssSkC6 ssSkC5 ssSkC4 ssSkC3 ssSkC2 ssSkC0 c4_0 ssSkC29 c3_0 ssSkC24 c6_0 c8_0 c7_0 c1_0 ndr1_1 c10_1 c8_1 c7_1 c9_1 c5_1 ssSkP7 ssSkP6 ssSkP5 c2_1 c4_1 ssSkP4 ssSkP3 ssSkP2 ssSkP1 ssSkP0 c3_1 c6_1 c1_1 c9_0 ssSkC23 ssSkC13 c2_2 c3_2 c6_2 c4_2 c9_2 c7_2 c5_2 c10_2 c8_2 c1_2 ssSkC28 ssSkC30 ssSkC27 ssSkC14 ssSkC9
% 117.52/24.12 Fol Constants: a7 a123 a105 a100 a97 a90 a87 a68 a66 a45 a37 a33 a31 a19 a16 a12 a9 a6 a1 a143 a139 a126 a122 a119 a108 a102 a98 a93 a77 a35 a8 a125 a124 a121 a107 a106 a101 a91 a85 a84 a79 a75 a62 a60 a57 a55 a49 a48 a47 a41 a38 a34 a32 a21 a20 a17 a13 a10 a2 a144 a141 a140 a127 a120 a116 a114 a112 a110 a109 a99 a94 a78 a51 a36 a26 a18 a88 a69 a64 a46 a136 a134 a128 a117 a115 a103 a95 a59 a53 a44 a29 a27 a137 a135 a113 a96 a54 a30 a28 a22 a23 a132 a25 a3 a58 a80 a24 a5 a4 a145 a138 a89 a86 a118 a133 a67 a65 a50 a146 a142 a63 a111 a52 a61 a130 a56 a81 a74 a15 a82 a70 a14 a83 a76 a92 a42 a73 a131 a39 a43 a40 a104 a11 a129 a71 a72
% 117.52/24.12 Fol Functions:
% 117.52/24.12 Problem Properties:
% 117.52/24.12 This is a Bernays Schoenfinkel problem.
% 117.52/24.12
% 117.52/24.12 After reduction: Problem Properties:
% 117.52/24.12 This is a Bernays Schoenfinkel problem.
% 117.52/24.12
% 117.52/24.12
% 117.52/24.12 Reduced Input Clauses:
% 117.52/24.12 505:1:0:[24.1,1.0]:: -> ndr1_0
% 117.52/24.12 696:15:5:[505.1,504.3]:TopTopTopTopTop: c8_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c8_2(x2,x3),c5_2(x2,x3),ndr1_1(x2),c7_2(x2,x4),c3_2(x2,x4),c10_2(a71,a72) -> c10_2(x0,x1),c1_1(x0),c10_1(x0),c1_2(x2,x3),c2_2(x2,x4),c5_1(x2)
% 117.52/24.12 695:15:5:[505.1,503.3]:TopTopTopTopTop: c8_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c8_2(x2,x3),c5_2(x2,x3),ndr1_1(x2),c7_2(x2,x4),c3_2(x2,x4),c2_1(a71) -> c10_2(x0,x1),c1_1(x0),c10_1(x0),c1_2(x2,x3),c2_2(x2,x4),c5_1(x2)
% 117.52/24.12 694:15:5:[505.1,502.3]:TopTopTopTopTop: c8_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c8_2(x2,x3),c5_2(x2,x3),ndr1_1(x2),c7_2(x2,x4),c3_2(x2,x4),c8_1(a71) -> c10_2(x0,x1),c1_1(x0),c10_1(x0),c1_2(x2,x3),c2_2(x2,x4),c5_1(x2)
% 117.52/24.12 693:15:5:[505.1,501.3]:TopTopTopTopTop: c8_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c8_2(x2,x3),c5_2(x2,x3),ndr1_1(x2),c7_2(x2,x4),c3_2(x2,x4) -> c10_2(x0,x1),c1_1(x0),c10_1(x0),c1_2(x2,x3),c2_2(x2,x4),c5_1(x2),c7_2(a71,a72)
% 117.52/24.12 692:15:5:[505.1,500.3]:TopTopTopTopTop: c8_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c8_2(x2,x3),c5_2(x2,x3),ndr1_1(x2),c7_2(x2,x4),c3_2(x2,x4) -> c10_2(x0,x1),c1_1(x0),c10_1(x0),c1_2(x2,x3),c2_2(x2,x4),c5_1(x2),c4_2(a71,a72)
% 117.52/24.12 691:15:5:[505.1,499.3]:TopTopTopTopTop: c8_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c8_2(x2,x3),c5_2(x2,x3),ndr1_1(x2),c7_2(x2,x4),c3_2(x2,x4) -> c10_2(x0,x1),c1_1(x0),c10_1(x0),c1_2(x2,x3),c2_2(x2,x4),c5_1(x2),ndr1_1(a71)
% 117.52/24.12 690:16:6:[505.1,498.0]:TopTopTopTopTopTop: c9_2(x0,x1),ndr1_1(x0),c9_2(x0,x2),ndr1_1(x3),c5_2(x3,a129),c9_1(x3) -> c1_1(x4),c5_1(x4),c8_2(x0,x1),c7_2(x0,x1),c1_2(x0,x2),c2_2(x0,x2),c4_1(x0),c9_2(x3,x5),c7_2(x3,x5),c4_2(x3,x5)
% 117.52/24.12 689:15:5:[505.1,497.5]:TopTopTopTopTop: c7_2(x0,x1),ndr1_1(x0),c1_2(x0,x2),c2_2(x0,x2),c7_2(x0,x2),c2_2(x3,x4),ndr1_1(x3),c1_1(x3) -> c10_2(x0,x1),c2_2(x0,x1),c3_1(x0),c8_2(x3,x4),c6_2(x3,x4),c5_1(x3),c5_0
% 117.52/24.12 688:16:6:[505.1,496.0]:TopTopTopTopTopTop: c9_2(x0,x1),ndr1_1(x0),c9_2(x0,x2),ndr1_1(x3),c9_1(x3) -> c1_1(x4),c5_1(x4),c8_2(x0,x1),c7_2(x0,x1),c1_2(x0,x2),c2_2(x0,x2),c4_1(x0),c9_2(x3,x5),c7_2(x3,x5),c4_2(x3,x5),c1_2(x3,a129)
% 117.52/24.12 687:16:6:[505.1,495.0]:TopTopTopTopTopTop: c9_2(x0,x1),ndr1_1(x0),c9_2(x0,x2),ndr1_1(x3),c9_1(x3) -> c1_1(x4),c5_1(x4),c8_2(x0,x1),c7_2(x0,x1),c1_2(x0,x2),c2_2(x0,x2),c4_1(x0),c9_2(x3,x5),c7_2(x3,x5),c4_2(x3,x5),c6_2(x3,a129)
% 117.52/24.12 686:13:4:[505.1,494.5]:TopTopTopTop: ssSkC2,c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c7_1(x0),c8_2(x2,x3),c1_2(x2,x3),ndr1_1(x2),c9_2(x2,a11),c3_1(x2) -> c3_2(x0,x1),c10_1(x0),c4_2(x2,x3)
% 117.52/24.12 685:13:4:[505.1,493.5]:TopTopTopTop: ssSkC2,c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c7_1(x0),c8_2(x2,x3),c1_2(x2,x3),ndr1_1(x2),c3_1(x2) -> c3_2(x0,x1),c10_1(x0),c4_2(x2,x3),c2_2(x2,a11)
% 117.52/24.12 684:13:4:[505.1,492.5]:TopTopTopTop: ssSkC2,c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c7_1(x0),c8_2(x2,x3),c1_2(x2,x3),ndr1_1(x2),c3_1(x2) -> c3_2(x0,x1),c10_1(x0),c4_2(x2,x3),c1_2(x2,a11)
% 117.52/24.12 683:12:4:[505.1,491.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c10_2(a73,x3),c7_2(a73,x3),ndr1_1(a73) -> c7_2(x0,x1),c6_2(x0,x1),c9_2(x0,x2),c2_2(x0,x2),c8_1(x0),c5_2(a73,x3)
% 117.52/24.12 682:12:4:[505.1,490.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c5_1(x0),c1_2(x2,x3),ndr1_1(x2),c1_2(x2,a104),c6_1(x2),c6_0 -> c3_2(x0,x1),c10_2(x0,x1),c9_1(x0),c4_2(x2,x3)
% 117.52/24.12 681:12:4:[505.1,489.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c5_1(x0),c1_2(x2,x3),ndr1_1(x2),c4_2(x2,a104),c6_1(x2),c6_0 -> c3_2(x0,x1),c10_2(x0,x1),c9_1(x0),c4_2(x2,x3)
% 117.52/24.12 680:11:3:[505.1,488.3]:TopTopTop: c10_2(x0,x1),ndr1_1(x0),c10_1(x0),c9_2(a15,x2),c4_2(a15,x2),c6_2(a15,x2),ndr1_1(a15) -> c7_2(x0,x1),c6_2(x0,x1),c3_1(x0),c8_0
% 117.52/24.12 506:2:0:[202.0,109.2]:: c2_0 -> c1_0
% 117.52/24.12 679:12:4:[505.1,487.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c5_1(x0),c1_2(x2,x3),ndr1_1(x2),c6_1(x2),c6_0 -> c3_2(x0,x1),c10_2(x0,x1),c9_1(x0),c4_2(x2,x3),c8_2(x2,a104)
% 117.52/24.12 678:11:3:[505.1,486.3]:TopTopTop: c10_2(x0,x1),ndr1_1(x0),c10_1(x0),c2_2(a15,x2),c4_2(a15,x2),ndr1_1(a15) -> c7_2(x0,x1),c6_2(x0,x1),c3_1(x0),c5_2(a15,x2),c8_0
% 117.52/24.12 507:2:0:[3.1,174.0]:: -> ndr1_1(a114),c2_0
% 117.52/24.12 677:12:4:[505.1,485.5]:TopTopTopTop: c1_2(x0,x1),c10_2(x0,x1),ndr1_1(x0),c1_2(x0,x2),c9_2(x0,x2) -> c9_2(x0,x1),c9_2(x0,x3),c3_2(x0,x3),c1_2(x0,x3),c10_2(x0,x2),c10_0,c6_0
% 117.52/24.12 676:10:3:[505.1,484.9]:TopTopTop: ssSkC8,ssSkC9,c9_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c6_2(x0,x2),c3_2(x0,x2),c4_2(x0,a40) -> c7_2(x0,x1)
% 117.52/24.12 675:10:3:[505.1,483.9]:TopTopTop: ssSkC8,ssSkC9,c9_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c6_2(x0,x2),c3_2(x0,x2),c3_2(x0,a40) -> c7_2(x0,x1)
% 117.52/24.12 674:10:3:[505.1,482.6]:TopTopTop: c4_2(x0,x1),c9_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c8_2(x0,a43),c5_0 -> c4_2(x0,x2),c2_2(x0,x2),c3_0
% 117.52/24.12 508:2:0:[3.1,266.0]:: -> c2_2(a114,a115),c2_0
% 117.52/24.12 509:2:0:[3.1,267.1]:: c1_1(a114) -> c2_0
% 117.52/24.12 510:2:0:[3.1,296.1]:: c5_2(a114,a115) -> c2_0
% 117.52/24.12 511:2:0:[3.1,297.1]:: c4_2(a114,a115) -> c2_0
% 117.52/24.12 512:3:1:[505.1,306.2]:Top: ssSkC5,c6_1(x0) -> ndr1_1(a22)
% 117.52/24.12 513:3:1:[505.1,307.2]:Top: ssSkC5,c6_1(x0) -> c8_1(a22)
% 117.52/24.12 514:3:1:[505.1,308.1]:Top: c3_1(x0) -> ndr1_1(x0),ssSkC28
% 117.52/24.12 515:3:1:[505.1,318.1]:Top: c3_1(x0),c4_0 -> ndr1_1(x0)
% 117.52/24.12 517:3:1:[61.1,319.0,505.1,516.1]:Top: -> ndr1_1(x0),c9_1(x0),ssSkC13
% 117.52/24.12 520:3:1:[52.1,320.0,51.1,518.1,505.1,519.2]:Top: -> ndr1_1(x0),c2_0,c3_0
% 117.52/24.12 522:3:1:[53.1,321.0,505.1,521.1]:Top: c7_0 -> ndr1_1(x0),c7_1(x0)
% 117.52/24.12 523:3:1:[505.1,322.2]:Top: ssSkC5,c6_1(x0) -> c2_2(a22,a23)
% 117.52/24.12 524:3:1:[505.1,323.2]:Top: ssSkC5,c6_1(x0) -> c7_2(a22,a23)
% 117.52/24.12 525:3:1:[505.1,324.2]:Top: ssSkC5,c6_1(x0) -> c10_2(a22,a23)
% 117.52/24.12 526:3:1:[505.1,325.1]:Top: c3_1(x0) -> c5_2(x0,a132),ssSkC28
% 117.52/24.12 527:3:1:[505.1,326.1]:Top: c3_1(x0),c4_0 -> c8_2(x0,a25)
% 117.52/24.12 528:3:1:[505.1,327.1]:Top: c3_1(x0),c4_0 -> c5_2(x0,a25)
% 117.52/24.12 529:3:1:[505.1,328.1]:Top: c3_1(x0),c4_0 -> c3_2(x0,a25)
% 117.52/24.12 530:4:1:[505.1,329.2]:Top: ssSkC0,c7_1(x0) -> c6_1(x0),ndr1_1(a3)
% 117.52/24.12 531:4:1:[505.1,330.0]:Top: c6_0,c5_0 -> c10_1(x0),c4_1(x0)
% 117.52/24.12 532:4:1:[505.1,331.1]:Top: c1_1(x0) -> ndr1_1(x0),c9_1(x0),ssSkC30
% 117.52/24.12 533:4:1:[505.1,332.1]:Top: c4_1(x0) -> ndr1_1(x0),c5_1(x0),ssSkC29
% 117.52/24.12 534:4:1:[505.1,333.1]:Top: ssSkP1(x0) -> c3_2(x0,a58),c9_1(x0),ssSkC13
% 117.52/24.12 535:4:1:[505.1,334.1]:Top: ssSkP1(x0) -> c2_2(x0,a58),c9_1(x0),ssSkC13
% 117.52/24.12 536:5:1:[505.1,335.2]:Top: ssSkC18,c6_1(x0) -> ndr1_1(x0),c4_1(x0),c4_0
% 117.52/24.12 537:4:1:[505.1,336.1]:Top: ssSkP5(x0),c7_0 -> c10_2(x0,a80),c7_1(x0)
% 117.52/24.12 538:4:1:[505.1,337.1]:Top: ssSkP5(x0),c7_0 -> c3_2(x0,a80),c7_1(x0)
% 117.52/24.12 539:3:1:[505.1,338.2]:Top: ssSkC5,c6_1(x0),c6_2(a22,a24) ->
% 117.52/24.12 540:3:1:[505.1,339.2]:Top: ssSkC5,c6_1(x0),c1_2(a22,a24) ->
% 117.52/24.12 541:3:1:[505.1,340.2]:Top: ssSkC5,c6_1(x0),c2_2(a22,a24) ->
% 117.52/24.12 542:3:1:[505.1,341.2]:Top: c4_2(x0,a132),c3_1(x0) -> ssSkC28
% 117.52/24.12 543:3:1:[505.1,342.2]:Top: c8_2(x0,a132),c3_1(x0) -> ssSkC28
% 117.52/24.12 544:3:1:[73.0,344.0]:Top: -> c4_2(a9,x0),c5_2(a9,x0),ssSkC2
% 117.52/24.12 545:4:1:[505.1,345.2]:Top: ssSkC0,c7_1(x0) -> c6_1(x0),c7_2(a3,a5)
% 117.52/24.12 546:4:1:[505.1,346.2]:Top: ssSkC0,c7_1(x0) -> c6_1(x0),c1_2(a3,a4)
% 117.52/24.12 547:4:1:[505.1,347.2]:Top: ssSkC0,c7_1(x0) -> c6_1(x0),c5_2(a3,a4)
% 117.52/24.12 548:4:1:[505.1,348.2]:Top: ssSkC0,c7_1(x0),c1_1(a3) -> c6_1(x0)
% 117.52/24.12 549:4:1:[505.1,349.1]:Top: c1_1(x0) -> c3_2(x0,a145),c9_1(x0),ssSkC30
% 117.52/24.12 550:4:1:[505.1,350.1]:Top: c1_1(x0) -> c1_2(x0,a145),c9_1(x0),ssSkC30
% 117.52/24.12 551:4:1:[505.1,351.1]:Top: c4_1(x0) -> c4_2(x0,a138),c5_1(x0),ssSkC29
% 117.52/24.12 552:4:1:[505.1,352.2]:Top: c4_1(x0),c2_1(x0) -> ndr1_1(x0),ssSkC24
% 117.52/24.12 553:4:1:[505.1,353.2]:Top: ssSkP1(x0),c4_2(x0,a58) -> c9_1(x0),ssSkC13
% 117.52/24.12 554:5:1:[505.1,354.4]:Top: ssSkC27,ssSkC28,c6_1(x0),c10_1(x0) -> ndr1_1(x0)
% 117.52/24.12 555:5:1:[505.1,355.2]:Top: ssSkC18,c6_1(x0) -> c10_2(x0,a89),c4_1(x0),c4_0
% 117.52/24.12 556:5:1:[505.1,356.2]:Top: ssSkC18,c6_1(x0) -> c4_2(x0,a89),c4_1(x0),c4_0
% 117.52/24.12 557:5:1:[505.1,357.3]:Top: ssSkP6(x0),ssSkP7(x0),c10_2(x0,a86) -> c2_0,c3_0
% 117.52/24.12 558:5:1:[505.1,358.3]:Top: ssSkP6(x0),ssSkP7(x0),c2_2(x0,a86) -> c2_0,c3_0
% 117.52/24.12 559:5:1:[505.1,359.3]:Top: ssSkP6(x0),ssSkP7(x0),c8_2(x0,a86) -> c2_0,c3_0
% 117.52/24.12 560:4:1:[505.1,360.2]:Top: ssSkP5(x0),c4_2(x0,a80),c7_0 -> c7_1(x0)
% 117.52/24.12 561:5:1:[505.1,361.3]:Top: ssSkC15,c10_1(x0),c8_1(x0) -> ndr1_1(x0),c7_0
% 117.52/24.12 562:5:1:[505.1,362.1]:Top: c1_1(x0),c4_0 -> c7_1(x0),c3_1(x0),c6_0
% 117.52/24.12 563:3:1:[64.0,364.1]:Top: c7_2(a37,x0) -> c10_2(a37,x0),ssSkC8
% 117.52/24.12 564:4:1:[505.1,365.2]:Top: ssSkC0,c7_1(x0),c1_2(a3,a5) -> c6_1(x0)
% 117.52/24.12 565:4:1:[505.1,366.2]:Top: ssSkC0,c7_1(x0),c3_2(a3,a5) -> c6_1(x0)
% 117.52/24.12 566:4:1:[505.1,367.2]:Top: ssSkC0,c7_1(x0),c3_2(a3,a4) -> c6_1(x0)
% 117.52/24.12 567:4:1:[505.1,368.2]:Top: c5_2(x0,a145),c1_1(x0) -> c9_1(x0),ssSkC30
% 117.52/24.12 568:4:1:[505.1,369.2]:Top: c6_2(x0,a138),c4_1(x0) -> c5_1(x0),ssSkC29
% 117.52/24.12 569:4:1:[505.1,370.2]:Top: c1_2(x0,a138),c4_1(x0) -> c5_1(x0),ssSkC29
% 117.52/24.12 570:4:1:[505.1,371.2]:Top: c4_1(x0),c2_1(x0) -> c5_2(x0,a118),ssSkC24
% 117.52/24.12 571:5:1:[505.1,372.4]:Top: ssSkC27,ssSkC28,c6_1(x0),c10_1(x0) -> c7_2(x0,a133)
% 117.52/24.12 572:5:1:[505.1,373.3]:Top: ssSkC18,c9_2(x0,a89),c6_1(x0) -> c4_1(x0),c4_0
% 117.52/24.12 573:5:1:[505.1,374.3]:Top: ssSkC15,c10_1(x0),c8_1(x0) -> c4_2(x0,a67),c7_0
% 117.52/24.12 575:4:1:[58.1,375.0,505.1,574.2]:Top: c4_1(x0),c3_0,c10_0 -> ndr1_1(x0)
% 117.52/24.12 577:5:2:[62.1,376.0,505.1,576.3]:TopTop: ssSkC11,c8_1(x0) -> c1_1(x0),ndr1_1(x1),c1_1(x1)
% 117.52/24.12 578:5:1:[505.1,377.1]:Top: c8_1(x0),c8_0,c5_0 -> c5_1(x0),c7_1(x0)
% 117.52/24.12 579:4:1:[92.1,378.3]:Top: ssSkC22,c2_2(a108,x0),c7_2(a108,x0) -> c2_0
% 117.52/24.12 580:4:1:[505.1,379.3]:Top: c2_2(x0,a118),c4_1(x0),c2_1(x0) -> ssSkC24
% 117.52/24.12 581:4:1:[505.1,380.3]:Top: c9_2(x0,a118),c4_1(x0),c2_1(x0) -> ssSkC24
% 117.52/24.12 582:6:2:[505.1,382.1]:TopTop: ssSkC30,c7_1(x0),c10_1(x0) -> c6_1(x1),c7_1(x1),ndr1_1(x0)
% 117.52/24.12 583:6:2:[505.1,383.1]:TopTop: c4_1(x0),c3_1(x1) -> c3_1(x0),ndr1_1(x1),c1_1(x1),c8_0
% 117.52/24.12 584:5:1:[505.1,384.5]:Top: ssSkC27,ssSkC28,c4_2(x0,a133),c6_1(x0),c10_1(x0) ->
% 117.52/24.12 585:5:1:[505.1,385.5]:Top: ssSkC27,ssSkC28,c8_2(x0,a133),c6_1(x0),c10_1(x0) ->
% 117.52/24.12 586:5:1:[505.1,387.4]:Top: ssSkC15,c2_2(x0,a67),c10_1(x0),c8_1(x0) -> c7_0
% 117.52/24.12 587:5:1:[505.1,388.4]:Top: ssSkC15,c1_2(x0,a67),c10_1(x0),c8_1(x0) -> c7_0
% 117.52/24.12 588:5:1:[505.1,389.2]:Top: ssSkP4(x0),c4_1(x0),c3_0,c10_0 -> c4_2(x0,a65)
% 117.52/24.12 589:5:1:[505.1,390.2]:Top: ssSkP4(x0),c4_1(x0),c3_0,c10_0 -> c5_2(x0,a65)
% 117.52/24.12 591:5:2:[59.1,391.0,505.1,590.3]:TopTop: ssSkC14,c3_1(x0),c5_1(x1) -> c8_1(x0),ndr1_1(x1)
% 117.52/24.12 592:6:2:[505.1,392.3]:TopTop: ssSkP0(x0),ssSkC11,c8_1(x1) -> c1_1(x1),c1_2(x0,a50),c1_1(x0)
% 117.52/24.12 593:6:2:[505.1,393.3]:TopTop: ssSkP0(x0),ssSkC11,c8_1(x1) -> c1_1(x1),c8_2(x0,a50),c1_1(x0)
% 117.52/24.12 594:6:2:[505.1,394.3]:TopTop: ssSkP0(x0),ssSkC11,c8_1(x1) -> c1_1(x1),c10_2(x0,a50),c1_1(x0)
% 117.52/24.12 595:4:1:[68.0,395.1]:Top: c2_2(a31,x0) -> c1_2(a31,x0),c6_2(a31,x0),ssSkC6
% 117.52/24.12 596:6:2:[505.1,396.1]:TopTop: ssSkC30,c7_1(x0),c10_1(x0) -> c6_1(x1),c7_1(x1),c7_2(x0,a146)
% 117.52/24.12 597:6:2:[505.1,397.1]:TopTop: c4_1(x0),c3_1(x1) -> c3_1(x0),c7_2(x1,a142),c1_1(x1),c8_0
% 117.52/24.12 598:5:1:[505.1,398.3]:Top: ssSkP4(x0),c6_2(x0,a65),c4_1(x0),c3_0,c10_0 ->
% 117.52/24.12 599:6:2:[505.1,399.3]:TopTop: ssSkP3(x0),ssSkC14,c3_1(x1),c5_1(x0) -> c8_1(x1),c3_2(x0,a63)
% 117.52/24.12 600:6:2:[505.1,401.2]:TopTop: c8_1(x0),c2_1(x0),c4_1(x1) -> c3_1(x0),c10_1(x1),c2_0
% 117.52/24.12 601:6:2:[505.1,402.2]:TopTop: c7_2(x0,x1),ndr1_1(x0) -> c6_2(x0,x1),c1_2(x0,x1),c10_1(x0),c8_0
% 117.52/24.12 602:4:1:[45.0,403.2]:Top: c3_2(a100,x0),c7_2(a100,x0) -> c2_2(a100,x0),ssSkC21
% 117.52/24.12 603:4:1:[50.0,404.2]:Top: c1_2(a87,x0),c5_2(a87,x0) -> c6_2(a87,x0),ssSkC18
% 117.52/24.12 604:6:2:[505.1,406.1]:TopTop: ssSkC30,c9_2(x0,a146),c7_1(x0),c10_1(x0) -> c6_1(x1),c7_1(x1)
% 117.52/24.12 605:6:2:[505.1,407.1]:TopTop: ssSkC30,c1_2(x0,a146),c7_1(x0),c10_1(x0) -> c6_1(x1),c7_1(x1)
% 117.52/24.12 606:6:2:[505.1,408.1]:TopTop: c4_1(x0),c6_2(x1,a142),c3_1(x1) -> c3_1(x0),c1_1(x1),c8_0
% 117.52/24.12 607:6:2:[505.1,409.1]:TopTop: c4_1(x0),c9_2(x1,a142),c3_1(x1) -> c3_1(x0),c1_1(x1),c8_0
% 117.52/24.12 609:4:1:[507.1,410.1,3.1,608.2]:Top: c8_2(a114,x0) -> c10_2(a114,x0),c1_2(a114,x0),c2_0
% 117.52/24.12 610:6:2:[505.1,411.3]:TopTop: ssSkP3(x0),ssSkC14,c3_1(x1),c7_2(x0,a63),c5_1(x0) -> c8_1(x1)
% 117.52/24.12 611:6:2:[505.1,412.3]:TopTop: ssSkP3(x0),ssSkC14,c3_1(x1),c8_2(x0,a63),c5_1(x0) -> c8_1(x1)
% 117.52/24.12 612:4:1:[71.0,414.3]:Top: c4_2(a16,x0),c7_2(a16,x0),c10_2(a16,x0) -> ssSkC4
% 117.52/24.12 613:5:1:[283.2,417.1]:Top: c3_2(a53,x0),c1_0,c5_0 -> c1_2(a53,x0),c6_2(a53,x0)
% 117.52/24.12 614:5:1:[283.2,418.1]:Top: c10_2(a53,x0),c1_0,c5_0 -> c4_2(a53,x0),c7_2(a53,x0)
% 117.52/24.12 615:5:1:[196.1,421.2]:Top: c7_2(a26,x0),c4_2(a26,x0),c9_0 -> c8_2(a26,x0),c10_0
% 117.52/24.12 616:6:2:[505.1,422.2]:TopTop: c4_2(x0,x1),ndr1_1(x0) -> c10_2(x0,x1),c8_2(x0,x1),c5_2(x0,a111),ssSkC23
% 117.52/24.12 617:6:2:[505.1,423.2]:TopTop: c4_2(x0,x1),ndr1_1(x0) -> c10_2(x0,x1),c8_2(x0,x1),c4_2(x0,a111),ssSkC23
% 117.52/24.12 618:7:2:[505.1,424.2]:TopTop: c7_2(x0,x1),ndr1_1(x0),c10_0 -> c10_2(x0,x1),c8_2(x0,a52),c10_1(x0),c3_0
% 117.52/24.12 619:7:2:[505.1,425.2]:TopTop: c7_2(x0,x1),ndr1_1(x0),c10_0 -> c10_2(x0,x1),c3_2(x0,a52),c10_1(x0),c3_0
% 117.52/24.12 620:7:2:[505.1,428.4]:TopTop: c4_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c6_1(x0) -> c8_1(x0),c10_0,c8_0
% 117.52/24.12 621:6:2:[505.1,429.3]:TopTop: c4_2(x0,x1),ndr1_1(x0),c3_2(x0,a111) -> c10_2(x0,x1),c8_2(x0,x1),ssSkC23
% 117.52/24.12 622:7:2:[505.1,430.3]:TopTop: ssSkP2(x0),c1_2(x0,x1),ndr1_1(x0) -> c7_2(x0,x1),c5_2(x0,x1),c9_2(x0,a61),ssSkC14
% 117.52/24.12 623:5:1:[258.2,431.3]:Top: c7_2(a134,x0),c2_2(a134,x0),c5_2(a134,x0),c1_0,c10_0 ->
% 117.52/24.12 624:8:2:[505.1,432.2]:TopTop: c6_2(x0,x1),ndr1_1(x0) -> c8_2(x0,x1),c10_2(x0,x1),c1_2(x0,a130),c5_1(x0),c9_0,c2_0
% 117.52/24.12 625:7:3:[505.1,433.4]:TopTopTop: c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0) -> c6_2(x0,x1),ndr1_1(x2),c8_0
% 117.52/24.12 626:8:2:[505.1,434.2]:TopTop: ssSkC12,ndr1_1(x0),c1_1(a56) -> c2_2(x0,x1),c6_2(x0,x1),c4_2(x0,x1),c6_1(x0),c1_1(x0)
% 117.52/24.12 627:8:2:[505.1,435.2]:TopTop: ssSkC12,ndr1_1(x0),c8_1(a56) -> c2_2(x0,x1),c6_2(x0,x1),c4_2(x0,x1),c6_1(x0),c1_1(x0)
% 117.52/24.12 628:7:2:[505.1,436.3]:TopTop: c7_2(x0,x1),ndr1_1(x0),c9_2(x0,a52),c10_0 -> c10_2(x0,x1),c10_1(x0),c3_0
% 117.52/24.12 629:7:2:[505.1,437.4]:TopTop: ssSkP2(x0),c1_2(x0,x1),ndr1_1(x0),c5_2(x0,a61) -> c7_2(x0,x1),c5_2(x0,x1),ssSkC14
% 117.52/24.12 630:8:2:[505.1,438.3]:TopTop: c6_2(x0,x1),ndr1_1(x0),c7_2(x0,a130) -> c8_2(x0,x1),c10_2(x0,x1),c5_1(x0),c9_0,c2_0
% 117.52/24.12 631:8:2:[505.1,439.3]:TopTop: c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x0) -> c8_2(x0,x1),c10_1(x0),c7_1(x0),ndr1_1(a81),c9_0
% 117.52/24.12 632:7:3:[505.1,440.4]:TopTopTop: c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0) -> c6_2(x0,x1),c3_2(x2,a74),c8_0
% 117.52/24.12 633:8:2:[505.1,441.3]:TopTop: c10_2(x0,x1),ndr1_1(x0),c10_1(x0) -> c7_2(x0,x1),c6_2(x0,x1),c3_1(x0),c3_1(a15),c8_0
% 117.52/24.12 634:8:2:[505.1,442.2]:TopTop: c2_2(x0,x1),ndr1_1(x0),c8_0,c1_0 -> c4_2(x0,x1),c10_2(x0,x1),c7_1(x0),c5_1(x0)
% 117.52/24.12 635:8:2:[505.1,443.3]:TopTop: c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x0) -> c8_2(x0,x1),c10_1(x0),c7_1(x0),c3_2(a81,a82),c9_0
% 117.52/24.12 636:8:2:[505.1,444.3]:TopTop: c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c1_1(a81) -> c8_2(x0,x1),c10_1(x0),c7_1(x0),c9_0
% 117.52/24.12 637:8:2:[505.1,445.3]:TopTop: c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c9_1(a81) -> c8_2(x0,x1),c10_1(x0),c7_1(x0),c9_0
% 117.52/24.12 638:7:3:[505.1,446.4]:TopTopTop: c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0),c2_2(x2,a74) -> c6_2(x0,x1),c8_0
% 117.52/24.12 639:7:3:[505.1,447.4]:TopTopTop: c10_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0),c8_2(x2,a74) -> c6_2(x0,x1),c8_0
% 117.52/24.12 640:8:2:[505.1,448.5]:TopTop: ssSkC16,c5_2(x0,x1),ndr1_1(x0),c5_2(x0,a70),c1_1(x0) -> c3_2(x0,x1),c2_2(x0,x1),c3_0
% 117.52/24.12 641:8:2:[505.1,449.5]:TopTop: ssSkC16,c5_2(x0,x1),ndr1_1(x0),c4_2(x0,a70),c1_1(x0) -> c3_2(x0,x1),c2_2(x0,x1),c3_0
% 117.52/24.12 642:8:2:[505.1,450.5]:TopTop: ssSkC16,c5_2(x0,x1),ndr1_1(x0),c3_2(x0,a70),c1_1(x0) -> c3_2(x0,x1),c2_2(x0,x1),c3_0
% 117.52/24.12 643:8:2:[505.1,451.5]:TopTop: ssSkC3,c2_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c6_1(x0) -> c1_2(x0,x1),c2_2(x0,a14),c8_0
% 117.52/24.12 644:8:2:[505.1,452.5]:TopTop: ssSkC3,c2_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c6_1(x0) -> c1_2(x0,x1),c10_2(x0,a14),c8_0
% 117.52/24.12 645:8:2:[505.1,453.5]:TopTop: c7_2(x0,x1),c3_2(x0,x1),c6_2(x0,x1),ndr1_1(x0),c3_1(x0) -> c8_1(x0),c3_0,c1_0
% 117.52/24.12 646:8:2:[505.1,454.4]:TopTop: c8_2(x0,x1),ndr1_1(x0),c8_1(x0),c4_1(x0),c6_0 -> c2_2(x0,x1),c7_2(x0,x1),c9_0
% 117.52/24.12 647:8:2:[505.1,455.5]:TopTop: c2_2(x0,x1),c3_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c3_1(x0) -> c6_2(x0,a83),c3_0,c5_0
% 117.52/24.12 648:8:2:[505.1,456.3]:TopTop: c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c10_2(a81,a82) -> c8_2(x0,x1),c10_1(x0),c7_1(x0),c9_0
% 117.52/24.12 649:8:2:[505.1,457.3]:TopTop: c5_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c1_2(a81,a82) -> c8_2(x0,x1),c10_1(x0),c7_1(x0),c9_0
% 117.52/24.12 650:8:2:[505.1,458.5]:TopTop: ssSkC17,c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c5_1(x0),c10_0 -> c7_2(x0,x1),c7_2(x0,a76)
% 117.52/24.12 651:8:2:[505.1,459.5]:TopTop: ssSkC17,c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c5_1(x0),c10_0 -> c7_2(x0,x1),c6_2(x0,a76)
% 117.52/24.12 652:8:2:[505.1,460.5]:TopTop: ssSkC17,c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c5_1(x0),c10_0 -> c7_2(x0,x1),c8_2(x0,a76)
% 117.52/24.12 653:8:2:[505.1,461.6]:TopTop: ssSkC3,c2_2(x0,x1),c7_2(x0,x1),ndr1_1(x0),c7_2(x0,a14),c6_1(x0) -> c1_2(x0,x1),c8_0
% 117.52/24.12 654:8:2:[505.1,462.4]:TopTop: c6_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c3_1(x0),c7_0,c10_0 -> c1_2(x0,x1),c6_1(x0)
% 117.52/24.12 655:8:2:[505.1,463.6]:TopTop: ssSkC19,c4_2(x0,x1),c6_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c8_1(x0),c8_0 -> c8_2(x0,a92)
% 117.52/24.12 656:8:2:[505.1,464.6]:TopTop: ssSkC19,c4_2(x0,x1),c6_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c8_1(x0),c8_0 -> c9_2(x0,a92)
% 117.52/24.12 657:8:2:[505.1,465.6]:TopTop: ssSkC19,c4_2(x0,x1),c6_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c8_1(x0),c8_0 -> c10_2(x0,a92)
% 117.52/24.12 658:9:3:[505.1,466.5]:TopTopTop: ssSkC10,c9_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c7_2(x0,x2) -> c2_2(x0,x2),c3_2(x0,x2),c5_2(x0,a42),c9_0
% 117.52/24.12 659:9:3:[505.1,467.5]:TopTopTop: ssSkC10,c9_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c7_2(x0,x2) -> c2_2(x0,x2),c3_2(x0,x2),c4_2(x0,a42),c9_0
% 117.52/24.12 660:9:3:[505.1,468.3]:TopTopTop: c5_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c4_1(a73) -> c7_2(x0,x1),c6_2(x0,x1),c9_2(x0,x2),c2_2(x0,x2),c8_1(x0)
% 117.52/24.12 661:9:3:[505.1,469.3]:TopTopTop: c5_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c7_1(a73) -> c7_2(x0,x1),c6_2(x0,x1),c9_2(x0,x2),c2_2(x0,x2),c8_1(x0)
% 117.52/24.12 662:9:3:[505.1,470.6]:TopTopTop: ssSkC10,c9_2(x0,x1),c8_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c10_2(x0,a42) -> c2_2(x0,x2),c3_2(x0,x2),c9_0
% 117.52/24.12 663:9:3:[505.1,471.4]:TopTopTop: c3_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c7_1(x0),c4_0 -> c8_2(x0,x1),c7_2(x0,x1),c9_2(x0,x2),c6_2(x0,x2)
% 117.52/24.12 664:9:3:[505.1,472.4]:TopTopTop: c6_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c6_2(x0,x2) -> c9_2(x0,x1),c2_2(x0,x1),c9_2(x0,x2),c2_2(x0,a131),ssSkC27
% 117.52/24.12 665:9:3:[505.1,473.4]:TopTopTop: c4_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c5_2(x0,x2) -> c5_2(x0,x1),c3_2(x0,x1),c10_2(x0,x2),c2_2(x0,a39),ssSkC9
% 117.52/24.12 666:9:3:[505.1,474.5]:TopTopTop: c6_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c6_2(x0,x2),c10_2(x0,a131) -> c9_2(x0,x1),c2_2(x0,x1),c9_2(x0,x2),ssSkC27
% 117.52/24.12 667:9:3:[505.1,475.5]:TopTopTop: c6_2(x0,x1),ndr1_1(x0),c7_2(x0,x2),c6_2(x0,x2),c1_2(x0,a131) -> c9_2(x0,x1),c2_2(x0,x1),c9_2(x0,x2),ssSkC27
% 117.52/24.12 668:9:3:[505.1,476.5]:TopTopTop: c4_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c5_2(x0,x2),c9_2(x0,a39) -> c5_2(x0,x1),c3_2(x0,x1),c10_2(x0,x2),ssSkC9
% 117.52/24.12 669:9:3:[505.1,477.5]:TopTopTop: c4_2(x0,x1),ndr1_1(x0),c2_2(x0,x2),c5_2(x0,x2),c3_2(x0,a39) -> c5_2(x0,x1),c3_2(x0,x1),c10_2(x0,x2),ssSkC9
% 117.52/24.12 670:11:4:[505.1,478.2]:TopTopTopTop: c3_2(x0,x1),ndr1_1(x0),c6_2(x2,x3),ndr1_1(x2) -> c8_2(x0,x1),c7_2(x0,x1),c2_1(x0),c7_2(x2,x3),c8_2(x2,x3),c7_1(x2),c2_0
% 117.52/24.12 671:10:3:[505.1,479.5]:TopTopTop: c4_2(x0,x1),c9_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c5_0 -> c4_2(x0,x2),c2_2(x0,x2),c1_2(x0,a43),c3_0
% 117.52/24.12 672:10:3:[505.1,480.5]:TopTopTop: c4_2(x0,x1),c9_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c3_2(x0,x2),c5_0 -> c4_2(x0,x2),c2_2(x0,x2),c10_2(x0,a43),c3_0
% 117.52/24.12 673:10:3:[505.1,481.8]:TopTopTop: ssSkC8,ssSkC9,c9_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c6_2(x0,x2),c3_2(x0,x2) -> c7_2(x0,x1),c9_2(x0,a40)
% 117.52/24.12
% 117.52/24.12 Most General Atoms: ndr1_0 c5_0 c10_0 c2_0 ssSkC26 ssSkC25 ssSkC22 ssSkC21 ssSkC20 ssSkC19 ssSkC18 ssSkC17 ssSkC16 ssSkC15 ssSkC12 ssSkC11 ssSkC10 ssSkC8 ssSkC7 ssSkC6 ssSkC5 ssSkC4 ssSkC3 ssSkC2 ssSkC1 ssSkC0 c4_0 c7_0 c1_0 c2_2(x0,x1) c6_0 c8_0 ssSkP7(x0) ssSkP6(x0) ssSkP5(x0) ssSkP4(x0) ssSkP3(x0) ssSkP2(x0) ssSkP1(x0) ssSkP0(x0) ssSkC29 c3_0 ssSkC24 c8_2(x0,x2) c9_1(x0) c9_0 ssSkC23 c9_2(x0,x3) c1_2(x0,x3) c10_2(x0,x2) ssSkC9 c3_2(x0,x2) c4_2(x0,x2) ssSkC13 ssSkC28 ssSkC30 c2_1(x0) ssSkC27 ndr1_1(x1) c1_1(x1) c6_1(x1) c3_1(x1) ssSkC14 c5_1(x1) c8_1(x1) c4_1(x1) c10_1(x1) c5_2(x0,x2) c6_2(x2,x3) c7_2(x2,x3) c7_1(x2)
% 117.52/24.12
% 117.52/24.12 === Starting SPASS-SCL-FOL A Little Less Naive, considering 540 atoms initially, heuristics mode: lmodel_grow ===
% 117.52/24.12
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 589
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 638
% 117.52/24.12 === Conflict found: 533:4:1:[505.1,332.1]:Top: c4_1(x0) -> ndr1_1(x0),c5_1(x0),ssSkC29 {x0 -> a81}
% 117.52/24.12 === Backtracking. Learning clause 697:6:1:[533.1,531.4]:Top: c6_0,c5_0 -> ndr1_1(x0),c5_1(x0),ssSkC29,c10_1(x0)
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 679
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 722
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 759
% 117.52/24.12 === Conflict found: 564:4:1:[505.1,365.2]:Top: ssSkC0,c7_1(x0),c1_2(a3,a5) -> c6_1(x0) {x0 -> a81}
% 117.52/24.12 === Backtracking. Learning clause 698:5:1:[564.4,540.2]:Top: ssSkC0,c7_1(x0),c1_2(a3,a5),ssSkC5,c1_2(a22,a24) ->
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 812
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 844
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 887
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 918
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 935
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 953
% 117.52/24.12 === Conflict found: 582:6:2:[505.1,382.1]:TopTop: ssSkC30,c7_1(x0),c10_1(x0) -> c6_1(x1),c7_1(x1),ndr1_1(x0) {x0 -> a42, x1 -> a104}
% 117.52/24.12 === Backtracking. Learning clause 699:6:2:[582.2,522.3]:TopTop: ssSkC30,c10_1(x0),c7_0 -> c6_1(x1),c7_1(x1),ndr1_1(x0)
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 985
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1002
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1019
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1035
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1045
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1055
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1067
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1082
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1093
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1105
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1117
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1129
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1140
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1151
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1162
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1177
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1187
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1201
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1216
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1229
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1244
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1257
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1269
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1281
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1293
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1305
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1316
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1328
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1339
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1353
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1364
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1376
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1387
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1401
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1412
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1426
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1437
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1451
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1462
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1474
% 117.52/24.12 === Conflict found: 582:6:2:[505.1,382.1]:TopTop: ssSkC30,c7_1(x0),c10_1(x0) -> c6_1(x1),c7_1(x1),ndr1_1(x0) {x0 -> a95, x1 -> a121}
% 117.52/24.12 === Backtracking. Learning clause 700:8:2:[582.3,531.3,522.3]:TopTop: ssSkC30,c6_0,c5_0,c7_0 -> c6_1(x0),c7_1(x0),c4_1(x1),ndr1_1(x1)
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1499
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1515
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1535
% 117.52/24.12 === Conflict found: 683:12:4:[505.1,491.3]:TopTopTopTop: c5_2(x0,x1),ndr1_1(x0),c8_2(x0,x2),c10_2(a73,x3),c7_2(a73,x3),ndr1_1(a73) -> c7_2(x0,x1),c6_2(x0,x1),c9_2(x0,x2),c2_2(x0,x2),c8_1(x0),c5_2(a73,x3) {x0 -> a7, x1 -> a85, x2 -> a133, x3 -> a7}
% 117.52/24.12 === Backtracking. Learning clause 701:15:4:[683.1,629.6]:TopTopTopTop: c8_2(x0,x1),c10_2(a73,x2),c7_2(a73,x2),ndr1_1(a73),ssSkP2(x0),c1_2(x0,x3),ndr1_1(x0),c5_2(x0,a61) -> c6_2(x0,x3),c9_2(x0,x1),c2_2(x0,x1),c8_1(x0),c5_2(a73,x2),c7_2(x0,x3),ssSkC14
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1549
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1559
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1567
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1576
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1585
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1595
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1604
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1615
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1625
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1635
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1645
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1657
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1666
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1674
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1681
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1687
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1694
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1700
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1707
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1714
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1720
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1727
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1735
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1742
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1748
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1755
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1761
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1768
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1774
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1781
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1787
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1794
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1800
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1807
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1813
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1820
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1827
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1833
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1840
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1846
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1854
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1859
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1865
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1872
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1877
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1883
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1889
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1894
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1897
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1899
% 117.52/24.12 === Clause set with instances from active satisfied. Growing active. New size: 1900
% 117.52/24.12
% 117.52/24.12 Linear Model Building succeeded.
% 117.52/24.12 SZS status Satisfiable
% 117.52/24.12
% 117.52/24.12 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.52/24.12
% 117.52/24.12 SPASS-SCL-FOL Statistics:
% 117.52/24.12 Number of learned clauses: 5
% 117.52/24.12 Number of propagations: 950
% 117.52/24.12 Number of decisions: 3971
% 117.52/24.12 Number of resolutions: 6
% 117.52/24.12 Number of condensations: 0
% 117.52/24.12 Number of sub resolutions: 192
% 117.52/24.12 Number of input literals (deduplicated): 540
% 117.52/24.12 Number of grows: 105
% 117.52/24.12 Number of considered ground atoms: 1900
% 117.52/24.12
% 117.52/24.12 Needed: 0:0:23.56
% 117.52/24.12
%------------------------------------------------------------------------------