%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PUZ080+2 : TPTP v9.2.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:31:32 PM UTC 2026
% Result : Satisfiable 0.72s 0.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ080+2 : TPTP v9.2.1. Bugfixed v5.4.0.
% 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n014.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:58:37 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.72/0.90 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.90 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.90 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.90 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.90 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.90 Execution lmodel_grow ended with status: satisfiable
% 0.72/0.90 Used heuristic: lmodel_grow
% 0.72/0.90
% 0.72/0.90 Input Clauses:
% 0.72/0.92
% 0.72/0.92 Predicates: p
% 0.72/0.92 Fol Constants: n1 n2 n3 n4 n5 n6 n7 n8 n9
% 0.72/0.92 Fol Functions:
% 0.72/0.92 Problem Properties:
% 0.72/0.92 This is a first-order ground problem without equality.
% 0.72/0.92
% 0.72/0.92 After reduction: Problem Properties:
% 0.72/0.92 This is a first-order ground problem without equality.
% 0.72/0.92
% 0.72/0.92
% 0.72/0.92 Reduced Input Clauses:
% 0.72/0.92 10555:1:0:[10531.0,21.1]:: p(n1,n1,n3) ->
% 0.72/0.92 10556:1:0:[10532.0,37.1]:: p(n1,n1,n1) ->
% 0.72/0.92 10557:1:0:[10531.0,84.1]:: p(n1,n2,n3) ->
% 0.72/0.92 10558:1:0:[10532.0,100.1]:: p(n1,n2,n1) ->
% 0.72/0.92 10559:1:0:[10531.0,138.1]:: p(n1,n3,n3) ->
% 0.72/0.92 10560:1:0:[10532.0,154.1]:: p(n1,n3,n1) ->
% 0.72/0.92 10561:1:0:[10531.0,192.0]:: p(n1,n5,n3) ->
% 0.72/0.92 10562:1:0:[10532.0,199.1]:: p(n1,n4,n1) ->
% 0.72/0.92 10563:1:0:[10531.0,201.0]:: p(n1,n6,n3) ->
% 0.72/0.92 12073:3:0:[10965.1,10529.0,10977.0,12068.3,10980.1,12069.5,10739.1,12070.6,10740.1,12071.7,10741.1,12072.8]:: -> p(n7,n8,n8),p(n7,n9,n8),p(n8,n8,n8)
% 0.72/0.92 10564:1:0:[10531.0,210.0]:: p(n1,n7,n3) ->
% 0.72/0.92 12067:1:0:[10681.1,10527.0,10682.1,12060.1,10683.1,12061.2,10976.0,12062.3,10867.1,12063.4,10979.0,12064.5,10989.1,12065.6,10868.1,12066.7]:: -> p(n9,n9,n6)
% 0.72/0.92 10565:1:0:[10531.0,219.0]:: p(n1,n8,n3) ->
% 0.72/0.92 12059:5:0:[10964.1,10526.0,10975.0,12056.3,10978.0,12057.5,10988.1,12058.6]:: -> p(n7,n8,n5),p(n7,n9,n5),p(n8,n8,n5),p(n9,n8,n5),p(n9,n9,n5)
% 0.72/0.92 10566:1:0:[10531.0,228.0]:: p(n1,n9,n3) ->
% 0.72/0.92 10567:1:0:[10532.0,235.1]:: p(n1,n5,n1) ->
% 0.72/0.92 12055:3:0:[10963.1,10525.0,10876.1,12050.2,10974.0,12051.3,10877.1,12052.5,10987.1,12053.6,10879.1,12054.8]:: -> p(n7,n8,n4),p(n8,n8,n4),p(n9,n8,n4)
% 0.72/0.92 12049:2:0:[10694.1,10523.0,10695.1,12043.1,10696.1,12044.2,10973.0,12045.3,10882.1,12046.5,10986.0,12047.6,10884.1,12048.8]:: -> p(n8,n8,n2),p(n9,n8,n2)
% 0.72/0.92 12042:2:0:[10957.1,10521.0,10817.1,12036.1,10962.1,12037.2,10721.0,12038.3,10723.0,12039.4,10725.0,12040.5,10818.1,12041.7]:: -> p(n9,n4,n9),p(n9,n6,n9)
% 0.72/0.92 12035:3:0:[10804.1,10520.0,10961.1,12030.2,10805.1,12031.3,10735.1,12032.6,10736.1,12033.7,10737.1,12034.8]:: -> p(n7,n5,n8),p(n8,n5,n8),p(n8,n6,n8)
% 0.72/0.92 12029:7:0:[10956.0,10517.0,10960.1,12028.2]:: -> p(n7,n5,n5),p(n8,n4,n5),p(n8,n5,n5),p(n8,n6,n5),p(n9,n4,n5),p(n9,n5,n5),p(n9,n6,n5)
% 0.72/0.92 12027:5:0:[10807.1,10516.0,10959.1,12024.2,10808.1,12025.3,10809.1,12026.6]:: -> p(n7,n5,n4),p(n8,n5,n4),p(n8,n6,n4),p(n9,n5,n4),p(n9,n6,n4)
% 0.72/0.92 12023:3:0:[10758.1,10507.0,10953.0,12018.2,10760.1,12019.3,10971.1,12020.5,10761.1,12021.6,10982.0,12022.8]:: -> p(n7,n2,n4),p(n8,n2,n4),p(n9,n2,n4)
% 0.72/0.92 10568:1:0:[10532.0,271.0]:: p(n1,n7,n1) ->
% 0.72/0.92 12017:3:0:[10669.0,10505.0,10673.0,12012.1,10678.0,12013.2,10966.0,12014.3,10970.1,12015.5,10981.0,12016.8]:: -> p(n8,n2,n2),p(n9,n1,n2),p(n9,n2,n2)
% 0.72/0.92 10569:1:0:[10532.0,280.0]:: p(n1,n8,n1) ->
% 0.72/0.92 12011:5:0:[10852.0,10503.0,10935.1,12008.2,10855.0,12009.3,10857.0,12010.6]:: -> p(n4,n8,n9),p(n5,n8,n9),p(n5,n9,n9),p(n6,n8,n9),p(n6,n9,n9)
% 0.72/0.92 10570:1:0:[10532.0,289.0]:: p(n1,n9,n1) ->
% 0.72/0.92 12007:6:0:[10631.1,10502.0,10632.1,12005.1,10634.1,12006.2]:: -> p(n5,n7,n8),p(n5,n8,n8),p(n5,n9,n8),p(n6,n7,n8),p(n6,n8,n8),p(n6,n9,n8)
% 0.72/0.92 12004:4:0:[10883.0,10501.2,10656.1,12000.3,10657.1,12001.4,10658.1,12002.5,10885.0,12003.8]:: -> p(n4,n7,n7),p(n4,n8,n7),p(n6,n7,n7),p(n6,n8,n7)
% 0.72/0.92 11999:8:0:[10934.1,10499.2]:: -> p(n4,n7,n5),p(n4,n8,n5),p(n5,n7,n5),p(n5,n8,n5),p(n5,n9,n5),p(n6,n7,n5),p(n6,n8,n5),p(n6,n9,n5)
% 0.72/0.92 11998:5:0:[10853.0,10497.0,10933.1,11995.2,10856.0,11996.3,10858.0,11997.6]:: -> p(n4,n8,n3),p(n5,n8,n3),p(n5,n9,n3),p(n6,n8,n3),p(n6,n9,n3)
% 0.72/0.92 11994:3:0:[10851.0,10495.0,10932.0,11989.2,10854.0,11990.3,10664.1,11991.6,10665.1,11992.7,10666.1,11993.8]:: -> p(n4,n8,n1),p(n5,n8,n1),p(n5,n9,n1)
% 0.72/0.92 11988:2:0:[10928.1,10494.0,10813.1,11982.1,10931.1,11983.2,10940.1,11984.3,10814.1,11985.4,10944.1,11986.5,10816.1,11987.7]:: -> p(n6,n4,n9),p(n6,n6,n9)
% 0.72/0.92 11981:4:0:[10927.0,10490.0,10930.0,11977.2,10938.1,11978.3,10942.0,11979.5,10948.1,11980.7]:: -> p(n4,n5,n5),p(n5,n5,n5),p(n6,n4,n5),p(n6,n6,n5)
% 0.72/0.92 10571:1:0:[10533.0,331.1]:: p(n2,n1,n7) ->
% 0.72/0.92 11976:2:0:[10633.0,10487.0,10636.0,11970.1,10639.0,11971.2,10937.0,11972.3,10841.0,11973.5,10945.1,11974.7,10843.0,11975.8]:: -> p(n5,n5,n2),p(n6,n4,n2)
% 0.72/0.92 11969:4:0:[10614.0,10484.0,10622.0,11965.1,10625.0,11966.2,10780.0,11967.5,10782.0,11968.8]:: -> p(n5,n1,n8),p(n5,n2,n8),p(n6,n1,n8),p(n6,n2,n8)
% 0.72/0.92 11964:4:0:[10617.0,10482.0,10623.0,11960.1,10626.0,11961.2,10778.0,11962.5,10781.0,11963.8]:: -> p(n5,n1,n6),p(n5,n2,n6),p(n6,n1,n6),p(n6,n2,n6)
% 0.72/0.92 10572:1:0:[10534.0,360.1]:: p(n2,n1,n9) ->
% 0.72/0.92 11959:8:0:[10924.1,10481.0]:: -> p(n4,n2,n5),p(n4,n3,n5),p(n5,n1,n5),p(n5,n2,n5),p(n5,n3,n5),p(n6,n1,n5),p(n6,n2,n5),p(n6,n3,n5)
% 0.72/0.92 11958:6:0:[10759.0,10479.0,10762.0,11956.3,10763.0,11957.6]:: -> p(n4,n2,n3),p(n4,n3,n3),p(n5,n2,n3),p(n5,n3,n3),p(n6,n2,n3),p(n6,n3,n3)
% 0.72/0.92 11955:6:0:[10620.0,10478.0,10624.0,11953.1,10627.0,11954.2]:: -> p(n5,n1,n2),p(n5,n2,n2),p(n5,n3,n2),p(n6,n1,n2),p(n6,n2,n2),p(n6,n3,n2)
% 0.72/0.92 11952:3:0:[10923.0,10477.0,10777.0,11947.2,10779.0,11948.5,10659.0,11949.6,10660.0,11950.7,10661.0,11951.8]:: -> p(n4,n2,n1),p(n5,n1,n1),p(n5,n2,n1)
% 0.72/0.92 10573:1:0:[10535.0,384.1]:: p(n2,n1,n6) ->
% 0.72/0.92 11946:7:0:[10911.1,10475.4,10922.1,11945.8]:: -> p(n1,n7,n8),p(n1,n8,n8),p(n1,n9,n8),p(n2,n7,n8),p(n2,n9,n8),p(n3,n7,n8),p(n3,n8,n8)
% 0.72/0.92 11944:4:0:[10871.0,10474.2,10579.1,11940.3,10581.1,11941.4,10582.1,11942.5,10878.0,11943.8]:: -> p(n1,n7,n7),p(n1,n8,n7),p(n3,n7,n7),p(n3,n8,n7)
% 0.72/0.92 11939:7:0:[10910.0,10472.4,10920.1,11938.8]:: -> p(n1,n7,n5),p(n1,n8,n5),p(n1,n9,n5),p(n2,n7,n5),p(n2,n9,n5),p(n3,n7,n5),p(n3,n8,n5)
% 0.72/0.92 11937:2:0:[10564.1,10470.0,10565.1,11931.1,10566.1,11932.2,10848.0,11933.3,10908.0,11934.4,10850.0,11935.6,10919.0,11936.8]:: -> p(n2,n9,n3),p(n3,n8,n3)
% 0.72/0.92 11930:2:0:[10568.1,10468.0,10569.1,11924.1,10570.1,11925.2,10847.0,11926.3,10906.0,11927.4,10849.0,11928.6,10918.0,11929.8]:: -> p(n2,n9,n1),p(n3,n8,n1)
% 0.72/0.92 10574:1:0:[10533.0,403.0]:: p(n2,n3,n7) ->
% 0.72/0.92 10575:1:0:[10533.0,412.0]:: p(n2,n4,n7) ->
% 0.72/0.92 10576:1:0:[10533.0,421.0]:: p(n2,n5,n7) ->
% 0.72/0.92 10577:1:0:[10534.0,423.1]:: p(n2,n2,n9) ->
% 0.72/0.92 10578:1:0:[10533.0,430.0]:: p(n2,n6,n7) ->
% 0.72/0.92 11923:4:0:[10791.0,10466.0,10893.1,11919.2,10797.0,11920.3,10905.0,11921.4,10799.0,11922.6]:: -> p(n1,n5,n8),p(n2,n6,n8),p(n3,n5,n8),p(n3,n6,n8)
% 0.72/0.92 10579:1:0:[10533.0,439.0]:: p(n2,n7,n7) ->
% 0.72/0.92 11918:3:0:[10889.1,10464.0,10826.0,11913.2,10586.0,11914.3,10589.0,11915.4,10592.0,11916.5,10832.0,11917.8]:: -> p(n1,n5,n6),p(n3,n4,n6),p(n3,n5,n6)
% 0.72/0.92 10580:1:0:[10535.0,447.1]:: p(n2,n2,n6) ->
% 0.72/0.92 10581:1:0:[10533.0,448.0]:: p(n2,n8,n7) ->
% 0.72/0.92 11912:6:0:[10888.1,10463.0,10892.1,11910.2,10904.0,11911.4]:: -> p(n1,n5,n5),p(n2,n4,n5),p(n2,n6,n5),p(n3,n4,n5),p(n3,n5,n5),p(n3,n6,n5)
% 0.72/0.92 11909:2:0:[10793.0,10462.0,10891.1,11903.2,10798.0,11904.3,10903.0,11905.4,10606.0,11906.6,10607.0,11907.7,10608.0,11908.8]:: -> p(n1,n5,n4),p(n2,n6,n4)
% 0.72/0.92 10582:1:0:[10533.0,457.0]:: p(n2,n9,n7) ->
% 0.72/0.92 11902:4:0:[10887.0,10460.0,10829.0,11898.2,10901.0,11899.4,10831.0,11900.5,10834.0,11901.8]:: -> p(n1,n5,n2),p(n2,n4,n2),p(n3,n4,n2),p(n3,n5,n2)
% 0.72/0.92 11897:4:0:[10771.0,10457.2,10900.1,11893.4,10773.0,11894.5,10917.0,11895.6,10776.0,11896.8]:: -> p(n1,n1,n8),p(n1,n2,n8),p(n2,n1,n8),p(n3,n2,n8)
% 0.72/0.92 11892:3:0:[10770.0,10455.2,10573.0,11887.3,10580.0,11888.4,10584.0,11889.5,10915.0,11890.6,10774.0,11891.8]:: -> p(n1,n1,n6),p(n1,n2,n6),p(n3,n2,n6)
% 0.72/0.92 10583:1:0:[10534.0,477.1]:: p(n2,n3,n9) ->
% 0.72/0.92 11886:7:0:[10899.0,10454.4,10914.0,11885.6]:: -> p(n1,n1,n5),p(n1,n2,n5),p(n1,n3,n5),p(n2,n1,n5),p(n2,n3,n5),p(n3,n2,n5),p(n3,n3,n5)
% 0.72/0.92 11884:3:0:[10555.0,10452.0,10557.0,11879.1,10559.0,11880.2,10750.0,11881.3,10897.0,11882.4,10755.0,11883.6]:: -> p(n2,n3,n3),p(n3,n2,n3),p(n3,n3,n3)
% 0.72/0.92 11878:7:0:[10896.0,10451.4,10913.0,11877.6]:: -> p(n1,n1,n2),p(n1,n2,n2),p(n1,n3,n2),p(n2,n1,n2),p(n2,n3,n2),p(n3,n2,n2),p(n3,n3,n2)
% 0.72/0.92 11876:2:0:[10556.0,10450.0,10558.0,11870.1,10560.0,11871.2,10895.0,11872.4,10772.0,11873.5,10912.0,11874.6,10775.0,11875.8]:: -> p(n2,n1,n1),p(n3,n2,n1)
% 0.72/0.92 10584:1:0:[10535.0,501.1]:: p(n2,n3,n6) ->
% 0.72/0.92 11869:2:0:[11034.1,10449.0,10884.1,11863.1,10746.1,11864.2,10879.1,11865.3,10886.1,11866.6,10741.1,11867.7,11040.1,11868.8]:: -> p(n9,n9,n5),p(n9,n9,n6)
% 0.72/0.92 11862:3:0:[11033.1,10448.0,10745.1,11857.2,10868.1,11858.5,11041.1,11859.6,10740.1,11860.7,11039.1,11861.8]:: -> p(n9,n8,n2),p(n9,n8,n4),p(n9,n8,n5)
% 0.72/0.92 11856:3:0:[10830.1,10446.0,10845.1,11851.1,10744.0,11852.2,10839.1,11853.5,10842.1,11854.6,10737.1,11855.7]:: -> p(n9,n6,n4),p(n9,n6,n5),p(n9,n6,n9)
% 0.72/0.92 11850:3:0:[10822.1,10445.0,11032.1,11845.1,10743.0,11846.2,11028.1,11847.6,10736.1,11848.7,10818.1,11849.8]:: -> p(n9,n5,n4),p(n9,n5,n5),p(n9,n5,n6)
% 0.72/0.92 11844:4:0:[11027.1,10442.0,10734.0,11840.2,11024.1,11841.5,10769.1,11842.6,10733.0,11843.7]:: -> p(n9,n2,n2),p(n9,n2,n4),p(n9,n2,n5),p(n9,n2,n9)
% 0.72/0.92 11839:4:0:[10718.1,10439.0,10707.1,11835.2,10867.1,11836.5,10730.0,11837.6,10727.1,11838.8]:: -> p(n8,n8,n2),p(n8,n8,n4),p(n8,n8,n5),p(n8,n8,n8)
% 0.72/0.92 10585:1:0:[10534.0,522.1]:: p(n2,n4,n9) ->
% 0.72/0.92 11834:3:0:[10715.1,10437.0,10844.1,11829.1,10704.1,11830.2,10838.1,11831.5,10726.0,11832.6,10725.0,11833.8]:: -> p(n8,n6,n4),p(n8,n6,n5),p(n8,n6,n8)
% 0.72/0.92 11828:4:0:[10714.1,10436.0,11030.1,11824.1,10703.1,11825.2,10724.0,11826.6,10723.0,11827.8]:: -> p(n8,n5,n4),p(n8,n5,n5),p(n8,n5,n6),p(n8,n5,n8)
% 0.72/0.92 11823:2:0:[10713.1,10435.0,11029.1,11817.1,10702.1,11818.2,10808.1,11819.3,10722.0,11820.6,10805.1,11821.7,10721.0,11822.8]:: -> p(n8,n4,n5),p(n8,n4,n6)
% 0.72/0.92 11816:3:0:[10710.0,10433.0,10699.1,11811.2,11022.1,11812.5,10712.0,11813.6,11025.0,11814.7,10711.0,11815.8]:: -> p(n8,n2,n2),p(n8,n2,n4),p(n8,n2,n5)
% 0.72/0.92 10586:1:0:[10535.0,546.1]:: p(n2,n4,n6) ->
% 0.72/0.92 11810:2:0:[10698.1,10431.0,10696.1,11804.1,11038.0,11805.2,10876.1,11806.3,10683.1,11807.5,10690.1,11808.6,11037.0,11809.8]:: -> p(n7,n9,n5),p(n7,n9,n8)
% 0.72/0.92 11803:3:0:[10697.1,10430.0,10695.1,11798.1,11036.0,11799.2,10682.1,11800.5,10689.1,11801.6,11035.0,11802.8]:: -> p(n7,n8,n4),p(n7,n8,n5),p(n7,n8,n8)
% 0.72/0.92 11797:1:0:[10670.0,10423.0,10669.0,11790.1,10764.0,11791.2,10758.1,11792.3,10667.0,11793.5,10668.0,11794.6,11019.0,11795.7,10754.1,11796.8]:: -> p(n7,n1,n5)
% 0.72/0.92 11789:5:0:[10666.1,10422.0,10881.1,11786.1,10875.1,11787.3,10885.0,11788.6]:: -> p(n6,n9,n3),p(n6,n9,n5),p(n6,n9,n6),p(n6,n9,n8),p(n6,n9,n9)
% 0.72/0.92 11785:6:0:[10665.1,10421.0,11018.1,11783.1,10866.1,11784.5]:: -> p(n6,n8,n3),p(n6,n8,n4),p(n6,n8,n5),p(n6,n8,n7),p(n6,n8,n8),p(n6,n8,n9)
% 0.72/0.92 11782:3:0:[10662.0,10417.0,10794.1,11777.2,10806.1,11778.3,11013.1,11779.5,10810.0,11780.6,10802.1,11781.7]:: -> p(n6,n4,n2),p(n6,n4,n5),p(n6,n4,n9)
% 0.72/0.92 10587:1:0:[10534.0,567.0]:: p(n2,n6,n9) ->
% 0.72/0.92 11776:5:0:[10661.0,10416.0,11008.1,11773.3,10781.0,11774.5,10782.0,11775.7]:: -> p(n6,n3,n2),p(n6,n3,n3),p(n6,n3,n5),p(n6,n3,n7),p(n6,n3,n9)
% 0.72/0.92 10588:1:0:[10534.0,576.0]:: p(n2,n7,n9) ->
% 0.72/0.92 10589:1:0:[10535.0,582.1]:: p(n2,n5,n6) ->
% 0.72/0.92 11772:6:0:[10660.0,10415.0,11007.1,11770.3,10768.1,11771.6]:: -> p(n6,n2,n2),p(n6,n2,n3),p(n6,n2,n5),p(n6,n2,n6),p(n6,n2,n8),p(n6,n2,n9)
% 0.72/0.92 10590:1:0:[10534.0,585.0]:: p(n2,n8,n9) ->
% 0.72/0.92 11769:5:0:[10659.0,10414.0,10763.0,11766.2,10757.1,11767.3,10753.1,11768.8]:: -> p(n6,n1,n2),p(n6,n1,n5),p(n6,n1,n6),p(n6,n1,n7),p(n6,n1,n8)
% 0.72/0.92 11765:6:0:[10880.1,10413.1,10654.1,11763.3,10658.1,11764.6]:: -> p(n5,n9,n1),p(n5,n9,n3),p(n5,n9,n5),p(n5,n9,n6),p(n5,n9,n8),p(n5,n9,n9)
% 0.72/0.92 10591:1:0:[10534.0,594.0]:: p(n2,n9,n9) ->
% 0.72/0.92 11762:5:0:[11016.1,10412.1,10653.1,11759.3,10865.1,11760.5,10657.1,11761.6]:: -> p(n5,n8,n1),p(n5,n8,n3),p(n5,n8,n5),p(n5,n8,n8),p(n5,n8,n9)
% 0.72/0.92 11758:3:0:[10854.0,10411.0,11015.1,11753.1,10856.0,11754.2,10652.1,11755.3,10656.1,11756.6,10855.0,11757.8]:: -> p(n5,n7,n5),p(n5,n7,n6),p(n5,n7,n8)
% 0.72/0.92 10592:1:0:[10535.0,609.1]:: p(n2,n6,n6) ->
% 0.72/0.92 11752:3:0:[10821.0,10409.0,10649.1,11747.3,11012.1,11748.5,10655.0,11749.6,11009.1,11750.7,10814.1,11751.8]:: -> p(n5,n5,n2),p(n5,n5,n3),p(n5,n5,n5)
% 0.72/0.92 11746:4:0:[10779.0,10407.0,10647.0,11742.3,10778.0,11743.5,10648.0,11744.6,10780.0,11745.7]:: -> p(n5,n3,n2),p(n5,n3,n3),p(n5,n3,n5),p(n5,n3,n9)
% 0.72/0.92 11741:7:0:[10645.0,10406.3,10646.0,11740.6]:: -> p(n5,n2,n1),p(n5,n2,n2),p(n5,n2,n3),p(n5,n2,n5),p(n5,n2,n6),p(n5,n2,n8),p(n5,n2,n9)
% 0.72/0.92 11739:5:0:[10762.0,10405.2,10643.0,11736.3,10644.0,11737.6,10752.1,11738.8]:: -> p(n5,n1,n1),p(n5,n1,n2),p(n5,n1,n5),p(n5,n1,n6),p(n5,n1,n8)
% 0.72/0.92 11735:5:0:[10642.0,10403.1,10619.1,11732.3,10638.1,11733.5,10632.1,11734.7]:: -> p(n4,n8,n1),p(n4,n8,n3),p(n4,n8,n5),p(n4,n8,n7),p(n4,n8,n9)
% 0.72/0.92 10593:1:0:[10535.0,627.1]:: p(n2,n7,n6) ->
% 0.72/0.92 11731:2:0:[10851.0,10402.0,10641.0,11725.1,10853.0,11726.2,10618.1,11727.3,10637.1,11728.5,10631.1,11729.7,10852.0,11730.8]:: -> p(n4,n7,n5),p(n4,n7,n7)
% 0.72/0.92 11724:2:0:[10820.0,10400.0,10636.0,11718.1,10615.1,11719.3,10635.0,11720.5,11011.0,11721.6,10628.1,11722.7,10813.1,11723.8]:: -> p(n4,n5,n3),p(n4,n5,n5)
% 0.72/0.92 11717:4:0:[10777.0,10398.0,10627.0,11713.1,10612.1,11714.3,10626.0,11715.5,10625.0,11716.7]:: -> p(n4,n3,n3),p(n4,n3,n5),p(n4,n3,n7),p(n4,n3,n9)
% 0.72/0.92 11712:4:0:[10624.0,10397.1,10611.1,11708.3,10623.0,11709.5,10767.1,11710.6,10622.0,11711.7]:: -> p(n4,n2,n1),p(n4,n2,n3),p(n4,n2,n5),p(n4,n2,n9)
% 0.72/0.92 11707:6:0:[10610.0,10394.3,10864.1,11705.5,10601.1,11706.8]:: -> p(n3,n8,n1),p(n3,n8,n2),p(n3,n8,n3),p(n3,n8,n5),p(n3,n8,n7),p(n3,n8,n8)
% 0.72/0.92 10594:1:0:[10535.0,645.0]:: p(n2,n9,n6) ->
% 0.72/0.92 11704:4:0:[10849.0,10393.0,10850.0,11700.2,10609.0,11701.3,11006.1,11702.5,10600.1,11703.8]:: -> p(n3,n7,n2),p(n3,n7,n5),p(n3,n7,n7),p(n3,n7,n8)
% 0.72/0.92 11699:2:0:[10824.1,10392.0,10834.0,11693.1,10998.1,11694.2,10608.0,11695.3,10832.0,11696.5,10833.0,11697.6,10599.1,11698.8]:: -> p(n3,n6,n5),p(n3,n6,n8)
% 0.72/0.92 10595:1:0:[10536.0,657.0]:: p(n3,n2,n9) ->
% 0.72/0.92 10596:1:0:[10536.0,666.0]:: p(n3,n3,n9) ->
% 0.72/0.92 10597:1:0:[10536.0,675.0]:: p(n3,n4,n9) ->
% 0.72/0.92 10598:1:0:[10536.0,684.0]:: p(n3,n5,n9) ->
% 0.72/0.92 10599:1:0:[10536.0,693.0]:: p(n3,n6,n9) ->
% 0.72/0.92 10600:1:0:[10536.0,702.0]:: p(n3,n7,n9) ->
% 0.72/0.92 10601:1:0:[10536.0,711.0]:: p(n3,n8,n9) ->
% 0.72/0.92 10602:1:0:[10537.0,715.1]:: p(n3,n1,n4) ->
% 0.72/0.92 10603:1:0:[10536.0,720.0]:: p(n3,n9,n9) ->
% 0.72/0.92 11692:5:0:[10819.0,10391.0,10997.1,11689.2,10607.0,11690.3,10598.1,11691.8]:: -> p(n3,n5,n2),p(n3,n5,n5),p(n3,n5,n6),p(n3,n5,n7),p(n3,n5,n8)
% 0.72/0.92 11688:3:0:[11000.1,10390.0,10789.1,11683.2,10606.0,11684.3,10800.0,11685.6,10799.0,11686.7,10597.1,11687.8]:: -> p(n3,n4,n2),p(n3,n4,n5),p(n3,n4,n6)
% 0.72/0.92 11682:3:0:[10775.0,10389.0,10605.0,11677.3,10774.0,11678.5,10995.1,11679.6,10776.0,11680.7,10596.1,11681.8]:: -> p(n3,n3,n2),p(n3,n3,n3),p(n3,n3,n5)
% 0.72/0.92 11676:6:0:[10604.0,10388.3,10766.1,11674.6,10595.1,11675.8]:: -> p(n3,n2,n1),p(n3,n2,n2),p(n3,n2,n3),p(n3,n2,n5),p(n3,n2,n6),p(n3,n2,n8)
% 0.72/0.92 11673:4:0:[10873.0,10386.1,10872.0,11669.3,10594.1,11670.5,10582.1,11671.6,10591.1,11672.8]:: -> p(n2,n9,n1),p(n2,n9,n3),p(n2,n9,n5),p(n2,n9,n8)
% 0.72/0.92 11668:3:0:[10847.0,10384.0,10848.0,11663.2,11005.0,11664.3,10593.0,11665.5,10579.1,11666.6,10588.1,11667.8]:: -> p(n2,n7,n2),p(n2,n7,n5),p(n2,n7,n8)
% 0.72/0.92 10604:1:0:[10537.0,778.1]:: p(n3,n2,n4) ->
% 0.72/0.92 11662:3:0:[10823.1,10383.0,10831.0,11657.1,10996.1,11658.2,10592.0,11659.5,10578.1,11660.6,10587.1,11661.8]:: -> p(n2,n6,n4),p(n2,n6,n5),p(n2,n6,n8)
% 0.72/0.92 11656:2:0:[10999.1,10381.0,10788.1,11650.2,10798.0,11651.3,10586.0,11652.5,10575.1,11653.6,10797.0,11654.7,10585.0,11655.8]:: -> p(n2,n4,n2),p(n2,n4,n5)
% 0.72/0.92 11649:4:0:[10772.0,10380.0,10584.0,11645.5,10574.1,11646.6,10773.0,11647.7,10583.0,11648.8]:: -> p(n2,n3,n2),p(n2,n3,n3),p(n2,n3,n4),p(n2,n3,n5)
% 0.72/0.92 11644:4:0:[10750.0,10378.2,10749.0,11640.3,10573.0,11641.5,10571.0,11642.6,10572.0,11643.8]:: -> p(n2,n1,n1),p(n2,n1,n2),p(n2,n1,n5),p(n2,n1,n8)
% 0.72/0.92 11639:3:0:[10570.1,10377.0,10870.0,11634.1,10566.1,11635.2,10869.0,11636.3,11004.0,11637.5,10871.0,11638.6]:: -> p(n1,n9,n5),p(n1,n9,n8),p(n1,n9,n9)
% 0.72/0.92 11633:5:0:[10569.1,10376.0,10565.1,11630.2,11003.0,11631.3,10863.0,11632.5]:: -> p(n1,n8,n2),p(n1,n8,n5),p(n1,n8,n7),p(n1,n8,n8),p(n1,n8,n9)
% 0.72/0.92 10605:1:0:[10537.0,832.1]:: p(n3,n3,n4) ->
% 0.72/0.92 11629:4:0:[10568.1,10375.0,10564.1,11625.2,11002.0,11626.3,11001.0,11627.5,10846.0,11628.8]:: -> p(n1,n7,n2),p(n1,n7,n5),p(n1,n7,n7),p(n1,n7,n8)
% 0.72/0.92 11624:6:0:[10567.0,10373.0,10561.1,11622.2,10812.0,11623.8]:: -> p(n1,n5,n2),p(n1,n5,n4),p(n1,n5,n5),p(n1,n5,n6),p(n1,n5,n7),p(n1,n5,n8)
% 0.72/0.92 11621:3:0:[10560.0,10371.0,10559.0,11616.2,10770.0,11617.5,10993.0,11618.6,10771.0,11619.7,10994.0,11620.8]:: -> p(n1,n3,n2),p(n1,n3,n4),p(n1,n3,n5)
% 0.72/0.92 11615:5:0:[10558.0,10370.0,10557.0,11612.2,10765.0,11613.6,10992.0,11614.8]:: -> p(n1,n2,n2),p(n1,n2,n4),p(n1,n2,n5),p(n1,n2,n6),p(n1,n2,n8)
% 0.72/0.92 11611:4:0:[10556.0,10369.0,10555.0,11607.2,10748.0,11608.3,10991.0,11609.6,10747.0,11610.8]:: -> p(n1,n1,n2),p(n1,n1,n5),p(n1,n1,n6),p(n1,n1,n8)
% 0.72/0.92 10606:1:0:[10537.0,877.1]:: p(n3,n4,n4) ->
% 0.72/0.92 11606:3:0:[10591.1,10368.1,10603.1,11601.2,10935.1,11602.3,11037.0,11603.6,10729.1,11604.7,11040.1,11605.8]:: -> p(n1,n9,n9),p(n5,n9,n9),p(n6,n9,n9)
% 0.72/0.92 11600:5:0:[10922.1,10367.2,10634.1,11597.3,10980.1,11598.7,10741.1,11599.8]:: -> p(n1,n9,n8),p(n2,n9,n8),p(n5,n9,n8),p(n6,n9,n8),p(n7,n9,n8)
% 0.72/0.92 11596:3:0:[11004.0,10365.0,10594.1,11591.1,10921.1,11592.2,10640.1,11593.3,10683.1,11594.6,10979.0,11595.7]:: -> p(n5,n9,n6),p(n6,n9,n6),p(n9,n9,n6)
% 0.72/0.92 11590:6:0:[10920.1,10364.2,10934.1,11588.3,10978.0,11589.7]:: -> p(n1,n9,n5),p(n2,n9,n5),p(n5,n9,n5),p(n6,n9,n5),p(n7,n9,n5),p(n9,n9,n5)
% 0.72/0.92 10607:1:0:[10537.0,913.1]:: p(n3,n5,n4) ->
% 0.72/0.92 11587:3:0:[10566.1,10362.0,10919.0,11582.2,10933.1,11583.3,11038.0,11584.6,10708.1,11585.7,10746.1,11586.8]:: -> p(n2,n9,n3),p(n5,n9,n3),p(n6,n9,n3)
% 0.72/0.92 11581:2:0:[10570.1,10360.0,10918.0,11575.2,10932.0,11576.3,10666.1,11577.5,10698.1,11578.6,10719.1,11579.7,11034.1,11580.8]:: -> p(n2,n9,n1),p(n5,n9,n1)
% 0.72/0.92 11574:4:0:[10590.1,10359.1,10601.1,11570.2,11035.0,11571.6,10727.1,11572.7,11039.1,11573.8]:: -> p(n1,n8,n9),p(n4,n8,n9),p(n5,n8,n9),p(n6,n8,n9)
% 0.72/0.92 10608:1:0:[10537.0,940.1]:: p(n3,n6,n4) ->
% 0.72/0.92 11569:6:0:[10911.1,10358.1,10632.1,11567.3,10740.1,11568.8]:: -> p(n1,n8,n8),p(n3,n8,n8),p(n5,n8,n8),p(n6,n8,n8),p(n7,n8,n8),p(n8,n8,n8)
% 0.72/0.92 11566:4:0:[10581.1,10357.1,10657.1,11562.4,10689.1,11563.6,10730.0,11564.7,11041.1,11565.8]:: -> p(n1,n8,n7),p(n3,n8,n7),p(n4,n8,n7),p(n6,n8,n7)
% 0.72/0.92 10609:1:0:[10537.0,958.1]:: p(n3,n7,n4) ->
% 0.72/0.92 11561:8:0:[10910.0,10355.1]:: -> p(n1,n8,n5),p(n3,n8,n5),p(n4,n8,n5),p(n5,n8,n5),p(n6,n8,n5),p(n7,n8,n5),p(n8,n8,n5),p(n9,n8,n5)
% 0.72/0.92 10610:1:0:[10537.0,967.1]:: p(n3,n8,n4) ->
% 0.72/0.92 11560:4:0:[11003.0,10354.0,10909.0,11556.1,10610.0,11557.2,10619.1,11558.3,10653.1,11559.4]:: -> p(n6,n8,n4),p(n7,n8,n4),p(n8,n8,n4),p(n9,n8,n4)
% 0.72/0.92 10611:1:0:[10538.0,976.0]:: p(n4,n2,n4) ->
% 0.72/0.92 10612:1:0:[10538.0,985.0]:: p(n4,n3,n4) ->
% 0.72/0.92 10613:1:0:[10538.0,994.0]:: p(n4,n4,n4) ->
% 0.72/0.92 10614:1:0:[10539.0,998.1]:: p(n4,n1,n8) ->
% 0.72/0.92 10615:1:0:[10538.0,1003.0]:: p(n4,n5,n4) ->
% 0.72/0.92 11555:4:0:[10565.1,10353.0,10908.0,11551.1,11036.0,11552.6,10707.1,11553.7,10745.1,11554.8]:: -> p(n3,n8,n3),p(n4,n8,n3),p(n5,n8,n3),p(n6,n8,n3)
% 0.72/0.92 10616:1:0:[10538.0,1012.0]:: p(n4,n6,n4) ->
% 0.72/0.92 10617:1:0:[10540.0,1014.1]:: p(n4,n1,n6) ->
% 0.72/0.92 11550:4:0:[10907.0,10352.1,10642.0,11546.3,11016.1,11547.4,11018.1,11548.5,10695.1,11549.6]:: -> p(n1,n8,n2),p(n3,n8,n2),p(n8,n8,n2),p(n9,n8,n2)
% 0.72/0.92 10618:1:0:[10538.0,1021.0]:: p(n4,n7,n4) ->
% 0.72/0.92 11545:3:0:[10569.1,10351.0,10906.0,11540.1,10665.1,11541.5,10697.1,11542.6,10718.1,11543.7,11033.1,11544.8]:: -> p(n3,n8,n1),p(n4,n8,n1),p(n5,n8,n1)
% 0.72/0.92 11539:5:0:[10631.1,10349.3,10965.1,11536.6,10977.0,11537.7,10739.1,11538.8]:: -> p(n1,n7,n8),p(n2,n7,n8),p(n3,n7,n8),p(n5,n7,n8),p(n6,n7,n8)
% 0.72/0.92 10619:1:0:[10538.0,1030.0]:: p(n4,n8,n4) ->
% 0.72/0.92 11535:4:0:[10579.1,10348.1,10656.1,11531.4,10688.1,11532.6,10728.0,11533.7,10990.1,11534.8]:: -> p(n1,n7,n7),p(n3,n7,n7),p(n4,n7,n7),p(n6,n7,n7)
% 0.72/0.92 11530:2:0:[11001.0,10347.0,10593.0,11524.1,11006.1,11525.2,10637.1,11526.3,10681.1,11527.6,10976.0,11528.7,10989.1,11529.8]:: -> p(n5,n7,n6),p(n6,n7,n6)
% 0.72/0.92 10620:1:0:[10541.0,1037.1]:: p(n4,n1,n2) ->
% 0.72/0.92 10621:1:0:[10538.0,1039.0]:: p(n4,n9,n4) ->
% 0.72/0.92 11523:6:0:[10964.1,10346.6,10975.0,11521.7,10988.1,11522.8]:: -> p(n1,n7,n5),p(n2,n7,n5),p(n3,n7,n5),p(n4,n7,n5),p(n5,n7,n5),p(n6,n7,n5)
% 0.72/0.92 11520:1:0:[11002.0,10345.0,11005.0,11513.1,10609.0,11514.2,10618.1,11515.3,10652.1,11516.4,10963.1,11517.6,10974.0,11518.7,10987.1,11519.8]:: -> p(n6,n7,n4)
% 0.72/0.92 11512:3:0:[10641.0,10343.3,11015.1,11507.4,11017.1,11508.5,10694.1,11509.6,10973.0,11510.7,10986.0,11511.8]:: -> p(n1,n7,n2),p(n2,n7,n2),p(n3,n7,n2)
% 0.72/0.92 11506:2:0:[10894.1,10341.0,10587.1,11500.1,10599.1,11501.2,10931.1,11502.3,10944.1,11503.4,10962.1,11504.6,10725.0,11505.7]:: -> p(n6,n6,n9),p(n9,n6,n9)
% 0.72/0.92 10622:1:0:[10539.0,1061.1]:: p(n4,n2,n8) ->
% 0.72/0.92 11499:3:0:[10893.1,10340.0,10630.1,11494.3,10943.1,11495.4,11010.1,11496.5,10961.1,11497.6,10737.1,11498.8]:: -> p(n2,n6,n8),p(n3,n6,n8),p(n8,n6,n8)
% 0.72/0.92 11493:5:0:[10892.1,10337.0,10930.0,11490.3,10942.0,11491.4,10960.1,11492.6]:: -> p(n2,n6,n5),p(n3,n6,n5),p(n6,n6,n5),p(n8,n6,n5),p(n9,n6,n5)
% 0.72/0.92 11489:3:0:[10891.1,10336.0,10608.0,11484.2,10616.1,11485.3,10650.1,11486.4,11014.1,11487.5,10959.1,11488.6]:: -> p(n2,n6,n4),p(n8,n6,n4),p(n9,n6,n4)
% 0.72/0.92 10623:1:0:[10540.0,1077.1]:: p(n4,n2,n6) ->
% 0.72/0.92 11483:1:0:[10563.1,10335.0,10996.1,11476.1,10998.1,11477.2,10929.0,11478.3,10941.0,11479.4,10958.1,11480.6,10704.1,11481.7,10744.0,11482.8]:: -> p(n6,n6,n3)
% 0.72/0.92 11475:4:0:[10905.0,10331.1,10628.1,11471.3,11009.1,11472.4,10951.1,11473.5,10736.1,11474.8]:: -> p(n1,n5,n8),p(n3,n5,n8),p(n7,n5,n8),p(n8,n5,n8)
% 0.72/0.92 11470:2:0:[10576.1,10330.1,11011.0,11464.3,10655.0,11465.4,10950.1,11466.5,10684.1,11467.6,10724.0,11468.7,11028.1,11469.8]:: -> p(n1,n5,n7),p(n3,n5,n7)
% 0.72/0.92 11463:4:0:[10589.0,10329.1,10635.0,11459.3,11012.1,11460.4,10949.1,11461.5,10677.1,11462.6]:: -> p(n1,n5,n6),p(n3,n5,n6),p(n8,n5,n6),p(n9,n5,n6)
% 0.72/0.92 11458:7:0:[10904.0,10328.1,10948.1,11457.5]:: -> p(n1,n5,n5),p(n3,n5,n5),p(n4,n5,n5),p(n5,n5,n5),p(n7,n5,n5),p(n8,n5,n5),p(n9,n5,n5)
% 0.72/0.92 11456:4:0:[10903.0,10327.1,10607.0,11452.2,10615.1,11453.3,10649.1,11454.4,10947.1,11455.5]:: -> p(n1,n5,n4),p(n7,n5,n4),p(n8,n5,n4),p(n9,n5,n4)
% 0.72/0.92 11451:3:0:[10901.0,10325.1,10636.0,11446.3,10945.1,11447.5,10691.0,11448.6,11030.1,11449.7,11032.1,11450.8]:: -> p(n1,n5,n2),p(n3,n5,n2),p(n5,n5,n2)
% 0.72/0.92 10624:1:0:[10541.0,1100.1]:: p(n4,n2,n2) ->
% 0.72/0.92 11445:2:0:[10890.1,10323.0,10585.0,11439.1,10597.1,11440.2,10928.1,11441.3,10940.1,11442.4,10957.1,11443.6,10721.0,11444.7]:: -> p(n6,n4,n9),p(n9,n4,n9)
% 0.72/0.92 11438:3:0:[10889.1,10320.0,10586.0,11433.1,10629.0,11434.3,10939.1,11435.4,11013.1,11436.5,10675.1,11437.6]:: -> p(n3,n4,n6),p(n8,n4,n6),p(n9,n4,n6)
% 0.72/0.92 11432:5:0:[10888.1,10319.0,10927.0,11429.3,10938.1,11430.4,10956.0,11431.6]:: -> p(n2,n4,n5),p(n3,n4,n5),p(n6,n4,n5),p(n8,n4,n5),p(n9,n4,n5)
% 0.72/0.92 11428:3:0:[10887.0,10316.0,10633.0,11423.3,10937.0,11424.4,10685.0,11425.6,11029.1,11426.7,11031.1,11427.8]:: -> p(n2,n4,n2),p(n3,n4,n2),p(n6,n4,n2)
% 0.72/0.92 10625:1:0:[10539.0,1115.1]:: p(n4,n3,n8) ->
% 0.72/0.92 11422:3:0:[10994.0,10314.0,10583.0,11417.1,10596.1,11418.2,10955.1,11419.6,10717.0,11420.7,10985.1,11421.8]:: -> p(n4,n3,n9),p(n5,n3,n9),p(n6,n3,n9)
% 0.72/0.92 11416:2:0:[10993.0,10312.0,10574.1,11410.1,10995.1,11411.2,10648.0,11412.4,10676.0,11413.6,10720.0,11414.7,10984.0,11415.8]:: -> p(n4,n3,n7),p(n6,n3,n7)
% 0.72/0.92 11409:6:0:[10954.0,10310.6,10972.1,11407.7,10983.0,11408.8]:: -> p(n1,n3,n5),p(n2,n3,n5),p(n3,n3,n5),p(n4,n3,n5),p(n5,n3,n5),p(n6,n3,n5)
% 0.72/0.92 10626:1:0:[10540.0,1131.1]:: p(n4,n3,n6) ->
% 0.72/0.92 11406:2:0:[10605.0,10309.2,10612.1,11400.3,10647.0,11401.4,11008.1,11402.5,10953.0,11403.6,10971.1,11404.7,10982.0,11405.8]:: -> p(n1,n3,n4),p(n2,n3,n4)
% 0.72/0.92 11399:5:0:[10559.0,10308.0,10952.0,11396.6,10701.1,11397.7,10738.0,11398.8]:: -> p(n2,n3,n3),p(n3,n3,n3),p(n4,n3,n3),p(n5,n3,n3),p(n6,n3,n3)
% 0.72/0.92 11395:5:0:[10627.0,10307.3,10678.0,11392.6,10970.1,11393.7,10981.0,11394.8]:: -> p(n1,n3,n2),p(n2,n3,n2),p(n3,n3,n2),p(n5,n3,n2),p(n6,n3,n2)
% 0.72/0.92 11391:4:0:[10900.1,10304.1,10622.0,11387.3,11021.0,11388.6,11025.0,11389.7,10733.0,11390.8]:: -> p(n1,n2,n8),p(n3,n2,n8),p(n5,n2,n8),p(n6,n2,n8)
% 0.72/0.92 11386:4:0:[10580.0,10302.1,10623.0,11382.3,10671.0,11383.6,11022.1,11384.7,11024.1,11385.8]:: -> p(n1,n2,n6),p(n3,n2,n6),p(n5,n2,n6),p(n6,n2,n6)
% 0.72/0.92 11381:8:0:[10899.0,10301.1]:: -> p(n1,n2,n5),p(n3,n2,n5),p(n4,n2,n5),p(n5,n2,n5),p(n6,n2,n5),p(n7,n2,n5),p(n8,n2,n5),p(n9,n2,n5)
% 0.72/0.92 11380:4:0:[10898.0,10300.1,10604.0,11376.2,10611.1,11377.3,10645.0,11378.4,11007.1,11379.5]:: -> p(n1,n2,n4),p(n7,n2,n4),p(n8,n2,n4),p(n9,n2,n4)
% 0.72/0.92 10627:1:0:[10541.0,1154.1]:: p(n4,n3,n2) ->
% 0.72/0.92 11375:4:0:[10557.0,10299.0,10897.0,11371.1,11020.0,11372.6,10699.1,11373.7,10734.0,11374.8]:: -> p(n3,n2,n3),p(n4,n2,n3),p(n5,n2,n3),p(n6,n2,n3)
% 0.72/0.92 11370:6:0:[10896.0,10298.1,10624.0,11368.3,10673.0,11369.6]:: -> p(n1,n2,n2),p(n3,n2,n2),p(n5,n2,n2),p(n6,n2,n2),p(n8,n2,n2),p(n9,n2,n2)
% 0.72/0.92 11367:3:0:[10558.0,10297.0,10895.0,11362.1,10660.0,11363.5,10674.0,11364.6,10710.0,11365.7,11027.1,11366.8]:: -> p(n3,n2,n1),p(n4,n2,n1),p(n5,n2,n1)
% 0.72/0.92 11361:4:0:[10917.0,10295.2,10614.0,11357.3,11019.0,11358.6,10969.1,11359.7,10731.0,11360.8]:: -> p(n1,n1,n8),p(n2,n1,n8),p(n5,n1,n8),p(n6,n1,n8)
% 0.72/0.92 10628:1:0:[10539.0,1169.0]:: p(n4,n5,n8) ->
% 0.72/0.92 11356:3:0:[10573.0,10293.1,10915.0,11351.2,10617.0,11352.3,10667.0,11353.6,10968.1,11354.7,11023.1,11355.8]:: -> p(n1,n1,n6),p(n5,n1,n6),p(n6,n1,n6)
% 0.72/0.92 10629:1:0:[10540.0,1176.1]:: p(n4,n4,n6) ->
% 0.72/0.92 10630:1:0:[10539.0,1178.0]:: p(n4,n6,n8) ->
% 0.72/0.92 11350:6:0:[10914.0,10292.2,10924.1,11348.3,10967.1,11349.7]:: -> p(n1,n1,n5),p(n2,n1,n5),p(n5,n1,n5),p(n6,n1,n5),p(n7,n1,n5),p(n9,n1,n5)
% 0.72/0.92 11347:5:0:[10913.0,10289.2,10620.0,11344.3,10669.0,11345.6,10966.0,11346.7]:: -> p(n1,n1,n2),p(n2,n1,n2),p(n5,n1,n2),p(n6,n1,n2),p(n9,n1,n2)
% 0.72/0.92 10631:1:0:[10539.0,1187.0]:: p(n4,n7,n8) ->
% 0.72/0.92 11343:2:0:[10556.0,10288.0,10912.0,11337.2,10923.0,11338.3,10659.0,11339.5,10670.0,11340.6,10700.0,11341.7,11026.1,11342.8]:: -> p(n2,n1,n1),p(n5,n1,n1)
% 0.72/0.92 11336:3:0:[10756.1,10287.0,10985.1,11331.2,10818.1,11332.4,10862.1,11333.6,11039.1,11334.7,11040.1,11335.8]:: -> p(n9,n2,n9),p(n9,n4,n9),p(n9,n6,n9)
% 0.72/0.92 10632:1:0:[10539.0,1196.0]:: p(n4,n8,n8) ->
% 0.72/0.92 10633:1:0:[10541.0,1199.1]:: p(n4,n4,n2) ->
% 0.72/0.92 11330:1:0:[10769.1,10285.1,10984.0,11323.2,10811.1,11324.3,11028.1,11325.4,10842.1,11326.5,10990.1,11327.6,11041.1,11328.7,10886.1,11329.8]:: -> p(n9,n1,n7)
% 0.72/0.92 11322:3:0:[11023.1,10284.0,11024.1,11317.1,10784.1,11318.2,10839.1,11319.5,10989.1,11320.6,10868.1,11321.7]:: -> p(n9,n4,n6),p(n9,n5,n6),p(n9,n9,n6)
% 0.72/0.92 10634:1:0:[10539.0,1205.0]:: p(n4,n9,n8) ->
% 0.72/0.92 11316:7:0:[10983.0,10283.2,10988.1,11315.6]:: -> p(n9,n1,n5),p(n9,n2,n5),p(n9,n4,n5),p(n9,n5,n5),p(n9,n6,n5),p(n9,n8,n5),p(n9,n9,n5)
% 0.72/0.92 10635:1:0:[10540.0,1212.1]:: p(n4,n5,n6) ->
% 0.72/0.92 11314:4:0:[10761.1,10282.0,10982.0,11310.2,10809.1,11311.3,10987.1,11312.6,10879.1,11313.8]:: -> p(n9,n2,n4),p(n9,n5,n4),p(n9,n6,n4),p(n9,n8,n4)
% 0.72/0.92 11309:3:0:[10981.0,10280.2,11031.1,11304.3,11032.1,11305.4,10845.1,11306.5,10986.0,11307.6,10884.1,11308.8]:: -> p(n9,n1,n2),p(n9,n2,n2),p(n9,n8,n2)
% 0.72/0.92 11303:1:0:[11026.1,10279.0,11027.1,11296.1,10786.1,11297.2,10822.1,11298.4,10830.1,11299.5,10860.1,11300.6,11033.1,11301.7,11034.1,11302.8]:: -> p(n9,n4,n1)
% 0.72/0.92 11295:3:0:[10969.1,10277.0,11025.0,11290.1,10787.0,11291.2,10805.1,11292.3,10977.0,11293.6,10980.1,11294.8]:: -> p(n8,n5,n8),p(n8,n6,n8),p(n8,n8,n8)
% 0.72/0.92 11289:2:0:[10968.1,10275.0,11022.1,11283.1,10783.1,11284.2,10838.1,11285.5,10976.0,11286.6,10867.1,11287.7,10979.0,11288.8]:: -> p(n8,n4,n6),p(n8,n5,n6)
% 0.72/0.92 11282:5:0:[10967.1,10274.0,10972.1,11279.2,10975.0,11280.6,10978.0,11281.8]:: -> p(n8,n2,n5),p(n8,n4,n5),p(n8,n5,n5),p(n8,n6,n5),p(n8,n8,n5)
% 0.72/0.92 11278:4:0:[10760.1,10273.0,10971.1,11274.2,10808.1,11275.3,10974.0,11276.6,10877.1,11277.8]:: -> p(n8,n2,n4),p(n8,n5,n4),p(n8,n6,n4),p(n8,n8,n4)
% 0.72/0.92 10636:1:0:[10541.0,1235.1]:: p(n4,n5,n2) ->
% 0.72/0.92 11273:2:0:[10966.0,10271.0,10970.1,11267.2,11029.1,11268.3,11030.1,11269.4,10844.1,11270.5,10973.0,11271.6,10882.1,11272.8]:: -> p(n8,n2,n2),p(n8,n8,n2)
% 0.72/0.92 11266:1:0:[10754.1,10269.0,10955.1,11259.2,10957.1,11260.3,10817.1,11261.4,10962.1,11262.5,10859.0,11263.6,11035.0,11264.7,11037.0,11265.8]:: -> p(n7,n2,n9)
% 0.72/0.92 11258:3:0:[11019.0,10268.0,11021.0,11253.1,10785.0,11254.2,10804.1,11255.3,10961.1,11256.5,10965.1,11257.6]:: -> p(n7,n5,n8),p(n7,n8,n8),p(n7,n9,n8)
% 0.72/0.92 11252:5:0:[10954.0,10265.2,10956.0,11249.3,10960.1,11250.5,10964.1,11251.6]:: -> p(n7,n1,n5),p(n7,n2,n5),p(n7,n5,n5),p(n7,n8,n5),p(n7,n9,n5)
% 0.72/0.92 10637:1:0:[10540.0,1248.0]:: p(n4,n7,n6) ->
% 0.72/0.92 11248:3:0:[10758.1,10264.0,10953.0,11243.2,10807.1,11244.3,10959.1,11245.5,10963.1,11246.6,10876.1,11247.8]:: -> p(n7,n2,n4),p(n7,n5,n4),p(n7,n8,n4)
% 0.72/0.92 11242:1:0:[10764.0,10263.0,11020.0,11235.1,10952.0,11236.2,10795.1,11237.3,10958.1,11238.5,10861.0,11239.6,11036.0,11240.7,11038.0,11241.8]:: -> p(n7,n5,n3)
% 0.72/0.92 10638:1:0:[10540.0,1257.0]:: p(n4,n8,n6) ->
% 0.72/0.92 11234:6:0:[10753.1,10260.0,10816.1,11232.4,10857.0,11233.6]:: -> p(n6,n2,n9),p(n6,n3,n9),p(n6,n4,n9),p(n6,n6,n9),p(n6,n8,n9),p(n6,n9,n9)
% 0.72/0.92 10639:1:0:[10541.0,1262.1]:: p(n4,n6,n2) ->
% 0.72/0.92 11231:5:0:[10782.0,10259.2,10802.1,11228.3,10951.1,11229.4,11010.1,11230.5]:: -> p(n6,n1,n8),p(n6,n2,n8),p(n6,n7,n8),p(n6,n8,n8),p(n6,n9,n8)
% 0.72/0.92 10640:1:0:[10540.0,1266.0]:: p(n4,n9,n6) ->
% 0.72/0.92 11227:4:0:[10768.1,10258.1,10810.0,11223.3,10950.1,11224.4,10840.1,11225.5,10885.0,11226.8]:: -> p(n6,n1,n7),p(n6,n3,n7),p(n6,n7,n7),p(n6,n8,n7)
% 0.72/0.92 11222:4:0:[10781.0,10257.2,11013.1,11218.3,10949.1,11219.4,10837.1,11220.5,10866.1,11221.7]:: -> p(n6,n1,n6),p(n6,n2,n6),p(n6,n7,n6),p(n6,n9,n6)
% 0.72/0.92 11217:8:0:[10948.1,10256.4]:: -> p(n6,n1,n5),p(n6,n2,n5),p(n6,n3,n5),p(n6,n4,n5),p(n6,n6,n5),p(n6,n7,n5),p(n6,n8,n5),p(n6,n9,n5)
% 0.72/0.92 11216:2:0:[10757.1,10255.0,11007.1,11210.1,11008.1,11211.2,10806.1,11212.3,10947.1,11213.4,11014.1,11214.5,10875.1,11215.8]:: -> p(n6,n7,n4),p(n6,n8,n4)
% 0.72/0.92 10641:1:0:[10541.0,1280.1]:: p(n4,n7,n2) ->
% 0.72/0.92 11209:5:0:[10763.0,10254.0,10794.1,11206.3,10946.1,11207.4,10858.0,11208.6]:: -> p(n6,n2,n3),p(n6,n3,n3),p(n6,n6,n3),p(n6,n8,n3),p(n6,n9,n3)
% 0.72/0.92 11205:4:0:[10945.1,10253.4,10843.0,11201.5,11017.1,11202.6,11018.1,11203.7,10881.1,11204.8]:: -> p(n6,n1,n2),p(n6,n2,n2),p(n6,n3,n2),p(n6,n4,n2)
% 0.72/0.92 11200:4:0:[10752.1,10251.0,10940.1,11196.3,10814.1,11197.4,10944.1,11198.5,10855.0,11199.6]:: -> p(n5,n2,n9),p(n5,n3,n9),p(n5,n8,n9),p(n5,n9,n9)
% 0.72/0.92 10642:1:0:[10541.0,1289.1]:: p(n4,n8,n2) ->
% 0.72/0.92 11195:5:0:[10780.0,10250.2,10801.1,11192.3,11009.1,11193.4,10943.1,11194.5]:: -> p(n5,n1,n8),p(n5,n2,n8),p(n5,n7,n8),p(n5,n8,n8),p(n5,n9,n8)
% 0.72/0.92 11191:4:0:[10778.0,10248.2,10939.1,11187.3,11012.1,11188.4,10835.1,11189.5,10865.1,11190.7]:: -> p(n5,n1,n6),p(n5,n2,n6),p(n5,n7,n6),p(n5,n9,n6)
% 0.72/0.92 11186:7:0:[10938.1,10247.3,10942.0,11185.5]:: -> p(n5,n1,n5),p(n5,n2,n5),p(n5,n3,n5),p(n5,n5,n5),p(n5,n7,n5),p(n5,n8,n5),p(n5,n9,n5)
% 0.72/0.92 10643:1:0:[10542.0,1318.1]:: p(n5,n1,n4) ->
% 0.72/0.92 11184:5:0:[10762.0,10245.0,10792.1,11181.3,10941.0,11182.5,10856.0,11183.6]:: -> p(n5,n2,n3),p(n5,n3,n3),p(n5,n5,n3),p(n5,n8,n3),p(n5,n9,n3)
% 0.72/0.92 11180:4:0:[10937.0,10244.3,10841.0,11176.5,11015.1,11177.6,11016.1,11178.7,10880.1,11179.8]:: -> p(n5,n1,n2),p(n5,n2,n2),p(n5,n3,n2),p(n5,n5,n2)
% 0.72/0.92 10644:1:0:[10543.0,1339.1]:: p(n5,n1,n7) ->
% 0.72/0.92 11175:4:0:[10779.0,10243.2,10936.0,11171.3,10821.0,11172.4,10827.1,11173.5,10854.0,11174.6]:: -> p(n5,n1,n1),p(n5,n2,n1),p(n5,n8,n1),p(n5,n9,n1)
% 0.72/0.92 11170:3:0:[10751.1,10242.0,10928.1,11165.3,10813.1,11166.4,10931.1,11167.5,10852.0,11168.6,10935.1,11169.8]:: -> p(n4,n2,n9),p(n4,n3,n9),p(n4,n8,n9)
% 0.72/0.92 11164:3:0:[10925.1,10240.0,10767.1,11159.1,10803.0,11160.3,11011.0,11161.4,10836.0,11162.5,10883.0,11163.8]:: -> p(n4,n3,n7),p(n4,n7,n7),p(n4,n8,n7)
% 0.72/0.92 11158:5:0:[10924.1,10238.0,10927.0,11155.3,10930.0,11156.5,10934.1,11157.8]:: -> p(n4,n2,n5),p(n4,n3,n5),p(n4,n5,n5),p(n4,n7,n5),p(n4,n8,n5)
% 0.72/0.92 11154:4:0:[10759.0,10236.0,10790.1,11150.3,10929.0,11151.5,10853.0,11152.6,10933.1,11153.8]:: -> p(n4,n2,n3),p(n4,n3,n3),p(n4,n5,n3),p(n4,n8,n3)
% 0.72/0.92 11149:2:0:[10923.0,10234.0,10777.0,11143.2,10926.0,11144.3,10820.0,11145.4,10825.1,11146.5,10851.0,11147.6,10932.0,11148.8]:: -> p(n4,n2,n1),p(n4,n8,n1)
% 0.72/0.92 10645:1:0:[10542.0,1381.1]:: p(n5,n2,n4) ->
% 0.72/0.92 11142:5:0:[10917.0,10232.0,10776.0,11139.2,10799.0,11140.3,10922.1,11141.8]:: -> p(n3,n2,n8),p(n3,n5,n8),p(n3,n6,n8),p(n3,n7,n8),p(n3,n8,n8)
% 0.72/0.92 11138:3:0:[10916.0,10231.0,10766.1,11133.1,10995.1,11134.2,10800.0,11135.3,10833.0,11136.5,10878.0,11137.8]:: -> p(n3,n5,n7),p(n3,n7,n7),p(n3,n8,n7)
% 0.72/0.92 10646:1:0:[10543.0,1402.1]:: p(n5,n2,n7) ->
% 0.72/0.92 11132:3:0:[10915.0,10230.0,10774.0,11127.2,10832.0,11128.5,11006.1,11129.6,10864.1,11130.7,10921.1,11131.8]:: -> p(n3,n2,n6),p(n3,n4,n6),p(n3,n5,n6)
% 0.72/0.92 11126:7:0:[10914.0,10229.0,10920.1,11125.8]:: -> p(n3,n2,n5),p(n3,n3,n5),p(n3,n4,n5),p(n3,n5,n5),p(n3,n6,n5),p(n3,n7,n5),p(n3,n8,n5)
% 0.72/0.92 11124:3:0:[10755.0,10227.0,10789.1,11119.3,10997.1,11120.4,10998.1,11121.5,10850.0,11122.6,10919.0,11123.8]:: -> p(n3,n2,n3),p(n3,n3,n3),p(n3,n8,n3)
% 0.72/0.92 11118:6:0:[10913.0,10226.0,10834.0,11116.5,10874.0,11117.8]:: -> p(n3,n2,n2),p(n3,n3,n2),p(n3,n4,n2),p(n3,n5,n2),p(n3,n7,n2),p(n3,n8,n2)
% 0.72/0.92 11115:2:0:[10912.0,10225.0,10775.0,11109.2,11000.1,11110.3,10819.0,11111.4,10824.1,11112.5,10849.0,11113.6,10918.0,11114.8]:: -> p(n3,n2,n1),p(n3,n8,n1)
% 0.72/0.92 11108:4:0:[10900.1,10223.1,10773.0,11104.2,10797.0,11105.3,10905.0,11106.4,10911.1,11107.7]:: -> p(n2,n1,n8),p(n2,n6,n8),p(n2,n7,n8),p(n2,n9,n8)
% 0.72/0.92 10647:1:0:[10542.0,1435.1]:: p(n5,n3,n4) ->
% 0.72/0.92 11103:6:0:[10899.0,10220.1,10904.0,11101.4,10910.0,11102.7]:: -> p(n2,n1,n5),p(n2,n3,n5),p(n2,n4,n5),p(n2,n6,n5),p(n2,n7,n5),p(n2,n9,n5)
% 0.72/0.92 11100:2:0:[10749.0,10219.0,10898.0,11094.1,10798.0,11095.3,10903.0,11096.4,11005.0,11097.6,10909.0,11098.7,10872.0,11099.8]:: -> p(n2,n3,n4),p(n2,n6,n4)
% 0.72/0.92 10648:1:0:[10543.0,1456.1]:: p(n5,n3,n7) ->
% 0.72/0.92 11093:2:0:[10750.0,10218.0,10897.0,11087.1,10788.1,11088.3,10902.0,11089.4,10996.1,11090.5,10848.0,11091.6,10908.0,11092.7]:: -> p(n2,n3,n3),p(n2,n9,n3)
% 0.72/0.92 11086:4:0:[10896.0,10217.1,10901.0,11082.4,10831.0,11083.5,10907.0,11084.7,10873.0,11085.8]:: -> p(n2,n1,n2),p(n2,n3,n2),p(n2,n4,n2),p(n2,n7,n2)
% 0.72/0.92 11081:2:0:[10895.0,10216.1,10772.0,11075.2,10999.1,11076.3,10815.0,11077.4,10823.1,11078.5,10847.0,11079.6,10906.0,11080.7]:: -> p(n2,n1,n1),p(n2,n9,n1)
% 0.72/0.92 11074:2:0:[10747.0,10215.0,10992.0,11068.1,10994.0,11069.2,10890.1,11070.3,10812.0,11071.4,10894.1,11072.5,10846.0,11073.6]:: -> p(n1,n8,n9),p(n1,n9,n9)
% 0.72/0.92 11067:6:0:[10771.0,10214.2,10791.0,11065.3,10893.1,11066.5]:: -> p(n1,n1,n8),p(n1,n2,n8),p(n1,n5,n8),p(n1,n7,n8),p(n1,n8,n8),p(n1,n9,n8)
% 0.72/0.92 11064:3:0:[10991.0,10213.0,10765.0,11059.1,10993.0,11060.2,10796.0,11061.3,10828.0,11062.5,10871.0,11063.8]:: -> p(n1,n5,n7),p(n1,n7,n7),p(n1,n8,n7)
% 0.72/0.92 10649:1:0:[10542.0,1489.0]:: p(n5,n5,n4) ->
% 0.72/0.92 10650:1:0:[10542.0,1498.0]:: p(n5,n6,n4) ->
% 0.72/0.92 10651:1:0:[10543.0,1501.1]:: p(n5,n4,n7) ->
% 0.72/0.92 10652:1:0:[10542.0,1507.0]:: p(n5,n7,n4) ->
% 0.72/0.92 11058:3:0:[10770.0,10212.2,10889.1,11053.3,10826.0,11054.5,11001.0,11055.6,10863.0,11056.7,11004.0,11057.8]:: -> p(n1,n1,n6),p(n1,n2,n6),p(n1,n5,n6)
% 0.72/0.92 10653:1:0:[10542.0,1516.0]:: p(n5,n8,n4) ->
% 0.72/0.92 11052:7:0:[10888.1,10211.3,10892.1,11051.5]:: -> p(n1,n1,n5),p(n1,n2,n5),p(n1,n3,n5),p(n1,n5,n5),p(n1,n7,n5),p(n1,n8,n5),p(n1,n9,n5)
% 0.72/0.92 10654:1:0:[10542.0,1525.0]:: p(n5,n9,n4) ->
% 0.72/0.92 11050:3:0:[10748.0,10210.0,10793.0,11045.3,10891.1,11046.5,11002.0,11047.6,11003.0,11048.7,10869.0,11049.8]:: -> p(n1,n2,n4),p(n1,n3,n4),p(n1,n5,n4)
% 0.72/0.92 11044:6:0:[10887.0,10208.3,10829.0,11042.5,10870.0,11043.8]:: -> p(n1,n1,n2),p(n1,n2,n2),p(n1,n3,n2),p(n1,n5,n2),p(n1,n7,n2),p(n1,n8,n2)
% 0.72/0.92 10655:1:0:[10543.0,1537.1]:: p(n5,n5,n7) ->
% 0.72/0.92 11041:1:0:[10552.0,10204.0]:: p(n9,n8,n7) ->
% 0.72/0.92 11040:1:0:[10551.0,10170.0]:: p(n9,n9,n9) ->
% 0.72/0.92 11039:1:0:[10551.0,10161.0]:: p(n9,n8,n9) ->
% 0.72/0.92 11038:1:0:[10554.0,10137.1]:: p(n7,n9,n3) ->
% 0.72/0.92 10656:1:0:[10543.0,1573.0]:: p(n5,n7,n7) ->
% 0.72/0.92 10657:1:0:[10543.0,1582.0]:: p(n5,n8,n7) ->
% 0.72/0.92 11037:1:0:[10551.0,10125.1]:: p(n7,n9,n9) ->
% 0.72/0.92 10658:1:0:[10543.0,1591.0]:: p(n5,n9,n7) ->
% 0.72/0.92 11036:1:0:[10554.0,10101.1]:: p(n7,n8,n3) ->
% 0.72/0.92 11035:1:0:[10551.0,10089.1]:: p(n7,n8,n9) ->
% 0.72/0.92 11034:1:0:[10548.0,10072.0]:: p(n9,n9,n1) ->
% 0.72/0.92 11033:1:0:[10548.0,10063.0]:: p(n9,n8,n1) ->
% 0.72/0.92 10659:1:0:[10544.0,1648.1]:: p(n6,n1,n1) ->
% 0.72/0.92 10660:1:0:[10544.0,1711.1]:: p(n6,n2,n1) ->
% 0.72/0.92 10661:1:0:[10544.0,1765.1]:: p(n6,n3,n1) ->
% 0.72/0.92 11032:1:0:[10547.0,9983.0]:: p(n9,n5,n2) ->
% 0.72/0.92 11031:1:0:[10547.0,9974.0]:: p(n9,n4,n2) ->
% 0.72/0.92 11030:1:0:[10547.0,9965.0]:: p(n8,n5,n2) ->
% 0.72/0.92 10662:1:0:[10544.0,1810.1]:: p(n6,n4,n1) ->
% 0.72/0.92 11029:1:0:[10547.0,9956.0]:: p(n8,n4,n2) ->
% 0.72/0.92 10663:1:0:[10544.0,1855.0]:: p(n6,n6,n1) ->
% 0.72/0.92 10664:1:0:[10544.0,1864.0]:: p(n6,n7,n1) ->
% 0.72/0.92 10665:1:0:[10544.0,1873.0]:: p(n6,n8,n1) ->
% 0.72/0.92 10666:1:0:[10544.0,1882.0]:: p(n6,n9,n1) ->
% 0.72/0.92 11028:1:0:[10546.0,9907.0]:: p(n9,n5,n7) ->
% 0.72/0.92 11027:1:0:[10550.0,9874.0]:: p(n9,n2,n1) ->
% 0.72/0.92 10667:1:0:[10545.0,1959.1]:: p(n7,n1,n6) ->
% 0.72/0.92 11026:1:0:[10550.0,9865.0]:: p(n9,n1,n1) ->
% 0.72/0.92 10668:1:0:[10546.0,1969.1]:: p(n7,n1,n7) ->
% 0.72/0.92 11025:1:0:[10553.0,9863.1]:: p(n8,n2,n8) ->
% 0.72/0.92 10669:1:0:[10547.0,1982.1]:: p(n7,n1,n2) ->
% 0.72/0.92 11024:1:0:[10545.0,9825.0]:: p(n9,n2,n6) ->
% 0.72/0.92 10670:1:0:[10548.0,1990.1]:: p(n7,n1,n1) ->
% 0.72/0.92 11023:1:0:[10545.0,9816.0]:: p(n9,n1,n6) ->
% 0.72/0.92 11022:1:0:[10545.0,9807.0]:: p(n8,n2,n6) ->
% 0.72/0.92 11021:1:0:[10553.0,9791.1]:: p(n7,n2,n8) ->
% 0.72/0.92 11020:1:0:[10549.0,9759.1]:: p(n7,n2,n3) ->
% 0.72/0.92 11019:1:0:[10553.0,9755.1]:: p(n7,n1,n8) ->
% 0.72/0.92 10671:1:0:[10545.0,2022.1]:: p(n7,n2,n6) ->
% 0.72/0.92 10672:1:0:[10546.0,2032.1]:: p(n7,n2,n7) ->
% 0.72/0.92 10673:1:0:[10547.0,2045.1]:: p(n7,n2,n2) ->
% 0.72/0.92 10674:1:0:[10548.0,2053.1]:: p(n7,n2,n1) ->
% 0.72/0.92 10675:1:0:[10545.0,2085.0]:: p(n7,n4,n6) ->
% 0.72/0.92 10676:1:0:[10546.0,2086.1]:: p(n7,n3,n7) ->
% 0.72/0.92 10677:1:0:[10545.0,2094.0]:: p(n7,n5,n6) ->
% 0.72/0.92 11018:1:0:[10541.0,9659.0]:: p(n6,n8,n2) ->
% 0.72/0.92 10678:1:0:[10547.0,2099.1]:: p(n7,n3,n2) ->
% 0.72/0.92 10679:1:0:[10545.0,2103.0]:: p(n7,n6,n6) ->
% 0.72/0.92 11017:1:0:[10541.0,9650.0]:: p(n6,n7,n2) ->
% 0.72/0.92 10680:1:0:[10548.0,2107.1]:: p(n7,n3,n1) ->
% 0.72/0.92 11016:1:0:[10541.0,9641.0]:: p(n5,n8,n2) ->
% 0.72/0.92 10681:1:0:[10545.0,2112.0]:: p(n7,n7,n6) ->
% 0.72/0.92 11015:1:0:[10541.0,9632.0]:: p(n5,n7,n2) ->
% 0.72/0.92 10682:1:0:[10545.0,2121.0]:: p(n7,n8,n6) ->
% 0.72/0.92 10683:1:0:[10545.0,2130.0]:: p(n7,n9,n6) ->
% 0.72/0.92 10684:1:0:[10546.0,2140.0]:: p(n7,n5,n7) ->
% 0.72/0.92 10685:1:0:[10547.0,2144.1]:: p(n7,n4,n2) ->
% 0.72/0.92 10686:1:0:[10546.0,2149.0]:: p(n7,n6,n7) ->
% 0.72/0.92 10687:1:0:[10548.0,2152.1]:: p(n7,n4,n1) ->
% 0.72/0.92 10688:1:0:[10546.0,2158.0]:: p(n7,n7,n7) ->
% 0.72/0.92 10689:1:0:[10546.0,2167.0]:: p(n7,n8,n7) ->
% 0.72/0.92 10690:1:0:[10546.0,2176.0]:: p(n7,n9,n7) ->
% 0.72/0.92 10691:1:0:[10547.0,2180.1]:: p(n7,n5,n2) ->
% 0.72/0.92 10692:1:0:[10548.0,2188.1]:: p(n7,n5,n1) ->
% 0.72/0.92 11014:1:0:[10542.0,9517.0]:: p(n6,n6,n4) ->
% 0.72/0.92 11013:1:0:[10540.0,9492.0]:: p(n6,n4,n6) ->
% 0.72/0.92 11012:1:0:[10540.0,9483.0]:: p(n5,n5,n6) ->
% 0.72/0.92 11011:1:0:[10543.0,9448.1]:: p(n4,n5,n7) ->
% 0.72/0.92 11010:1:0:[10539.0,9431.0]:: p(n6,n6,n8) ->
% 0.72/0.92 11009:1:0:[10539.0,9404.0]:: p(n5,n5,n8) ->
% 0.72/0.92 10693:1:0:[10548.0,2215.1]:: p(n7,n6,n1) ->
% 0.72/0.92 10694:1:0:[10547.0,2216.0]:: p(n7,n7,n2) ->
% 0.72/0.92 10695:1:0:[10547.0,2225.0]:: p(n7,n8,n2) ->
% 0.72/0.92 10696:1:0:[10547.0,2234.0]:: p(n7,n9,n2) ->
% 0.72/0.92 10697:1:0:[10548.0,2242.0]:: p(n7,n8,n1) ->
% 0.72/0.92 10698:1:0:[10548.0,2251.0]:: p(n7,n9,n1) ->
% 0.72/0.92 10699:1:0:[10549.0,2271.0]:: p(n8,n2,n3) ->
% 0.72/0.92 10700:1:0:[10550.0,2278.1]:: p(n8,n1,n1) ->
% 0.72/0.92 10701:1:0:[10549.0,2280.0]:: p(n8,n3,n3) ->
% 0.72/0.92 10702:1:0:[10549.0,2289.0]:: p(n8,n4,n3) ->
% 0.72/0.92 10703:1:0:[10549.0,2298.0]:: p(n8,n5,n3) ->
% 0.72/0.92 10704:1:0:[10549.0,2307.0]:: p(n8,n6,n3) ->
% 0.72/0.92 10705:1:0:[10549.0,2316.0]:: p(n8,n7,n3) ->
% 0.72/0.92 10706:1:0:[10551.0,2322.1]:: p(n8,n1,n9) ->
% 0.72/0.92 10707:1:0:[10549.0,2325.0]:: p(n8,n8,n3) ->
% 0.72/0.92 10708:1:0:[10549.0,2334.0]:: p(n8,n9,n3) ->
% 0.72/0.92 10709:1:0:[10552.0,2338.1]:: p(n8,n1,n7) ->
% 0.72/0.92 10710:1:0:[10550.0,2341.1]:: p(n8,n2,n1) ->
% 0.72/0.92 10711:1:0:[10551.0,2385.1]:: p(n8,n2,n9) ->
% 0.72/0.92 11008:1:0:[10538.0,9265.0]:: p(n6,n3,n4) ->
% 0.72/0.92 11007:1:0:[10538.0,9256.0]:: p(n6,n2,n4) ->
% 0.72/0.92 10712:1:0:[10552.0,2401.1]:: p(n8,n2,n7) ->
% 0.72/0.92 10713:1:0:[10550.0,2404.0]:: p(n8,n4,n1) ->
% 0.72/0.92 10714:1:0:[10550.0,2413.0]:: p(n8,n5,n1) ->
% 0.72/0.92 10715:1:0:[10550.0,2422.0]:: p(n8,n6,n1) ->
% 0.72/0.92 10716:1:0:[10550.0,2431.0]:: p(n8,n7,n1) ->
% 0.72/0.92 10717:1:0:[10551.0,2439.1]:: p(n8,n3,n9) ->
% 0.72/0.92 10718:1:0:[10550.0,2440.0]:: p(n8,n8,n1) ->
% 0.72/0.92 11006:1:0:[10535.0,9204.0]:: p(n3,n7,n6) ->
% 0.72/0.92 11005:1:0:[10537.0,9193.1]:: p(n2,n7,n4) ->
% 0.72/0.92 10719:1:0:[10550.0,2449.0]:: p(n8,n9,n1) ->
% 0.72/0.92 10720:1:0:[10552.0,2455.1]:: p(n8,n3,n7) ->
% 0.72/0.92 11004:1:0:[10535.0,9159.1]:: p(n1,n9,n6) ->
% 0.72/0.92 10721:1:0:[10551.0,2484.1]:: p(n8,n4,n9) ->
% 0.72/0.92 11003:1:0:[10537.0,9139.1]:: p(n1,n8,n4) ->
% 0.72/0.92 10722:1:0:[10552.0,2500.1]:: p(n8,n4,n7) ->
% 0.72/0.92 10723:1:0:[10551.0,2520.1]:: p(n8,n5,n9) ->
% 0.72/0.92 11002:1:0:[10537.0,9103.1]:: p(n1,n7,n4) ->
% 0.72/0.92 10724:1:0:[10552.0,2536.1]:: p(n8,n5,n7) ->
% 0.72/0.92 10725:1:0:[10551.0,2547.1]:: p(n8,n6,n9) ->
% 0.72/0.92 11001:1:0:[10535.0,9078.1]:: p(n1,n7,n6) ->
% 0.72/0.92 10726:1:0:[10552.0,2563.1]:: p(n8,n6,n7) ->
% 0.72/0.92 10727:1:0:[10551.0,2574.0]:: p(n8,n8,n9) ->
% 0.72/0.92 11000:1:0:[10532.0,9001.0]:: p(n3,n4,n1) ->
% 0.72/0.92 10728:1:0:[10552.0,2581.1]:: p(n8,n7,n7) ->
% 0.72/0.92 10729:1:0:[10551.0,2583.0]:: p(n8,n9,n9) ->
% 0.72/0.92 10999:1:0:[10532.0,8983.0]:: p(n2,n4,n1) ->
% 0.72/0.92 10730:1:0:[10552.0,2590.1]:: p(n8,n8,n7) ->
% 0.72/0.92 10731:1:0:[10553.0,2609.1]:: p(n9,n1,n8) ->
% 0.72/0.92 10732:1:0:[10554.0,2640.1]:: p(n9,n1,n3) ->
% 0.72/0.92 10733:1:0:[10553.0,2672.1]:: p(n9,n2,n8) ->
% 0.72/0.92 10998:1:0:[10531.0,8940.0]:: p(n3,n6,n3) ->
% 0.72/0.92 10997:1:0:[10531.0,8931.0]:: p(n3,n5,n3) ->
% 0.72/0.92 10996:1:0:[10531.0,8922.0]:: p(n2,n6,n3) ->
% 0.72/0.92 10734:1:0:[10554.0,2703.1]:: p(n9,n2,n3) ->
% 0.72/0.92 10995:1:0:[10533.0,8890.0]:: p(n3,n3,n7) ->
% 0.72/0.92 10735:1:0:[10553.0,2735.0]:: p(n9,n4,n8) ->
% 0.72/0.92 10736:1:0:[10553.0,2744.0]:: p(n9,n5,n8) ->
% 0.72/0.92 10737:1:0:[10553.0,2753.0]:: p(n9,n6,n8) ->
% 0.72/0.92 10738:1:0:[10554.0,2757.1]:: p(n9,n3,n3) ->
% 0.72/0.92 10739:1:0:[10553.0,2762.0]:: p(n9,n7,n8) ->
% 0.72/0.92 10740:1:0:[10553.0,2771.0]:: p(n9,n8,n8) ->
% 0.72/0.92 10741:1:0:[10553.0,2780.0]:: p(n9,n9,n8) ->
% 0.72/0.92 10742:1:0:[10554.0,2802.1]:: p(n9,n4,n3) ->
% 0.72/0.92 10994:1:0:[10536.0,8847.1]:: p(n1,n3,n9) ->
% 0.72/0.92 10993:1:0:[10533.0,8836.1]:: p(n1,n3,n7) ->
% 0.72/0.92 10743:1:0:[10554.0,2838.1]:: p(n9,n5,n3) ->
% 0.72/0.92 10992:1:0:[10536.0,8811.1]:: p(n1,n2,n9) ->
% 0.72/0.92 10744:1:0:[10554.0,2865.1]:: p(n9,n6,n3) ->
% 0.72/0.92 10745:1:0:[10554.0,2892.0]:: p(n9,n8,n3) ->
% 0.72/0.92 10746:1:0:[10554.0,2901.0]:: p(n9,n9,n3) ->
% 0.72/0.92 10991:1:0:[10533.0,8755.1]:: p(n1,n1,n7) ->
% 0.72/0.92 10747:1:0:[10536.0,2934.1]:: p(n1,n1,n9) ->
% 0.72/0.92 10748:1:0:[10538.0,2938.1]:: p(n1,n1,n4) ->
% 0.72/0.92 10990:1:0:[10554.0,8659.0]:: p(n9,n7,n7) ->
% 0.72/0.92 10989:1:0:[10554.0,8658.0]:: p(n9,n7,n6) ->
% 0.72/0.92 10988:1:0:[10554.0,8657.0]:: p(n9,n7,n5) ->
% 0.72/0.92 10987:1:0:[10554.0,8656.0]:: p(n9,n7,n4) ->
% 0.72/0.92 10986:1:0:[10554.0,8649.1]:: p(n9,n7,n2) ->
% 0.72/0.92 10749:1:0:[10538.0,3001.1]:: p(n2,n1,n4) ->
% 0.72/0.92 10985:1:0:[10553.0,8532.0]:: p(n9,n3,n9) ->
% 0.72/0.92 10984:1:0:[10553.0,8530.1]:: p(n9,n3,n7) ->
% 0.72/0.92 10983:1:0:[10553.0,8525.1]:: p(n9,n3,n5) ->
% 0.72/0.92 10982:1:0:[10553.0,8521.1]:: p(n9,n3,n4) ->
% 0.72/0.92 10981:1:0:[10553.0,8510.1]:: p(n9,n3,n2) ->
% 0.72/0.92 10750:1:0:[10549.0,3036.1]:: p(n2,n1,n3) ->
% 0.72/0.92 10751:1:0:[10536.0,3060.0]:: p(n4,n1,n9) ->
% 0.72/0.92 10752:1:0:[10536.0,3069.0]:: p(n5,n1,n9) ->
% 0.72/0.92 10753:1:0:[10536.0,3078.0]:: p(n6,n1,n9) ->
% 0.72/0.92 10754:1:0:[10536.0,3087.0]:: p(n7,n1,n9) ->
% 0.72/0.92 10755:1:0:[10549.0,3090.1]:: p(n3,n1,n3) ->
% 0.72/0.92 10980:1:0:[10552.0,8422.0]:: p(n8,n9,n8) ->
% 0.72/0.92 10979:1:0:[10552.0,8419.1]:: p(n8,n9,n6) ->
% 0.72/0.92 10978:1:0:[10552.0,8416.1]:: p(n8,n9,n5) ->
% 0.72/0.92 10756:1:0:[10536.0,3105.0]:: p(n9,n1,n9) ->
% 0.72/0.92 10977:1:0:[10551.0,8352.1]:: p(n8,n7,n8) ->
% 0.72/0.92 10976:1:0:[10551.0,8349.1]:: p(n8,n7,n6) ->
% 0.72/0.92 10757:1:0:[10538.0,3118.0]:: p(n6,n1,n4) ->
% 0.72/0.92 10975:1:0:[10551.0,8346.1]:: p(n8,n7,n5) ->
% 0.72/0.92 10974:1:0:[10551.0,8342.1]:: p(n8,n7,n4) ->
% 0.72/0.92 10758:1:0:[10538.0,3127.0]:: p(n7,n1,n4) ->
% 0.72/0.92 10973:1:0:[10551.0,8331.1]:: p(n8,n7,n2) ->
% 0.72/0.92 10759:1:0:[10549.0,3135.1]:: p(n4,n1,n3) ->
% 0.72/0.92 10760:1:0:[10538.0,3136.0]:: p(n8,n1,n4) ->
% 0.72/0.92 10761:1:0:[10538.0,3145.0]:: p(n9,n1,n4) ->
% 0.72/0.92 10972:1:0:[10550.0,8176.0]:: p(n8,n3,n5) ->
% 0.72/0.92 10971:1:0:[10550.0,8175.0]:: p(n8,n3,n4) ->
% 0.72/0.92 10970:1:0:[10550.0,8173.0]:: p(n8,n3,n2) ->
% 0.72/0.92 10762:1:0:[10549.0,3171.1]:: p(n5,n1,n3) ->
% 0.72/0.92 10969:1:0:[10549.0,8120.0]:: p(n8,n1,n8) ->
% 0.72/0.92 10968:1:0:[10549.0,8118.0]:: p(n8,n1,n6) ->
% 0.72/0.92 10967:1:0:[10549.0,8117.0]:: p(n8,n1,n5) ->
% 0.72/0.92 10966:1:0:[10549.0,8109.1]:: p(n8,n1,n2) ->
% 0.72/0.92 10763:1:0:[10549.0,3198.1]:: p(n6,n1,n3) ->
% 0.72/0.92 10764:1:0:[10549.0,3216.1]:: p(n7,n1,n3) ->
% 0.72/0.92 10965:1:0:[10548.0,7999.0]:: p(n7,n7,n8) ->
% 0.72/0.92 10964:1:0:[10548.0,7996.0]:: p(n7,n7,n5) ->
% 0.72/0.92 10963:1:0:[10548.0,7995.0]:: p(n7,n7,n4) ->
% 0.72/0.92 10962:1:0:[10547.0,7971.0]:: p(n7,n6,n9) ->
% 0.72/0.92 10961:1:0:[10547.0,7970.0]:: p(n7,n6,n8) ->
% 0.72/0.92 10960:1:0:[10547.0,7967.0]:: p(n7,n6,n5) ->
% 0.72/0.92 10959:1:0:[10547.0,7966.0]:: p(n7,n6,n4) ->
% 0.72/0.92 10958:1:0:[10547.0,7965.0]:: p(n7,n6,n3) ->
% 0.72/0.92 10957:1:0:[10546.0,7919.0]:: p(n7,n4,n9) ->
% 0.72/0.92 10956:1:0:[10546.0,7912.1]:: p(n7,n4,n5) ->
% 0.72/0.92 10765:1:0:[10533.0,3247.1]:: p(n1,n2,n7) ->
% 0.72/0.92 10955:1:0:[10545.0,7881.0]:: p(n7,n3,n9) ->
% 0.72/0.92 10954:1:0:[10545.0,7875.1]:: p(n7,n3,n5) ->
% 0.72/0.92 10953:1:0:[10545.0,7871.1]:: p(n7,n3,n4) ->
% 0.72/0.92 10952:1:0:[10545.0,7866.1]:: p(n7,n3,n3) ->
% 0.72/0.92 10766:1:0:[10533.0,3319.0]:: p(n3,n2,n7) ->
% 0.72/0.92 10767:1:0:[10533.0,3328.0]:: p(n4,n2,n7) ->
% 0.72/0.92 10768:1:0:[10533.0,3346.0]:: p(n6,n2,n7) ->
% 0.72/0.92 10769:1:0:[10533.0,3373.0]:: p(n9,n2,n7) ->
% 0.72/0.92 10951:1:0:[10544.0,7603.0]:: p(n6,n5,n8) ->
% 0.72/0.92 10950:1:0:[10544.0,7602.0]:: p(n6,n5,n7) ->
% 0.72/0.92 10949:1:0:[10544.0,7601.0]:: p(n6,n5,n6) ->
% 0.72/0.92 10948:1:0:[10544.0,7600.0]:: p(n6,n5,n5) ->
% 0.72/0.92 10947:1:0:[10544.0,7599.0]:: p(n6,n5,n4) ->
% 0.72/0.92 10946:1:0:[10544.0,7598.0]:: p(n6,n5,n3) ->
% 0.72/0.92 10945:1:0:[10544.0,7597.0]:: p(n6,n5,n2) ->
% 0.72/0.92 10944:1:0:[10543.0,7343.0]:: p(n5,n6,n9) ->
% 0.72/0.92 10943:1:0:[10543.0,7342.0]:: p(n5,n6,n8) ->
% 0.72/0.92 10942:1:0:[10543.0,7336.1]:: p(n5,n6,n5) ->
% 0.72/0.92 10941:1:0:[10543.0,7327.1]:: p(n5,n6,n3) ->
% 0.72/0.92 10940:1:0:[10542.0,7262.0]:: p(n5,n4,n9) ->
% 0.72/0.92 10939:1:0:[10542.0,7259.0]:: p(n5,n4,n6) ->
% 0.72/0.92 10938:1:0:[10542.0,7258.0]:: p(n5,n4,n5) ->
% 0.72/0.92 10937:1:0:[10542.0,7246.1]:: p(n5,n4,n2) ->
% 0.72/0.92 10936:1:0:[10542.0,7239.1]:: p(n5,n4,n1) ->
% 0.72/0.92 10770:1:0:[10545.0,3615.1]:: p(n1,n3,n6) ->
% 0.72/0.92 10771:1:0:[10553.0,3635.1]:: p(n1,n3,n8) ->
% 0.72/0.92 10772:1:0:[10550.0,3682.1]:: p(n2,n3,n1) ->
% 0.72/0.92 10935:1:0:[10541.0,7107.0]:: p(n4,n9,n9) ->
% 0.72/0.92 10934:1:0:[10541.0,7103.0]:: p(n4,n9,n5) ->
% 0.72/0.92 10933:1:0:[10541.0,7101.0]:: p(n4,n9,n3) ->
% 0.72/0.92 10932:1:0:[10541.0,7093.1]:: p(n4,n9,n1) ->
% 0.72/0.92 10773:1:0:[10553.0,3698.1]:: p(n2,n3,n8) ->
% 0.72/0.92 10931:1:0:[10540.0,7017.0]:: p(n4,n6,n9) ->
% 0.72/0.92 10930:1:0:[10540.0,7011.1]:: p(n4,n6,n5) ->
% 0.72/0.92 10929:1:0:[10540.0,7002.1]:: p(n4,n6,n3) ->
% 0.72/0.92 10774:1:0:[10545.0,3732.1]:: p(n3,n3,n6) ->
% 0.72/0.92 10775:1:0:[10550.0,3736.1]:: p(n3,n3,n1) ->
% 0.72/0.92 10928:1:0:[10539.0,6948.0]:: p(n4,n4,n9) ->
% 0.72/0.92 10927:1:0:[10539.0,6941.1]:: p(n4,n4,n5) ->
% 0.72/0.92 10926:1:0:[10539.0,6919.1]:: p(n4,n4,n1) ->
% 0.72/0.93 10776:1:0:[10553.0,3752.1]:: p(n3,n3,n8) ->
% 0.72/0.93 10925:1:0:[10538.0,6828.0]:: p(n4,n1,n7) ->
% 0.72/0.93 10924:1:0:[10538.0,6826.0]:: p(n4,n1,n5) ->
% 0.72/0.93 10923:1:0:[10538.0,6807.1]:: p(n4,n1,n1) ->
% 0.72/0.93 10922:1:0:[10537.0,6793.0]:: p(n3,n9,n8) ->
% 0.72/0.93 10921:1:0:[10537.0,6791.0]:: p(n3,n9,n6) ->
% 0.72/0.93 10920:1:0:[10537.0,6790.0]:: p(n3,n9,n5) ->
% 0.72/0.93 10919:1:0:[10537.0,6784.1]:: p(n3,n9,n3) ->
% 0.72/0.93 10918:1:0:[10537.0,6771.1]:: p(n3,n9,n1) ->
% 0.72/0.93 10777:1:0:[10550.0,3781.1]:: p(n4,n3,n1) ->
% 0.72/0.93 10778:1:0:[10545.0,3813.1]:: p(n5,n3,n6) ->
% 0.72/0.93 10779:1:0:[10550.0,3817.1]:: p(n5,n3,n1) ->
% 0.72/0.93 10780:1:0:[10553.0,3833.1]:: p(n5,n3,n8) ->
% 0.72/0.93 10781:1:0:[10545.0,3840.1]:: p(n6,n3,n6) ->
% 0.72/0.93 10782:1:0:[10553.0,3860.1]:: p(n6,n3,n8) ->
% 0.72/0.93 10783:1:0:[10545.0,3867.0]:: p(n8,n3,n6) ->
% 0.72/0.93 10784:1:0:[10545.0,3876.0]:: p(n9,n3,n6) ->
% 0.72/0.93 10785:1:0:[10553.0,3878.1]:: p(n7,n3,n8) ->
% 0.72/0.93 10786:1:0:[10550.0,3880.0]:: p(n9,n3,n1) ->
% 0.72/0.93 10787:1:0:[10553.0,3887.1]:: p(n8,n3,n8) ->
% 0.72/0.93 10788:1:0:[10531.0,3891.0]:: p(n2,n4,n3) ->
% 0.72/0.93 10789:1:0:[10531.0,3900.0]:: p(n3,n4,n3) ->
% 0.72/0.93 10790:1:0:[10531.0,3909.0]:: p(n4,n4,n3) ->
% 0.72/0.93 10791:1:0:[10539.0,3914.1]:: p(n1,n4,n8) ->
% 0.72/0.93 10792:1:0:[10531.0,3918.0]:: p(n5,n4,n3) ->
% 0.72/0.93 10793:1:0:[10542.0,3919.1]:: p(n1,n4,n4) ->
% 0.72/0.93 10794:1:0:[10531.0,3927.0]:: p(n6,n4,n3) ->
% 0.72/0.93 10917:1:0:[10536.0,6516.1]:: p(n3,n1,n8) ->
% 0.72/0.93 10916:1:0:[10536.0,6515.1]:: p(n3,n1,n7) ->
% 0.72/0.93 10915:1:0:[10536.0,6513.1]:: p(n3,n1,n6) ->
% 0.72/0.93 10795:1:0:[10531.0,3936.0]:: p(n7,n4,n3) ->
% 0.72/0.93 10796:1:0:[10546.0,3940.1]:: p(n1,n4,n7) ->
% 0.72/0.93 10914:1:0:[10536.0,6510.1]:: p(n3,n1,n5) ->
% 0.72/0.93 10913:1:0:[10536.0,6495.1]:: p(n3,n1,n2) ->
% 0.72/0.93 10912:1:0:[10536.0,6488.1]:: p(n3,n1,n1) ->
% 0.72/0.93 10911:1:0:[10535.0,6440.0]:: p(n2,n8,n8) ->
% 0.72/0.93 10797:1:0:[10539.0,3977.1]:: p(n2,n4,n8) ->
% 0.72/0.93 10910:1:0:[10535.0,6435.1]:: p(n2,n8,n5) ->
% 0.72/0.93 10909:1:0:[10535.0,6431.1]:: p(n2,n8,n4) ->
% 0.72/0.93 10798:1:0:[10542.0,3982.1]:: p(n2,n4,n4) ->
% 0.72/0.93 10908:1:0:[10535.0,6426.1]:: p(n2,n8,n3) ->
% 0.72/0.93 10907:1:0:[10535.0,6420.1]:: p(n2,n8,n2) ->
% 0.72/0.93 10906:1:0:[10535.0,6413.1]:: p(n2,n8,n1) ->
% 0.72/0.93 10905:1:0:[10534.0,6336.1]:: p(n2,n5,n8) ->
% 0.72/0.93 10904:1:0:[10534.0,6330.1]:: p(n2,n5,n5) ->
% 0.72/0.93 10903:1:0:[10534.0,6326.1]:: p(n2,n5,n4) ->
% 0.72/0.93 10902:1:0:[10534.0,6321.1]:: p(n2,n5,n3) ->
% 0.72/0.93 10901:1:0:[10534.0,6315.1]:: p(n2,n5,n2) ->
% 0.72/0.93 10799:1:0:[10539.0,4031.1]:: p(n3,n4,n8) ->
% 0.72/0.93 10900:1:0:[10533.0,6226.0]:: p(n2,n2,n8) ->
% 0.72/0.93 10899:1:0:[10533.0,6220.1]:: p(n2,n2,n5) ->
% 0.72/0.93 10898:1:0:[10533.0,6216.1]:: p(n2,n2,n4) ->
% 0.72/0.93 10800:1:0:[10546.0,4057.1]:: p(n3,n4,n7) ->
% 0.72/0.93 10897:1:0:[10533.0,6211.1]:: p(n2,n2,n3) ->
% 0.72/0.93 10896:1:0:[10533.0,6205.1]:: p(n2,n2,n2) ->
% 0.72/0.93 10895:1:0:[10533.0,6198.1]:: p(n2,n2,n1) ->
% 0.72/0.93 10801:1:0:[10539.0,4085.0]:: p(n5,n4,n8) ->
% 0.72/0.93 10802:1:0:[10539.0,4094.0]:: p(n6,n4,n8) ->
% 0.72/0.93 10803:1:0:[10546.0,4102.1]:: p(n4,n4,n7) ->
% 0.72/0.93 10804:1:0:[10539.0,4103.0]:: p(n7,n4,n8) ->
% 0.72/0.93 10805:1:0:[10539.0,4112.0]:: p(n8,n4,n8) ->
% 0.72/0.93 10806:1:0:[10542.0,4126.0]:: p(n6,n4,n4) ->
% 0.72/0.93 10807:1:0:[10542.0,4135.0]:: p(n7,n4,n4) ->
% 0.72/0.93 10808:1:0:[10542.0,4144.0]:: p(n8,n4,n4) ->
% 0.72/0.93 10894:1:0:[10532.0,6020.0]:: p(n1,n6,n9) ->
% 0.72/0.93 10893:1:0:[10532.0,6019.0]:: p(n1,n6,n8) ->
% 0.72/0.93 10809:1:0:[10542.0,4153.0]:: p(n9,n4,n4) ->
% 0.72/0.93 10892:1:0:[10532.0,6016.0]:: p(n1,n6,n5) ->
% 0.72/0.93 10891:1:0:[10532.0,6015.0]:: p(n1,n6,n4) ->
% 0.72/0.93 10810:1:0:[10546.0,4165.1]:: p(n6,n4,n7) ->
% 0.72/0.93 10890:1:0:[10531.0,5961.0]:: p(n1,n4,n9) ->
% 0.72/0.93 10889:1:0:[10531.0,5958.0]:: p(n1,n4,n6) ->
% 0.72/0.93 10888:1:0:[10531.0,5957.0]:: p(n1,n4,n5) ->
% 0.72/0.93 10887:1:0:[10531.0,5949.1]:: p(n1,n4,n2) ->
% 0.72/0.93 10811:1:0:[10546.0,4201.0]:: p(n9,n4,n7) ->
% 0.72/0.93 10812:1:0:[10534.0,4221.1]:: p(n1,n5,n9) ->
% 0.72/0.93 10886:1:0:[10552.0,5830.0]:: p(n9,n9,n7) ->
% 0.72/0.93 10885:1:0:[10552.0,5794.1]:: p(n6,n9,n7) ->
% 0.72/0.93 10813:1:0:[10534.0,4302.0]:: p(n4,n5,n9) ->
% 0.72/0.93 10814:1:0:[10534.0,4311.0]:: p(n5,n5,n9) ->
% 0.72/0.93 10815:1:0:[10544.0,4312.1]:: p(n2,n5,n1) ->
% 0.72/0.93 10816:1:0:[10534.0,4320.0]:: p(n6,n5,n9) ->
% 0.72/0.93 10884:1:0:[10541.0,5735.0]:: p(n9,n9,n2) ->
% 0.72/0.93 10817:1:0:[10534.0,4329.0]:: p(n7,n5,n9) ->
% 0.72/0.93 10883:1:0:[10552.0,5731.1]:: p(n4,n9,n7) ->
% 0.72/0.93 10882:1:0:[10541.0,5726.0]:: p(n8,n9,n2) ->
% 0.72/0.93 10818:1:0:[10534.0,4347.0]:: p(n9,n5,n9) ->
% 0.72/0.93 10881:1:0:[10541.0,5708.0]:: p(n6,n9,n2) ->
% 0.72/0.93 10880:1:0:[10541.0,5699.0]:: p(n5,n9,n2) ->
% 0.72/0.93 10819:1:0:[10544.0,4366.1]:: p(n3,n5,n1) ->
% 0.72/0.93 10879:1:0:[10537.0,5692.0]:: p(n9,n9,n4) ->
% 0.72/0.93 10878:1:0:[10552.0,5686.1]:: p(n3,n9,n7) ->
% 0.72/0.93 10877:1:0:[10537.0,5683.0]:: p(n8,n9,n4) ->
% 0.72/0.93 10876:1:0:[10537.0,5674.0]:: p(n7,n9,n4) ->
% 0.72/0.93 10875:1:0:[10537.0,5665.0]:: p(n6,n9,n4) ->
% 0.72/0.93 10820:1:0:[10544.0,4411.1]:: p(n4,n5,n1) ->
% 0.72/0.93 10874:1:0:[10541.0,5645.1]:: p(n3,n9,n2) ->
% 0.72/0.93 10873:1:0:[10541.0,5591.1]:: p(n2,n9,n2) ->
% 0.72/0.93 10872:1:0:[10537.0,5584.1]:: p(n2,n9,n4) ->
% 0.72/0.93 10821:1:0:[10544.0,4447.1]:: p(n5,n5,n1) ->
% 0.72/0.93 10871:1:0:[10552.0,5569.1]:: p(n1,n9,n7) ->
% 0.72/0.93 10870:1:0:[10541.0,5528.1]:: p(n1,n9,n2) ->
% 0.72/0.93 10869:1:0:[10537.0,5521.1]:: p(n1,n9,n4) ->
% 0.72/0.93 10822:1:0:[10544.0,4501.0]:: p(n9,n5,n1) ->
% 0.72/0.93 10823:1:0:[10532.0,4537.0]:: p(n2,n6,n1) ->
% 0.72/0.93 10824:1:0:[10532.0,4546.0]:: p(n3,n6,n1) ->
% 0.72/0.93 10825:1:0:[10532.0,4555.0]:: p(n4,n6,n1) ->
% 0.72/0.93 10826:1:0:[10540.0,4560.1]:: p(n1,n6,n6) ->
% 0.72/0.93 10827:1:0:[10532.0,4564.0]:: p(n5,n6,n1) ->
% 0.72/0.93 10828:1:0:[10543.0,4570.1]:: p(n1,n6,n7) ->
% 0.72/0.93 10829:1:0:[10547.0,4583.1]:: p(n1,n6,n2) ->
% 0.72/0.93 10830:1:0:[10532.0,4600.0]:: p(n9,n6,n1) ->
% 0.72/0.93 10831:1:0:[10547.0,4646.1]:: p(n2,n6,n2) ->
% 0.72/0.93 10868:1:0:[10535.0,5316.0]:: p(n9,n8,n6) ->
% 0.72/0.93 10867:1:0:[10535.0,5307.0]:: p(n8,n8,n6) ->
% 0.72/0.93 10832:1:0:[10540.0,4677.1]:: p(n3,n6,n6) ->
% 0.72/0.93 10866:1:0:[10535.0,5289.0]:: p(n6,n8,n6) ->
% 0.72/0.93 10833:1:0:[10543.0,4687.1]:: p(n3,n6,n7) ->
% 0.72/0.93 10865:1:0:[10535.0,5280.0]:: p(n5,n8,n6) ->
% 0.72/0.93 10834:1:0:[10547.0,4700.1]:: p(n3,n6,n2) ->
% 0.72/0.93 10864:1:0:[10535.0,5262.0]:: p(n3,n8,n6) ->
% 0.72/0.93 10835:1:0:[10540.0,4731.0]:: p(n5,n6,n6) ->
% 0.72/0.93 10836:1:0:[10543.0,4732.1]:: p(n4,n6,n7) ->
% 0.72/0.93 10837:1:0:[10540.0,4740.0]:: p(n6,n6,n6) ->
% 0.72/0.93 10838:1:0:[10540.0,4758.0]:: p(n8,n6,n6) ->
% 0.72/0.93 10863:1:0:[10535.0,5190.1]:: p(n1,n8,n6) ->
% 0.72/0.93 10839:1:0:[10540.0,4767.0]:: p(n9,n6,n6) ->
% 0.72/0.93 10862:1:0:[10551.0,5184.0]:: p(n9,n7,n9) ->
% 0.72/0.93 10840:1:0:[10543.0,4777.0]:: p(n6,n6,n7) ->
% 0.72/0.93 10841:1:0:[10547.0,4781.1]:: p(n5,n6,n2) ->
% 0.72/0.93 10861:1:0:[10554.0,5169.1]:: p(n7,n7,n3) ->
% 0.72/0.93 10860:1:0:[10548.0,5167.0]:: p(n9,n7,n1) ->
% 0.72/0.93 10859:1:0:[10551.0,5166.1]:: p(n7,n7,n9) ->
% 0.72/0.93 10858:1:0:[10554.0,5151.1]:: p(n6,n7,n3) ->
% 0.72/0.93 10857:1:0:[10551.0,5148.1]:: p(n6,n7,n9) ->
% 0.72/0.93 10842:1:0:[10543.0,4804.0]:: p(n9,n6,n7) ->
% 0.72/0.93 10843:1:0:[10547.0,4808.1]:: p(n6,n6,n2) ->
% 0.72/0.93 10856:1:0:[10554.0,5124.1]:: p(n5,n7,n3) ->
% 0.72/0.93 10855:1:0:[10551.0,5121.1]:: p(n5,n7,n9) ->
% 0.72/0.93 10844:1:0:[10547.0,4835.0]:: p(n8,n6,n2) ->
% 0.72/0.93 10845:1:0:[10547.0,4844.0]:: p(n9,n6,n2) ->
% 0.72/0.93 10854:1:0:[10548.0,5104.1]:: p(n5,n7,n1) ->
% 0.72/0.93 10853:1:0:[10554.0,5088.1]:: p(n4,n7,n3) ->
% 0.72/0.93 10852:1:0:[10551.0,5085.1]:: p(n4,n7,n9) ->
% 0.72/0.93 10851:1:0:[10548.0,5068.1]:: p(n4,n7,n1) ->
% 0.72/0.93 10850:1:0:[10554.0,5043.1]:: p(n3,n7,n3) ->
% 0.72/0.93 10849:1:0:[10548.0,5023.1]:: p(n3,n7,n1) ->
% 0.72/0.93 10846:1:0:[10551.0,4923.1]:: p(n1,n7,n9) ->
% 0.72/0.93 10848:1:0:[10554.0,4989.1]:: p(n2,n7,n3) ->
% 0.72/0.93 10847:1:0:[10548.0,4969.1]:: p(n2,n7,n1) ->
% 0.72/0.93
% 0.72/0.93 Most General Atoms: p(n1,n1,n1) p(n1,n2,n1) p(n1,n1,n2) p(n1,n2,n2) p(n1,n1,n3) p(n1,n2,n3) p(n1,n1,n4) p(n1,n2,n4) p(n1,n1,n5) p(n1,n2,n5) p(n1,n1,n6) p(n1,n2,n6) p(n1,n1,n7) p(n1,n2,n7) p(n1,n1,n8) p(n1,n2,n8) p(n1,n1,n9) p(n1,n2,n9) p(n1,n3,n1) p(n1,n3,n2) p(n1,n3,n3) p(n1,n3,n4) p(n1,n3,n5) p(n1,n3,n6) p(n1,n3,n7) p(n1,n3,n8) p(n1,n3,n9) p(n1,n4,n1) p(n1,n4,n2) p(n1,n4,n4) p(n1,n4,n5) p(n1,n4,n6) p(n1,n4,n7) p(n1,n4,n8) p(n1,n4,n9) p(n1,n5,n1) p(n1,n5,n2) p(n9,n7,n3) p(n1,n5,n4) p(n1,n5,n5) p(n1,n5,n6) p(n1,n5,n7) p(n1,n5,n8) p(n1,n5,n9) p(n1,n6,n2) p(n9,n3,n8) p(n1,n6,n4) p(n1,n6,n5) p(n1,n6,n6) p(n1,n6,n7) p(n1,n6,n8) p(n1,n6,n9) p(n8,n9,n7) p(n1,n7,n2) p(n8,n7,n9) p(n1,n7,n4) p(n1,n7,n5) p(n1,n7,n6) p(n1,n7,n7) p(n1,n7,n8) p(n1,n7,n9) p(n8,n3,n1) p(n1,n8,n2) p(n8,n1,n3) p(n1,n8,n4) p(n1,n8,n5) p(n1,n8,n6) p(n1,n8,n7) p(n1,n8,n8) p(n1,n8,n9) p(n7,n7,n1) p(n1,n9,n2) p(n7,n6,n2) p(n1,n9,n4) p(n1,n9,n5) p(n1,n9,n6) p(n1,n9,n7) p(n1,n9,n8) p(n1,n9,n9) p(n7,n4,n7) p(n7,n3,n6) p(n6,n5,n1) p(n5,n6,n7) p(n5,n4,n4) p(n4,n9,n2) p(n4,n6,n6) p(n4,n4,n8) p(n4,n1,n4) p(n3,n9,n4) p(n3,n1,n9) p(n2,n8,n6) p(n2,n5,n9) p(n2,n2,n7) p(n1,n6,n1) p(n1,n4,n3) p(n1,n5,n3) p(n1,n6,n3) p(n7,n8,n8) p(n7,n9,n8) p(n8,n8,n8) p(n1,n7,n3) p(n9,n9,n6) p(n1,n8,n3) p(n7,n8,n5) p(n7,n9,n5) p(n8,n8,n5) p(n9,n8,n5) p(n9,n9,n5) p(n1,n9,n3) p(n7,n8,n4) p(n8,n8,n4) p(n9,n8,n4) p(n8,n8,n2) p(n9,n8,n2) p(n9,n4,n9) p(n9,n6,n9) p(n7,n5,n8) p(n8,n5,n8) p(n8,n6,n8) p(n7,n5,n5) p(n8,n4,n5) p(n8,n5,n5) p(n8,n6,n5) p(n9,n4,n5) p(n9,n5,n5) p(n9,n6,n5) p(n7,n5,n4) p(n8,n5,n4) p(n8,n6,n4) p(n9,n5,n4) p(n9,n6,n4) p(n7,n2,n4) p(n8,n2,n4) p(n9,n2,n4) p(n1,n7,n1) p(n8,n2,n2) p(n9,n1,n2) p(n9,n2,n2) p(n1,n8,n1) p(n4,n8,n9) p(n5,n8,n9) p(n5,n9,n9) p(n6,n8,n9) p(n6,n9,n9) p(n1,n9,n1) p(n5,n7,n8) p(n5,n8,n8) p(n5,n9,n8) p(n6,n7,n8) p(n6,n8,n8) p(n6,n9,n8) p(n4,n7,n7) p(n4,n8,n7) p(n6,n7,n7) p(n6,n8,n7) p(n4,n7,n5) p(n4,n8,n5) p(n5,n7,n5) p(n5,n8,n5) p(n5,n9,n5) p(n6,n7,n5) p(n6,n8,n5) p(n6,n9,n5) p(n4,n8,n3) p(n5,n8,n3) p(n5,n9,n3) p(n6,n8,n3) p(n6,n9,n3) p(n4,n8,n1) p(n5,n8,n1) p(n5,n9,n1) p(n6,n4,n9) p(n6,n6,n9) p(n4,n5,n5) p(n5,n5,n5) p(n6,n4,n5) p(n6,n6,n5) p(n2,n1,n1) p(n2,n2,n1) p(n2,n1,n2) p(n2,n2,n2) p(n2,n1,n3) p(n2,n2,n3) p(n2,n1,n4) p(n2,n2,n4) p(n2,n1,n5) p(n2,n2,n5) p(n2,n1,n6) p(n2,n2,n6) p(n2,n1,n7) p(n2,n1,n8) p(n2,n2,n8) p(n2,n1,n9) p(n2,n2,n9) p(n2,n3,n1) p(n2,n3,n2) p(n2,n3,n3) p(n2,n3,n4) p(n2,n3,n5) p(n2,n3,n6) p(n5,n5,n2) p(n6,n4,n2) p(n2,n3,n8) p(n2,n3,n9) p(n2,n4,n1) p(n2,n4,n2) p(n2,n4,n3) p(n2,n4,n4) p(n2,n4,n5) p(n2,n4,n6) p(n5,n1,n8) p(n5,n2,n8) p(n6,n1,n8) p(n6,n2,n8) p(n2,n4,n8) p(n2,n4,n9) p(n2,n5,n1) p(n2,n5,n2) p(n2,n5,n3) p(n2,n5,n4) p(n2,n5,n5) p(n2,n5,n6) p(n5,n1,n6) p(n5,n2,n6) p(n6,n1,n6) p(n6,n2,n6) p(n2,n5,n8) p(n2,n6,n1) p(n2,n6,n2) p(n2,n6,n3) p(n2,n6,n4) p(n2,n6,n5) p(n2,n6,n6) p(n4,n2,n5) p(n4,n3,n5) p(n5,n1,n5) p(n5,n2,n5) p(n5,n3,n5) p(n6,n1,n5) p(n6,n2,n5) p(n6,n3,n5) p(n2,n6,n8) p(n4,n2,n3) p(n4,n3,n3) p(n5,n2,n3) p(n5,n3,n3) p(n6,n2,n3) p(n6,n3,n3) p(n2,n7,n1) p(n2,n7,n2) p(n2,n7,n3) p(n2,n7,n4) p(n2,n7,n5) p(n2,n7,n6) p(n5,n1,n2) p(n5,n2,n2) p(n5,n3,n2) p(n6,n1,n2) p(n6,n2,n2) p(n6,n3,n2) p(n2,n7,n8) p(n4,n2,n1) p(n5,n1,n1) p(n5,n2,n1) p(n2,n8,n1) p(n2,n8,n2) p(n2,n8,n3) p(n2,n8,n4) p(n2,n8,n5) p(n2,n9,n8) p(n3,n7,n8) p(n3,n8,n8) p(n2,n8,n8) p(n3,n7,n7) p(n3,n8,n7) p(n2,n9,n1) p(n2,n9,n2) p(n2,n9,n3) p(n2,n9,n4) p(n2,n9,n5) p(n3,n7,n5) p(n3,n8,n5) p(n3,n8,n3) p(n3,n8,n1) p(n2,n3,n7) p(n2,n4,n7) p(n2,n5,n7) p(n2,n6,n7) p(n3,n5,n8) p(n3,n6,n8) p(n2,n7,n7) p(n3,n4,n6) p(n3,n5,n6) p(n2,n8,n7) p(n3,n4,n5) p(n3,n5,n5) p(n3,n6,n5) p(n2,n9,n7) p(n3,n4,n2) p(n3,n5,n2) p(n3,n2,n8) p(n3,n2,n6) p(n3,n2,n5) p(n3,n3,n5) p(n3,n2,n3) p(n3,n3,n3) p(n3,n2,n2) p(n3,n3,n2) p(n3,n2,n1) p(n9,n5,n6) p(n9,n2,n5) p(n9,n2,n9) p(n8,n5,n6) p(n8,n4,n6) p(n8,n2,n5) p(n7,n1,n5) p(n6,n9,n6) p(n6,n8,n4) p(n2,n6,n9) p(n6,n3,n7) p(n6,n3,n9) p(n2,n7,n9) p(n6,n2,n9) p(n2,n8,n9) p(n6,n1,n7) p(n5,n9,n6) p(n2,n9,n9) p(n5,n7,n6) p(n5,n5,n3) p(n5,n3,n9) p(n5,n2,n9) p(n4,n5,n3) p(n4,n3,n7) p(n4,n3,n9) p(n4,n2,n9) p(n3,n8,n2) p(n2,n9,n6) p(n3,n7,n2) p(n3,n1,n1) p(n3,n1,n2) p(n3,n1,n3) p(n3,n1,n4) p(n3,n2,n4) p(n3,n1,n5) p(n3,n1,n6) p(n3,n1,n7) p(n3,n2,n7) p(n3,n1,n8) p(n3,n2,n9) p(n3,n3,n1) p(n3,n3,n4) p(n3,n3,n6) p(n3,n3,n7) p(n3,n3,n8) p(n3,n3,n9) p(n3,n4,n1) p(n3,n4,n3) p(n3,n4,n4) p(n3,n4,n7) p(n3,n4,n8) p(n3,n4,n9) p(n3,n5,n1) p(n3,n5,n3) p(n3,n5,n4) p(n3,n5,n7) p(n3,n5,n9) p(n3,n6,n1) p(n3,n6,n2) p(n3,n6,n3) p(n3,n6,n4) p(n3,n6,n6) p(n3,n6,n7) p(n3,n6,n9) p(n3,n7,n1) p(n3,n7,n3) p(n3,n7,n4) p(n3,n7,n6) p(n3,n7,n9) p(n3,n8,n4) p(n3,n8,n6) p(n3,n8,n9) p(n3,n9,n1) p(n3,n9,n2) p(n3,n9,n3) p(n3,n9,n5) p(n3,n9,n6) p(n3,n9,n7) p(n3,n9,n8) p(n3,n9,n9) p(n4,n1,n1) p(n4,n1,n2) p(n4,n2,n2) p(n4,n1,n3) p(n4,n2,n4) p(n4,n1,n5) p(n4,n1,n6) p(n4,n2,n6) p(n4,n1,n7) p(n4,n2,n7) p(n4,n1,n8) p(n4,n2,n8) p(n4,n1,n9) p(n4,n3,n1) p(n4,n3,n2) p(n4,n3,n4) p(n4,n3,n6) p(n4,n3,n8) p(n4,n4,n1) p(n4,n4,n2) p(n4,n4,n3) p(n4,n4,n4) p(n4,n4,n5) p(n4,n4,n6) p(n4,n4,n7) p(n4,n4,n9) p(n4,n5,n1) p(n4,n5,n2) p(n4,n5,n4) p(n4,n5,n6) p(n4,n5,n7) p(n4,n5,n9) p(n4,n6,n1) p(n4,n6,n2) p(n4,n6,n3) p(n4,n6,n4) p(n4,n6,n5) p(n4,n6,n7) p(n4,n6,n9) p(n4,n7,n1) p(n4,n7,n2) p(n4,n7,n3) p(n4,n7,n4) p(n4,n7,n9) p(n4,n8,n2) p(n4,n8,n4) p(n6,n7,n6) p(n4,n9,n1) p(n4,n9,n3) p(n4,n9,n4) p(n4,n9,n5) p(n4,n9,n7) p(n6,n7,n4) p(n4,n9,n9) p(n6,n6,n3) p(n9,n4,n6) p(n7,n2,n5) p(n4,n5,n8) p(n4,n6,n8) p(n9,n1,n5) p(n4,n7,n8) p(n4,n8,n8) p(n9,n1,n7) p(n4,n9,n8) p(n9,n4,n1) p(n7,n2,n9) p(n4,n7,n6) p(n7,n5,n3) p(n4,n8,n6) p(n4,n9,n6) p(n5,n1,n3) p(n5,n1,n4) p(n5,n2,n4) p(n5,n1,n7) p(n5,n2,n7) p(n5,n1,n9) p(n5,n3,n1) p(n5,n3,n4) p(n5,n3,n6) p(n5,n3,n7) p(n5,n3,n8) p(n5,n4,n1) p(n5,n4,n2) p(n5,n4,n3) p(n5,n4,n5) p(n5,n4,n6) p(n5,n4,n7) p(n5,n4,n8) p(n5,n4,n9) p(n5,n5,n1) p(n5,n5,n6) p(n5,n5,n7) p(n5,n5,n8) p(n5,n5,n9) p(n5,n6,n1) p(n5,n6,n2) p(n5,n6,n3) p(n5,n6,n5) p(n5,n6,n6) p(n5,n6,n8) p(n5,n6,n9) p(n5,n7,n1) p(n5,n7,n2) p(n5,n7,n3) p(n5,n7,n9) p(n5,n8,n2) p(n5,n8,n6) p(n5,n9,n2) p(n5,n5,n4) p(n5,n6,n4) p(n5,n7,n4) p(n5,n8,n4) p(n5,n9,n4) p(n9,n8,n7) p(n9,n9,n9) p(n9,n8,n9) p(n7,n9,n3) p(n5,n7,n7) p(n5,n8,n7) p(n7,n9,n9) p(n5,n9,n7) p(n7,n8,n3) p(n7,n8,n9) p(n9,n9,n1) p(n9,n8,n1) p(n6,n1,n1) p(n6,n2,n1) p(n6,n1,n3) p(n6,n1,n4) p(n6,n2,n4) p(n6,n2,n7) p(n6,n1,n9) p(n6,n3,n1) p(n6,n3,n4) p(n6,n3,n6) p(n6,n3,n8) p(n6,n4,n1) p(n6,n4,n3) p(n6,n4,n4) p(n6,n4,n6) p(n6,n4,n7) p(n6,n4,n8) p(n6,n5,n2) p(n6,n5,n3) p(n6,n5,n4) p(n6,n5,n5) p(n6,n5,n6) p(n6,n5,n7) p(n6,n5,n8) p(n6,n5,n9) p(n6,n6,n2) p(n6,n6,n4) p(n6,n6,n6) p(n6,n6,n7) p(n6,n6,n8) p(n6,n7,n2) p(n6,n7,n3) p(n6,n7,n9) p(n6,n8,n2) p(n6,n8,n6) p(n6,n9,n2) p(n6,n9,n4) p(n6,n9,n7) p(n9,n5,n2) p(n9,n4,n2) p(n8,n5,n2) p(n8,n4,n2) p(n6,n6,n1) p(n6,n7,n1) p(n6,n8,n1) p(n6,n9,n1) p(n9,n5,n7) p(n9,n2,n1) p(n7,n1,n1) p(n7,n2,n1) p(n7,n1,n2) p(n7,n2,n2) p(n7,n1,n3) p(n7,n2,n3) p(n7,n1,n4) p(n7,n1,n6) p(n7,n2,n6) p(n7,n1,n7) p(n7,n2,n7) p(n7,n1,n8) p(n7,n2,n8) p(n7,n1,n9) p(n7,n3,n1) p(n7,n3,n2) p(n7,n3,n3) p(n7,n3,n4) p(n7,n3,n5) p(n7,n3,n7) p(n7,n3,n8) p(n7,n3,n9) p(n7,n4,n1) p(n7,n4,n2) p(n7,n4,n3) p(n7,n4,n4) p(n7,n4,n5) p(n9,n1,n1) p(n7,n4,n8) p(n7,n4,n9) p(n7,n5,n1) p(n7,n5,n2) p(n8,n2,n8) p(n7,n5,n9) p(n7,n6,n1) p(n7,n6,n3) p(n7,n6,n4) p(n7,n6,n5) p(n9,n2,n6) p(n7,n6,n8) p(n7,n6,n9) p(n9,n1,n6) p(n7,n7,n3) p(n7,n7,n4) p(n7,n7,n5) p(n8,n2,n6) p(n7,n7,n8) p(n7,n7,n9) p(n7,n9,n4) p(n7,n4,n6) p(n7,n5,n6) p(n7,n6,n6) p(n7,n7,n6) p(n7,n8,n6) p(n7,n9,n6) p(n7,n5,n7) p(n7,n6,n7) p(n7,n7,n7) p(n7,n8,n7) p(n7,n9,n7) p(n7,n7,n2) p(n7,n8,n2) p(n7,n9,n2) p(n7,n8,n1) p(n7,n9,n1) p(n8,n1,n1) p(n8,n2,n1) p(n8,n1,n2) p(n8,n2,n3) p(n8,n1,n4) p(n8,n1,n5) p(n8,n1,n6) p(n8,n1,n7) p(n8,n2,n7) p(n8,n1,n8) p(n8,n1,n9) p(n8,n2,n9) p(n8,n3,n2) p(n8,n3,n3) p(n8,n3,n4) p(n8,n3,n5) p(n8,n3,n6) p(n8,n3,n7) p(n8,n3,n8) p(n8,n3,n9) p(n8,n4,n3) p(n8,n4,n4) p(n8,n4,n7) p(n8,n4,n8) p(n8,n4,n9) p(n8,n5,n3) p(n8,n5,n7) p(n8,n5,n9) p(n8,n6,n2) p(n8,n6,n3) p(n8,n6,n6) p(n8,n6,n7) p(n8,n6,n9) p(n8,n7,n2) p(n8,n7,n3) p(n8,n7,n4) p(n8,n7,n5) p(n8,n7,n6) p(n8,n7,n7) p(n8,n7,n8) p(n8,n8,n3) p(n8,n8,n6) p(n8,n8,n7) p(n8,n9,n2) p(n8,n9,n3) p(n8,n9,n4) p(n8,n9,n5) p(n8,n9,n6) p(n8,n9,n8) p(n8,n4,n1) p(n8,n5,n1) p(n8,n6,n1) p(n8,n7,n1) p(n8,n8,n1) p(n8,n9,n1) p(n8,n8,n9) p(n8,n9,n9) p(n9,n1,n3) p(n9,n2,n3) p(n9,n1,n4) p(n9,n2,n7) p(n9,n1,n8) p(n9,n2,n8) p(n9,n1,n9) p(n9,n3,n1) p(n9,n3,n2) p(n9,n3,n3) p(n9,n3,n4) p(n9,n3,n5) p(n9,n3,n6) p(n9,n3,n7) p(n9,n3,n9) p(n9,n4,n3) p(n9,n4,n4) p(n9,n4,n7) p(n9,n5,n1) p(n9,n5,n3) p(n9,n5,n9) p(n9,n6,n1) p(n9,n6,n2) p(n9,n6,n3) p(n9,n6,n6) p(n9,n6,n7) p(n9,n7,n1) p(n9,n7,n2) p(n9,n7,n4) p(n9,n7,n5) p(n9,n7,n6) p(n9,n7,n7) p(n9,n7,n9) p(n9,n8,n6) p(n9,n9,n2) p(n9,n9,n4) p(n9,n9,n7) p(n9,n4,n8) p(n9,n5,n8) p(n9,n6,n8) p(n9,n7,n8) p(n9,n8,n8) p(n9,n9,n8) p(n9,n8,n3) p(n9,n9,n3)
% 0.72/0.93
% 0.72/0.93 === Starting SPASS-SCL-FOL A Little Less Naive, considering 729 atoms initially, heuristics mode: lmodel_grow ===
% 0.72/0.93
% 0.72/0.93 === Conflict found: 11731:2:0:[10851.0,10402.0,10641.0,11725.1,10853.0,11726.2,10618.1,11727.3,10637.1,11728.5,10631.1,11729.7,10852.0,11730.8]:: -> p(n4,n7,n5),p(n4,n7,n7) {}
% 0.72/0.93 === Backtracking. Learning clause 12074:1:0:[11731.1,9590.1,1141.2,11789.2,1911.2,11416.1,5786.1,1854.2,11988.1,11810.2,7537.2,7653.2,11483.1,2012.2,11797.1,5802.1,12067.1]:: p(n6,n3,n2) ->
% 0.72/0.93 === Backtracking. Learning clause 12075:4:0:[8687.1,12049.2,12059.4,8374.2,8362.1]:: p(n8,n8,n4) -> p(n7,n8,n5),p(n7,n9,n5),p(n9,n9,n5)
% 0.72/0.93 === Conflict found: 11912:6:0:[10888.1,10463.0,10892.1,11910.2,10904.0,11911.4]:: -> p(n1,n5,n5),p(n2,n4,n5),p(n2,n6,n5),p(n3,n4,n5),p(n3,n5,n5),p(n3,n6,n5) {}
% 0.72/0.93 === Backtracking. Learning clause 12081:15:0:[4235.0,12076.5,9719.0,12077.7,1067.0,12078.8,1121.0,12079.9,9390.1,12080.14,11912.6,6689.1,6615.1,11923.4,6275.2,6358.2,11428.1,6361.2,98.2,11897.2,6600.1,6658.2,6536.2,11909.2,4279.1,2951.1,11132.2,6655.1,3014.1,11470.2,11884.2,4352.1,11195.1,7193.2,11959.4,11850.1,3657.1,3399.1,259.1,11772.4,11633.3,7376.2,5426.1,1745.1,4442.2,3530.1,7217.2,5228.1,3711.1]:: p(n5,n7,n6),p(n4,n5,n5),p(n9,n2,n2),p(n6,n8,n8),p(n5,n3,n3) -> p(n6,n4,n2),p(n5,n1,n5),p(n6,n1,n5),p(n6,n3,n5),p(n9,n5,n6),p(n6,n2,n5),p(n6,n2,n9),p(n1,n8,n2),p(n1,n8,n5),p(n1,n8,n9)
% 0.72/0.93 === Conflict found: 11717:4:0:[10777.0,10398.0,10627.0,11713.1,10612.1,11714.3,10626.0,11715.5,10625.0,11716.7]:: -> p(n4,n3,n3),p(n4,n3,n5),p(n4,n3,n7),p(n4,n3,n9) {}
% 0.72/0.93 === Backtracking. Learning clause 12083:10:0:[2951.0,12082.9,11717.4,3762.1,3702.2,11746.4,3659.2,11649.4,3639.1,11682.2,812.1,11704.1,923.2,764.2,806.1,481.1,1442.1,11897.4,3014.1]:: p(n3,n6,n5),p(n2,n6,n4),p(n5,n5,n2),p(n5,n1,n8) -> p(n4,n3,n5),p(n4,n3,n7),p(n5,n3,n3),p(n2,n3,n2),p(n3,n7,n7),p(n1,n2,n8)
% 0.72/0.93
% 0.72/0.93 Linear Model Building succeeded.
% 0.72/0.93 SZS status Satisfiable
% 0.72/0.93
% 0.72/0.93 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.93
% 0.72/0.93 SPASS-SCL-FOL Statistics:
% 0.72/0.93 Number of learned clauses: 4
% 0.72/0.93 Number of propagations: 2037
% 0.72/0.93 Number of decisions: 15
% 0.72/0.93 Number of resolutions: 74
% 0.72/0.93 Number of condensations: 0
% 0.72/0.93 Number of sub resolutions: 1525
% 0.72/0.93 Number of input literals (deduplicated): 729
% 0.72/0.93 Number of grows: 0
% 0.72/0.93 Number of considered ground atoms: 729
% 0.72/0.93
% 0.72/0.93 Needed: 0:00:00.33
% 0.72/0.93
%------------------------------------------------------------------------------