%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PUZ079+2 : TPTP v9.2.1. Bugfixed v5.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n031.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.70s 0.90s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ079+2 : TPTP v9.2.1. Bugfixed v5.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.15/0.33 % Computer : n031.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 13:00:26 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 1.75/0.87 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.75/0.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.75/0.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.75/0.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.75/0.87 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.75/0.87 Execution lmodel_grow ended with status: satisfiable % 1.75/0.87 Used heuristic: lmodel_grow % 1.75/0.87 % 1.75/0.87 Input Clauses: % 1.75/0.89 % 1.75/0.89 Predicates: p % 1.75/0.89 Fol Constants: n1 n2 n3 n4 n5 n6 n7 n8 n9 % 1.75/0.89 Fol Functions: % 1.75/0.89 Problem Properties: % 1.75/0.89 This is a first-order ground problem without equality. % 1.75/0.89 % 1.75/0.89 After reduction: Problem Properties: % 1.75/0.89 This is a first-order ground problem without equality. % 1.75/0.89 % 1.75/0.89 % 1.75/0.89 Reduced Input Clauses: % 1.75/0.89 10559:1:0:[10531.0,1.0]:: p(n1,n2,n1) -> % 1.75/0.89 10560:1:0:[10531.0,10.0]:: p(n1,n3,n1) -> % 1.75/0.89 10561:1:0:[10531.0,19.0]:: p(n1,n4,n1) -> % 1.75/0.89 10562:1:0:[10532.0,24.1]:: p(n1,n1,n6) -> % 1.75/0.89 10563:1:0:[10531.0,28.0]:: p(n1,n5,n1) -> % 1.75/0.89 10564:1:0:[10531.0,37.0]:: p(n1,n6,n1) -> % 1.75/0.89 10565:1:0:[10533.0,40.1]:: p(n1,n1,n4) -> % 1.75/0.89 10566:1:0:[10531.0,46.0]:: p(n1,n7,n1) -> % 1.75/0.89 10567:1:0:[10531.0,55.0]:: p(n1,n8,n1) -> % 1.75/0.89 10568:1:0:[10531.0,64.0]:: p(n1,n9,n1) -> % 1.75/0.89 10569:1:0:[10534.0,72.1]:: p(n1,n1,n9) -> % 1.75/0.89 10570:1:0:[10532.0,87.1]:: p(n1,n2,n6) -> % 1.75/0.89 10571:1:0:[10533.0,103.1]:: p(n1,n2,n4) -> % 1.75/0.89 10572:1:0:[10534.0,135.1]:: p(n1,n2,n9) -> % 1.75/0.89 10573:1:0:[10532.0,141.1]:: p(n1,n3,n6) -> % 1.75/0.89 10574:1:0:[10533.0,157.1]:: p(n1,n3,n4) -> % 1.75/0.89 12113:3:0:[11025.1,10530.0,10920.1,12108.2,10744.1,12109.3,10745.1,12110.4,10746.1,12111.5,10921.1,12112.8]:: -> p(n7,n8,n9),p(n9,n7,n9),p(n9,n8,n9) % 1.75/0.89 12107:5:0:[11024.1,10529.0,10933.1,12104.2,10934.1,12105.5,10936.1,12106.8]:: -> p(n7,n8,n8),p(n8,n7,n8),p(n8,n8,n8),p(n9,n7,n8),p(n9,n8,n8) % 1.75/0.89 12103:5:0:[10722.1,10528.0,10723.1,12100.1,10724.1,12101.2,11045.1,12102.8]:: -> p(n8,n7,n7),p(n8,n8,n7),p(n8,n9,n7),p(n9,n7,n7),p(n9,n8,n7) % 1.75/0.89 12099:3:0:[11023.1,10527.0,10913.1,12094.1,10914.1,12095.4,10777.1,12096.6,10778.1,12097.7,10780.1,12098.8]:: -> p(n7,n9,n6),p(n8,n7,n6),p(n8,n9,n6) % 1.75/0.89 12093:3:0:[11021.1,10524.0,10929.1,12088.2,10748.1,12089.3,10749.1,12090.4,10750.1,12091.5,10930.1,12092.8]:: -> p(n7,n8,n3),p(n9,n7,n3),p(n9,n8,n3) % 1.75/0.89 12087:2:0:[10717.1,10519.0,10719.1,12081.1,10720.1,12082.2,11028.0,12083.3,10875.1,12084.5,11039.1,12085.6,10877.1,12086.8]:: -> p(n8,n5,n7),p(n9,n5,n7) % 1.75/0.89 12080:2:0:[11018.0,10516.1,10868.1,12074.2,11027.0,12075.3,10870.1,12076.5,10774.0,12077.6,10776.0,12078.7,10779.0,12079.8]:: -> p(n7,n4,n4),p(n8,n5,n4) % 1.75/0.89 12073:3:0:[10801.1,10512.0,11015.1,12068.2,10735.0,12069.3,10737.0,12070.4,10739.0,12071.5,10803.1,12072.6]:: -> p(n7,n2,n9),p(n9,n2,n9),p(n9,n3,n9) % 1.75/0.89 12067:7:0:[11014.1,10511.2,11037.1,12066.6]:: -> p(n7,n1,n8),p(n7,n2,n8),p(n8,n1,n8),p(n8,n2,n8),p(n8,n3,n8),p(n9,n2,n8),p(n9,n3,n8) % 1.75/0.89 10575:1:0:[10534.0,189.1]:: p(n1,n3,n9) -> % 1.75/0.89 12065:5:0:[11013.0,10509.2,10757.0,12062.6,10763.0,12063.7,10766.0,12064.8]:: -> p(n7,n1,n6),p(n7,n2,n6),p(n8,n1,n6),p(n8,n2,n6),p(n8,n3,n6) % 1.75/0.89 10576:1:0:[10532.0,195.0]:: p(n1,n5,n6) -> % 1.75/0.89 12061:3:0:[10827.1,10506.2,10736.0,12056.3,10738.0,12057.4,10740.0,12058.5,11034.1,12059.6,10829.1,12060.8]:: -> p(n7,n1,n3),p(n7,n2,n3),p(n9,n2,n3) % 1.75/0.89 10577:1:0:[10533.0,202.1]:: p(n1,n4,n4) -> % 1.75/0.89 10578:1:0:[10532.0,204.0]:: p(n1,n6,n6) -> % 1.75/0.89 12055:3:0:[10646.1,10501.0,10648.1,12050.1,10650.1,12051.2,10995.1,12052.3,11008.1,12053.7,11011.0,12054.8]:: -> p(n5,n8,n7),p(n5,n9,n7),p(n6,n7,n7) % 1.75/0.89 12049:2:0:[10637.1,10498.0,10638.1,12043.1,10641.1,12044.2,10993.1,12045.3,10932.0,12046.5,11007.0,12047.7,10935.0,12048.8]:: -> p(n5,n8,n4),p(n6,n7,n4) % 1.75/0.89 10579:1:0:[10532.0,213.0]:: p(n1,n7,n6) -> % 1.75/0.89 12042:2:0:[10898.0,10496.0,10982.0,12036.1,10986.0,12037.2,10900.0,12038.3,10902.0,12039.6,11005.0,12040.7,11009.0,12041.8]:: -> p(n5,n8,n2),p(n5,n9,n2) % 1.75/0.89 12035:6:0:[10702.0,10493.6,10704.0,12033.7,10706.0,12034.8]:: -> p(n4,n4,n8),p(n4,n5,n8),p(n4,n6,n8),p(n5,n4,n8),p(n5,n5,n8),p(n5,n6,n8) % 1.75/0.89 10580:1:0:[10532.0,222.0]:: p(n1,n8,n6) -> % 1.75/0.89 12032:4:0:[10634.1,10489.0,10635.1,12028.1,10636.1,12029.2,10866.1,12030.5,10867.1,12031.8]:: -> p(n5,n4,n4),p(n5,n5,n4),p(n6,n4,n4),p(n6,n5,n4) % 1.75/0.89 10581:1:0:[10532.0,231.0]:: p(n1,n9,n6) -> % 1.75/0.89 10582:1:0:[10534.0,234.1]:: p(n1,n4,n9) -> % 1.75/0.89 12027:3:0:[10976.1,10484.0,10979.1,12022.1,10991.1,12023.5,10688.0,12024.6,10698.0,12025.7,10700.0,12026.8]:: -> p(n4,n3,n8),p(n5,n1,n8),p(n5,n2,n8) % 1.75/0.89 10583:1:0:[10533.0,238.1]:: p(n1,n5,n4) -> % 1.75/0.89 12021:3:0:[10975.1,10482.0,10978.0,12016.1,10990.1,12017.5,10686.0,12018.6,10696.0,12019.7,10699.0,12020.8]:: -> p(n4,n3,n6),p(n5,n1,n6),p(n5,n2,n6) % 1.75/0.89 12015:3:0:[10639.0,10481.0,10647.0,12010.1,10651.0,12011.2,10989.1,12012.5,10999.0,12013.6,11004.1,12014.7]:: -> p(n5,n1,n5),p(n5,n2,n5),p(n6,n3,n5) % 1.75/0.89 12009:3:0:[10798.0,10478.0,10977.0,12004.1,10800.0,12005.3,10988.0,12006.5,10802.0,12007.6,11001.1,12008.7]:: -> p(n4,n3,n2),p(n5,n2,n2),p(n6,n3,n2) % 1.75/0.89 12003:5:0:[10919.0,10475.2,10923.0,12000.5,10974.1,12001.6,10926.0,12002.8]:: -> p(n1,n7,n8),p(n1,n8,n8),p(n2,n7,n8),p(n2,n8,n8),p(n3,n8,n8) % 1.75/0.89 11999:3:0:[10579.1,10473.0,10580.1,11994.1,10581.1,11995.2,10905.0,11996.4,10972.1,11997.6,10906.0,11998.7]:: -> p(n2,n7,n6),p(n2,n9,n6),p(n3,n9,n6) % 1.75/0.89 11993:5:0:[10916.0,10470.2,10922.0,11990.5,10971.0,11991.6,10925.0,11992.8]:: -> p(n1,n7,n3),p(n1,n8,n3),p(n2,n7,n3),p(n2,n8,n3),p(n3,n8,n3) % 1.75/0.89 11989:5:0:[10888.0,10469.0,10950.0,11986.2,10890.0,11987.3,10894.0,11988.6]:: -> p(n1,n8,n2),p(n2,n8,n2),p(n2,n9,n2),p(n3,n8,n2),p(n3,n9,n2) % 1.75/0.89 11985:4:0:[10566.1,10468.0,10567.1,11981.1,10568.1,11982.2,10889.0,11983.3,10891.0,11984.6]:: -> p(n2,n8,n1),p(n2,n9,n1),p(n3,n8,n1),p(n3,n9,n1) % 1.75/0.89 11980:4:0:[10946.1,10466.0,10949.1,11976.2,10956.1,11977.3,10959.1,11978.5,10970.0,11979.7]:: -> p(n1,n5,n8),p(n2,n5,n8),p(n3,n4,n8),p(n3,n6,n8) % 1.75/0.89 11975:3:0:[10944.0,10461.0,10869.0,11970.2,10954.0,11971.3,10874.0,11972.5,10967.0,11973.7,10878.0,11974.8]:: -> p(n1,n5,n3),p(n2,n5,n3),p(n3,n4,n3) % 1.75/0.89 10584:1:0:[10534.0,270.1]:: p(n1,n5,n9) -> % 1.75/0.89 11969:4:0:[10943.0,10460.0,10947.0,11965.2,10953.0,11966.3,10958.0,11967.5,10966.0,11968.7]:: -> p(n1,n5,n2),p(n2,n5,n2),p(n3,n4,n2),p(n3,n6,n2) % 1.75/0.89 10585:1:0:[10533.0,274.0]:: p(n1,n7,n4) -> % 1.75/0.89 11964:2:0:[10561.1,10459.0,10563.1,11958.1,10564.1,11959.2,10844.0,11960.3,10957.0,11961.5,10846.0,11962.6,10965.0,11963.7]:: -> p(n2,n5,n1),p(n3,n6,n1) % 1.75/0.89 11957:7:0:[10942.1,10457.0,10964.1,11956.8]:: -> p(n1,n2,n8),p(n1,n3,n8),p(n2,n1,n8),p(n2,n2,n8),p(n2,n3,n8),p(n3,n1,n8),p(n3,n2,n8) % 1.75/0.89 10586:1:0:[10533.0,283.0]:: p(n1,n8,n4) -> % 1.75/0.89 11955:5:0:[10562.0,10455.0,10570.0,11952.1,10573.0,11953.2,10963.1,11954.8]:: -> p(n2,n1,n6),p(n2,n2,n6),p(n2,n3,n6),p(n3,n1,n6),p(n3,n2,n6) % 1.75/0.89 11951:5:0:[10939.1,10452.0,10816.0,11948.2,10819.0,11949.5,10820.0,11950.8]:: -> p(n1,n2,n3),p(n2,n1,n3),p(n2,n2,n3),p(n3,n1,n3),p(n3,n2,n3) % 1.75/0.89 10587:1:0:[10533.0,292.0]:: p(n1,n9,n4) -> % 1.75/0.89 11947:5:0:[10788.0,10451.0,10791.0,11944.3,10792.0,11945.6,10962.0,11946.8]:: -> p(n1,n2,n2),p(n1,n3,n2),p(n2,n2,n2),p(n2,n3,n2),p(n3,n2,n2) % 1.75/0.89 10588:1:0:[10534.0,297.1]:: p(n1,n6,n9) -> % 1.75/0.89 11943:4:0:[10772.1,10448.0,10759.1,11939.1,10782.0,11940.3,10911.1,11941.4,10778.1,11942.5]:: -> p(n9,n8,n3),p(n9,n8,n7),p(n9,n8,n8),p(n9,n8,n9) % 1.75/0.89 11938:4:0:[10771.1,10447.0,10758.1,11934.1,10781.0,11935.3,10896.1,11936.4,10777.1,11937.5]:: -> p(n9,n7,n3),p(n9,n7,n7),p(n9,n7,n8),p(n9,n7,n9) % 1.75/0.89 11933:2:0:[10768.1,10445.0,10755.1,11927.1,11073.1,11928.2,10776.0,11929.3,10863.1,11930.4,10775.0,11931.5,10859.1,11932.8]:: -> p(n9,n5,n7),p(n9,n5,n8) % 1.75/0.89 11926:3:0:[10765.0,10443.0,10752.1,11921.1,10829.1,11922.2,10767.0,11923.3,10766.0,11924.5,10832.1,11925.6]:: -> p(n9,n3,n5),p(n9,n3,n8),p(n9,n3,n9) % 1.75/0.89 11920:4:0:[10762.0,10442.0,10751.1,11916.1,10764.0,11917.3,10763.0,11918.5,10813.1,11919.6]:: -> p(n9,n2,n3),p(n9,n2,n5),p(n9,n2,n8),p(n9,n2,n9) % 1.75/0.89 11915:3:0:[11074.1,10439.1,10749.1,11910.2,11078.0,11911.3,10910.1,11912.4,10914.1,11913.5,10745.1,11914.8]:: -> p(n8,n8,n1),p(n8,n8,n7),p(n8,n8,n8) % 1.75/0.89 10589:1:0:[10534.0,315.1]:: p(n1,n7,n9) -> % 1.75/0.89 11909:3:0:[10901.1,10438.0,10903.1,11904.1,10748.1,11905.2,11077.0,11906.3,10895.1,11907.4,10744.1,11908.8]:: -> p(n8,n7,n6),p(n8,n7,n7),p(n8,n7,n8) % 1.75/0.89 11903:4:0:[10815.1,10433.0,11066.0,11899.1,10738.0,11900.2,10812.1,11901.6,10737.0,11902.8]:: -> p(n8,n2,n4),p(n8,n2,n5),p(n8,n2,n6),p(n8,n2,n8) % 1.75/0.89 11898:3:0:[10787.1,10432.0,10804.0,11893.1,10736.0,11894.2,10797.1,11895.3,11065.1,11896.6,10735.0,11897.8]:: -> p(n8,n1,n5),p(n8,n1,n6),p(n8,n1,n8) % 1.75/0.89 10590:1:0:[10534.0,324.1]:: p(n1,n8,n9) -> % 1.75/0.89 10591:1:0:[10535.0,347.1]:: p(n2,n1,n5) -> % 1.75/0.89 11892:2:0:[10734.1,10431.1,10929.1,11886.2,10937.0,11887.3,10731.1,11888.4,10724.1,11889.6,10933.1,11890.7,10920.1,11891.8]:: -> p(n7,n9,n1),p(n7,n9,n6) % 1.75/0.89 11885:4:0:[10733.1,10430.1,11076.0,11881.3,10730.1,11882.4,10913.1,11883.5,10723.1,11884.6]:: -> p(n7,n8,n1),p(n7,n8,n3),p(n7,n8,n8),p(n7,n8,n9) % 1.75/0.89 10592:1:0:[10536.0,367.1]:: p(n2,n1,n7) -> % 1.75/0.89 11880:1:0:[11070.0,10428.0,10732.0,11873.1,10883.0,11874.2,10868.1,11875.3,10727.1,11876.4,10884.0,11877.5,10720.1,11878.6,11069.0,11879.8]:: -> p(n7,n6,n8) % 1.75/0.89 11872:2:0:[10851.0,10426.0,10726.0,11866.1,11068.0,11867.2,10725.0,11868.4,10838.1,11869.5,10717.1,11870.6,10850.0,11871.8]:: -> p(n7,n4,n4),p(n7,n4,n8) % 1.75/0.89 11865:5:0:[10814.1,10424.0,10716.0,11862.1,10715.0,11863.4,10714.0,11864.6]:: -> p(n7,n2,n3),p(n7,n2,n4),p(n7,n2,n6),p(n7,n2,n8),p(n7,n2,n9) % 1.75/0.89 11861:3:0:[10786.1,10423.0,10713.0,11856.1,10796.1,11857.3,10712.0,11858.4,10711.0,11859.6,10801.1,11860.8]:: -> p(n7,n1,n3),p(n7,n1,n6),p(n7,n1,n8) % 1.75/0.89 11855:2:0:[10694.1,10420.0,10902.0,11849.1,11062.1,11850.2,10893.1,11851.4,10707.0,11852.5,10708.0,11853.7,10685.1,11854.8]:: -> p(n6,n7,n4),p(n6,n7,n7) % 1.75/0.89 11848:2:0:[10693.1,10419.0,10882.0,11842.2,10867.1,11843.3,10705.0,11844.5,10873.1,11845.6,10706.0,11846.7,10684.1,11847.8]:: -> p(n6,n6,n2),p(n6,n6,n5) % 1.75/0.89 10593:1:0:[10535.0,410.1]:: p(n2,n2,n5) -> % 1.75/0.89 11841:4:0:[10692.1,10418.0,10861.0,11837.4,10703.0,11838.5,10704.0,11839.7,10683.1,11840.8]:: -> p(n6,n5,n2),p(n6,n5,n3),p(n6,n5,n4),p(n6,n5,n7) % 1.75/0.89 11836:4:0:[10691.1,10417.0,10841.1,11832.4,10701.0,11833.5,10702.0,11834.7,10682.1,11835.8]:: -> p(n6,n4,n2),p(n6,n4,n3),p(n6,n4,n4),p(n6,n4,n7) % 1.75/0.89 10594:1:0:[10536.0,430.1]:: p(n2,n2,n7) -> % 1.75/0.89 11831:2:0:[10690.1,10416.0,10826.1,11825.2,10822.1,11826.3,10699.0,11827.5,10830.0,11828.6,10700.0,11829.7,10681.1,11830.8]:: -> p(n6,n3,n2),p(n6,n3,n5) % 1.75/0.89 11824:2:0:[10678.1,10413.0,10673.1,11818.2,10932.0,11819.3,11061.1,11820.4,11064.0,11821.5,10931.0,11822.7,10918.1,11823.8]:: -> p(n5,n9,n2),p(n5,n9,n7) % 1.75/0.89 11817:4:0:[10677.1,10412.0,10672.1,11813.2,10907.1,11814.4,10912.0,11815.5,11063.0,11816.7]:: -> p(n5,n8,n2),p(n5,n8,n4),p(n5,n8,n7),p(n5,n8,n9) % 1.75/0.89 11812:4:0:[10676.0,10410.0,10669.1,11808.2,10866.1,11809.3,10881.0,11810.5,10872.1,11811.6]:: -> p(n5,n6,n2),p(n5,n6,n5),p(n5,n6,n8),p(n5,n6,n9) % 1.75/0.89 11807:5:0:[10675.0,10409.0,10668.1,11804.2,10860.0,11805.4,10857.1,11806.8]:: -> p(n5,n5,n2),p(n5,n5,n4),p(n5,n5,n6),p(n5,n5,n7),p(n5,n5,n8) % 1.75/0.89 11803:4:0:[10674.0,10408.0,10667.1,11799.2,10840.1,11800.4,10837.1,11801.5,10849.0,11802.8]:: -> p(n5,n4,n2),p(n5,n4,n4),p(n5,n4,n7),p(n5,n4,n8) % 1.75/0.89 10595:1:0:[10535.0,464.1]:: p(n2,n3,n5) -> % 1.75/0.89 11798:4:0:[10666.0,10406.0,10665.0,11794.2,11054.1,11795.3,10809.1,11796.6,11058.0,11797.8]:: -> p(n5,n2,n2),p(n5,n2,n5),p(n5,n2,n6),p(n5,n2,n8) % 1.75/0.89 11793:3:0:[10664.0,10405.0,10800.0,11788.1,10663.0,11789.2,10793.1,11790.3,11055.1,11791.6,10799.0,11792.8]:: -> p(n5,n1,n5),p(n5,n1,n6),p(n5,n1,n8) % 1.75/0.89 10596:1:0:[10536.0,484.1]:: p(n2,n3,n7) -> % 1.75/0.89 11787:1:0:[10897.0,10402.0,10898.0,11780.1,10660.0,11781.2,10637.1,11782.3,10659.0,11783.4,11059.0,11784.5,10646.1,11785.6,11060.0,11786.7]:: -> p(n4,n7,n9) % 1.75/0.89 11779:4:0:[10658.0,10401.2,10636.1,11775.3,10657.0,11776.4,10880.0,11777.5,10645.1,11778.6]:: -> p(n4,n6,n1),p(n4,n6,n2),p(n4,n6,n8),p(n4,n6,n9) % 1.75/0.89 11774:4:0:[10656.0,10400.2,10635.1,11770.3,10655.0,11771.4,10644.1,11772.6,10856.1,11773.8]:: -> p(n4,n5,n1),p(n4,n5,n2),p(n4,n5,n6),p(n4,n5,n8) % 1.75/0.89 11769:2:0:[10848.0,10399.0,10654.0,11763.2,10634.1,11764.3,10653.0,11765.4,10836.1,11766.5,10643.1,11767.6,10847.0,11768.8]:: -> p(n4,n4,n2),p(n4,n4,n8) % 1.75/0.89 11762:3:0:[11057.0,10398.0,10652.0,11757.2,10633.1,11758.3,10651.0,11759.4,10642.1,11760.6,11056.0,11761.8]:: -> p(n4,n3,n2),p(n4,n3,n6),p(n4,n3,n8) % 1.75/0.89 11756:4:0:[10925.0,10395.2,10620.1,11752.3,10630.1,11753.4,10926.0,11754.7,10627.1,11755.8]:: -> p(n3,n9,n1),p(n3,n9,n2),p(n3,n9,n6),p(n3,n9,n7) % 1.75/0.89 10597:1:0:[10535.0,518.0]:: p(n2,n5,n5) -> % 1.75/0.89 10598:1:0:[10535.0,527.0]:: p(n2,n6,n5) -> % 1.75/0.89 10599:1:0:[10536.0,529.1]:: p(n2,n4,n7) -> % 1.75/0.89 10600:1:0:[10535.0,536.0]:: p(n2,n7,n5) -> % 1.75/0.89 11751:5:0:[10619.1,10394.3,10629.1,11748.4,10906.0,11749.5,10626.1,11750.8]:: -> p(n3,n8,n1),p(n3,n8,n2),p(n3,n8,n3),p(n3,n8,n7),p(n3,n8,n8) % 1.75/0.89 10601:1:0:[10535.0,545.0]:: p(n2,n8,n5) -> % 1.75/0.89 11747:3:0:[10878.0,10392.2,10616.1,11742.3,10628.0,11743.4,10879.0,11744.5,10871.1,11745.6,10623.1,11746.8]:: -> p(n3,n6,n1),p(n3,n6,n2),p(n3,n6,n8) % 1.75/0.89 10602:1:0:[10535.0,554.0]:: p(n2,n9,n5) -> % 1.75/0.89 11741:3:0:[10846.0,10390.0,10613.1,11736.3,10622.0,11737.4,10835.1,11738.5,11051.1,11739.6,10621.0,11740.8]:: -> p(n3,n4,n2),p(n3,n4,n3),p(n3,n4,n8) % 1.75/0.89 11735:4:0:[10808.0,10388.0,10610.0,11731.3,10612.0,11732.4,10807.0,11733.6,10611.0,11734.8]:: -> p(n3,n2,n2),p(n3,n2,n3),p(n3,n2,n6),p(n3,n2,n8) % 1.75/0.89 10603:1:0:[10536.0,565.1]:: p(n2,n5,n7) -> % 1.75/0.89 11730:3:0:[10922.0,10386.2,10924.0,11725.3,10602.1,11726.4,10606.1,11727.6,10923.0,11728.7,10915.1,11729.8]:: -> p(n2,n9,n1),p(n2,n9,n2),p(n2,n9,n6) % 1.75/0.89 11724:5:0:[10601.1,10385.4,10905.0,11721.5,10605.1,11722.6,11053.1,11723.8]:: -> p(n2,n8,n1),p(n2,n8,n2),p(n2,n8,n3),p(n2,n8,n4),p(n2,n8,n8) % 1.75/0.89 11720:4:0:[10889.0,10384.0,10890.0,11716.1,10600.1,11717.4,10604.1,11718.6,11052.1,11719.8]:: -> p(n2,n7,n3),p(n2,n7,n4),p(n2,n7,n6),p(n2,n7,n8) % 1.75/0.89 11715:4:0:[11050.1,10382.3,10597.1,11711.4,11048.1,11712.5,10603.0,11713.6,10855.0,11714.8]:: -> p(n2,n5,n1),p(n2,n5,n2),p(n2,n5,n3),p(n2,n5,n8) % 1.75/0.89 11710:4:0:[11046.1,10380.0,10819.0,11706.2,10818.0,11707.3,10595.0,11708.4,10596.0,11709.6]:: -> p(n2,n3,n2),p(n2,n3,n6),p(n2,n3,n8),p(n2,n3,n9) % 1.75/0.89 11705:5:0:[10806.0,10379.0,11047.0,11702.3,10593.0,11703.4,10594.0,11704.6]:: -> p(n2,n2,n2),p(n2,n2,n3),p(n2,n2,n6),p(n2,n2,n8),p(n2,n2,n9) % 1.75/0.89 11701:3:0:[10783.1,10378.0,10791.0,11696.1,10789.0,11697.3,10591.0,11698.4,10592.0,11699.6,10790.0,11700.8]:: -> p(n2,n1,n3),p(n2,n1,n6),p(n2,n1,n8) % 1.75/0.89 10604:1:0:[10536.0,601.0]:: p(n2,n7,n7) -> % 1.75/0.89 11695:4:0:[10567.1,10376.0,10586.1,11691.3,10904.0,11692.4,10580.1,11693.5,10590.0,11694.8]:: -> p(n1,n8,n2),p(n1,n8,n3),p(n1,n8,n7),p(n1,n8,n8) % 1.75/0.89 10605:1:0:[10536.0,610.0]:: p(n2,n8,n7) -> % 1.75/0.89 11690:3:0:[10566.1,10375.0,10888.0,11685.1,10585.1,11686.3,10887.0,11687.4,10579.1,11688.5,10589.0,11689.8]:: -> p(n1,n7,n3),p(n1,n7,n7),p(n1,n7,n8) % 1.75/0.89 10606:1:0:[10536.0,619.0]:: p(n2,n9,n7) -> % 1.75/0.89 11684:3:0:[10563.1,10373.0,10583.0,11679.3,10854.0,11680.4,10576.1,11681.5,11049.0,11682.6,10584.0,11683.8]:: -> p(n1,n5,n2),p(n1,n5,n3),p(n1,n5,n8) % 1.75/0.89 11678:3:0:[10560.1,10371.0,10816.0,11673.2,10574.0,11674.3,10573.0,11675.5,10817.0,11676.6,10575.0,11677.8]:: -> p(n1,n3,n2),p(n1,n3,n5),p(n1,n3,n8) % 1.75/0.89 11672:4:0:[10559.1,10370.0,10571.0,11668.3,10570.0,11669.5,10805.0,11670.6,10572.0,11671.8]:: -> p(n1,n2,n2),p(n1,n2,n3),p(n1,n2,n5),p(n1,n2,n8) % 1.75/0.89 11667:3:0:[10952.0,10366.0,10606.1,11662.1,10650.1,11663.3,11011.0,11664.5,10724.1,11665.6,11045.1,11666.8]:: -> p(n3,n9,n7),p(n5,n9,n7),p(n8,n9,n7) % 1.75/0.89 11661:4:0:[10581.1,10365.0,10987.1,11657.3,11064.0,11658.4,10709.1,11659.5,10780.1,11660.8]:: -> p(n2,n9,n6),p(n3,n9,n6),p(n7,n9,n6),p(n8,n9,n6) % 1.75/0.89 11656:1:0:[10951.0,10364.0,10602.1,11649.1,10630.1,11650.2,10662.1,11651.3,11061.1,11652.4,11010.0,11653.5,10731.1,11654.6,11044.1,11655.8]:: -> p(n8,n9,n5) % 1.75/0.89 10607:1:0:[10537.0,661.1]:: p(n3,n1,n4) -> % 1.75/0.89 11648:3:0:[10950.0,10361.0,10986.0,11643.3,11009.0,11644.5,10734.1,11645.6,11075.1,11646.7,10760.1,11647.8]:: -> p(n2,n9,n2),p(n3,n9,n2),p(n5,n9,n2) % 1.75/0.89 11642:4:0:[10568.1,10360.0,10985.0,11638.3,10678.1,11639.4,10697.1,11640.5,10773.1,11641.8]:: -> p(n2,n9,n1),p(n3,n9,n1),p(n7,n9,n1),p(n8,n9,n1) % 1.75/0.89 10608:1:0:[10538.0,684.1]:: p(n3,n1,n9) -> % 1.75/0.89 11637:3:0:[10590.0,10359.0,11053.1,11632.1,10626.1,11633.2,10984.1,11634.3,10687.1,11635.5,10745.1,11636.7]:: -> p(n5,n8,n9),p(n7,n8,n9),p(n9,n8,n9) % 1.75/0.89 11631:6:0:[10983.1,10358.3,11063.0,11629.4,10710.0,11630.5]:: -> p(n1,n8,n8),p(n2,n8,n8),p(n3,n8,n8),p(n7,n8,n8),p(n8,n8,n8),p(n9,n8,n8) % 1.75/0.89 11628:5:0:[10605.1,10357.1,10648.1,11625.3,11008.1,11626.5,10723.1,11627.6]:: -> p(n1,n8,n7),p(n3,n8,n7),p(n5,n8,n7),p(n8,n8,n7),p(n9,n8,n7) % 1.75/0.89 10609:1:0:[10539.0,698.1]:: p(n3,n1,n5) -> % 1.75/0.89 11624:2:0:[10586.1,10354.0,10619.1,11618.2,10638.1,11619.3,11007.0,11620.5,11076.0,11621.6,11078.0,11622.7,10782.0,11623.8]:: -> p(n2,n8,n4),p(n5,n8,n4) % 1.75/0.89 11617:5:0:[10661.0,10353.3,10672.1,11614.4,11006.0,11615.5,10749.1,11616.7]:: -> p(n1,n8,n3),p(n2,n8,n3),p(n3,n8,n3),p(n7,n8,n3),p(n9,n8,n3) % 1.75/0.89 11613:4:0:[10982.0,10352.3,11005.0,11609.5,10733.1,11610.6,11074.1,11611.7,10759.1,11612.8]:: -> p(n1,n8,n2),p(n2,n8,n2),p(n3,n8,n2),p(n5,n8,n2) % 1.75/0.89 11608:4:0:[10567.1,10351.0,10981.0,11604.3,10677.1,11605.4,10695.1,11606.5,10772.1,11607.8]:: -> p(n2,n8,n1),p(n3,n8,n1),p(n7,n8,n1),p(n8,n8,n1) % 1.75/0.89 11603:2:0:[10589.0,10350.0,11052.1,11597.1,10625.1,11598.2,10997.1,11599.4,10685.1,11600.5,11025.1,11601.6,10744.1,11602.7]:: -> p(n4,n7,n9),p(n9,n7,n9) % 1.75/0.89 11596:4:0:[10974.1,10349.2,11060.0,11592.3,10996.1,11593.4,10708.0,11594.5,11024.1,11595.6]:: -> p(n1,n7,n8),p(n2,n7,n8),p(n8,n7,n8),p(n9,n7,n8) % 1.75/0.89 11591:4:0:[10604.1,10348.1,10973.1,11587.2,10646.1,11588.3,10995.1,11589.4,10722.1,11590.6]:: -> p(n1,n7,n7),p(n6,n7,n7),p(n8,n7,n7),p(n9,n7,n7) % 1.75/0.89 10610:1:0:[10537.0,724.1]:: p(n3,n2,n4) -> % 1.75/0.89 11586:2:0:[10579.1,10347.0,10972.1,11580.2,11059.0,11581.3,10994.1,11582.4,10707.0,11583.5,11023.1,11584.6,10777.1,11585.8]:: -> p(n2,n7,n6),p(n8,n7,n6) % 1.75/0.89 11579:2:0:[10585.1,10345.0,10617.1,11573.2,10637.1,11574.3,10993.1,11575.4,11022.1,11576.6,11077.0,11577.7,10781.0,11578.8]:: -> p(n2,n7,n4),p(n6,n7,n4) % 1.75/0.89 10611:1:0:[10538.0,747.1]:: p(n3,n2,n9) -> % 1.75/0.89 11572:3:0:[10971.0,10344.2,10660.0,11567.3,10671.1,11568.4,11062.1,11569.5,11021.1,11570.6,10748.1,11571.7]:: -> p(n1,n7,n3),p(n2,n7,n3),p(n9,n7,n3) % 1.75/0.89 11566:2:0:[10588.0,10341.0,10960.1,11560.1,10623.1,11561.2,10684.1,11562.5,11069.0,11563.6,10743.1,11564.7,11043.1,11565.8]:: -> p(n4,n6,n9),p(n5,n6,n9) % 1.75/0.89 11559:4:0:[10949.1,10340.0,10959.1,11555.1,10706.0,11556.5,11033.1,11557.7,11042.1,11558.8]:: -> p(n3,n6,n8),p(n4,n6,n8),p(n5,n6,n8),p(n7,n6,n8) % 1.75/0.89 10612:1:0:[10539.0,761.1]:: p(n3,n2,n5) -> % 1.75/0.89 11554:2:0:[10948.1,10337.0,10598.1,11548.1,10628.0,11549.2,10657.0,11550.3,10727.1,11551.6,11032.1,11552.7,11041.0,11553.8]:: -> p(n5,n6,n5),p(n6,n6,n5) % 1.75/0.89 11547:4:0:[10947.0,10334.0,10958.0,11543.1,10732.0,11544.6,11031.0,11545.7,10756.1,11546.8]:: -> p(n3,n6,n2),p(n4,n6,n2),p(n5,n6,n2),p(n6,n6,n2) % 1.75/0.89 11542:2:0:[10564.1,10333.0,10957.0,11536.1,10676.0,11537.4,10693.1,11538.5,11070.0,11539.6,11030.0,11540.7,10769.1,11541.8]:: -> p(n3,n6,n1),p(n4,n6,n1) % 1.75/0.89 11535:6:0:[10970.0,10331.2,10704.0,11533.5,11020.1,11534.6]:: -> p(n1,n5,n8),p(n2,n5,n8),p(n4,n5,n8),p(n5,n5,n8),p(n8,n5,n8),p(n9,n5,n8) % 1.75/0.89 11532:4:0:[11049.0,10330.0,10603.0,11528.1,10969.0,11529.2,10644.1,11530.3,10719.1,11531.6]:: -> p(n5,n5,n7),p(n6,n5,n7),p(n8,n5,n7),p(n9,n5,n7) % 1.75/0.89 11527:2:0:[10576.1,10329.0,11048.1,11521.1,10968.0,11522.2,10703.0,11523.5,11019.1,11524.6,11072.0,11525.7,10775.0,11526.8]:: -> p(n4,n5,n6),p(n5,n5,n6) % 1.75/0.89 11520:3:0:[10583.0,10327.0,11050.1,11515.1,10614.1,11516.2,10635.1,11517.3,11018.0,11518.6,10776.0,11519.8]:: -> p(n5,n5,n4),p(n6,n5,n4),p(n8,n5,n4) % 1.75/0.89 10613:1:0:[10537.0,787.0]:: p(n3,n4,n4) -> % 1.75/0.89 10614:1:0:[10537.0,796.0]:: p(n3,n5,n4) -> % 1.75/0.89 10615:1:0:[10538.0,801.1]:: p(n3,n3,n9) -> % 1.75/0.89 10616:1:0:[10537.0,805.0]:: p(n3,n6,n4) -> % 1.75/0.89 11514:3:0:[10967.0,10326.2,10656.0,11509.3,10668.1,11510.4,11017.0,11511.6,10747.0,11512.7,11073.1,11513.8]:: -> p(n1,n5,n3),p(n2,n5,n3),p(n6,n5,n3) % 1.75/0.89 10617:1:0:[10537.0,814.0]:: p(n3,n7,n4) -> % 1.75/0.89 10618:1:0:[10539.0,815.1]:: p(n3,n3,n5) -> % 1.75/0.89 11508:2:0:[10563.1,10324.0,10965.0,11502.2,10675.0,11503.4,10692.1,11504.5,11016.0,11505.6,11071.0,11506.7,10768.1,11507.8]:: -> p(n2,n5,n1),p(n4,n5,n1) % 1.75/0.89 10619:1:0:[10537.0,823.0]:: p(n3,n8,n4) -> % 1.75/0.89 11501:4:0:[10946.1,10322.0,10956.1,11497.1,10702.0,11498.5,11029.0,11499.7,11040.1,11500.8]:: -> p(n3,n4,n8),p(n4,n4,n8),p(n5,n4,n8),p(n7,n4,n8) % 1.75/0.89 11496:2:0:[10945.1,10321.0,10599.0,11490.1,11051.1,11491.2,10643.1,11492.3,10717.1,11493.6,11028.0,11494.7,11039.1,11495.8]:: -> p(n5,n4,n7),p(n6,n4,n7) % 1.75/0.89 10620:1:0:[10537.0,832.0]:: p(n3,n9,n4) -> % 1.75/0.89 11489:3:0:[10577.0,10318.0,10955.0,11484.1,10613.1,11485.2,10634.1,11486.3,11027.0,11487.7,10774.0,11488.8]:: -> p(n5,n4,n4),p(n6,n4,n4),p(n7,n4,n4) % 1.75/0.89 11483:2:0:[10944.0,10317.0,10954.0,11477.1,10654.0,11478.3,10667.1,11479.4,11068.0,11480.6,10742.0,11481.7,11038.1,11482.8]:: -> p(n3,n4,n3),p(n6,n4,n3) % 1.75/0.89 11476:4:0:[10943.0,10316.0,10953.0,11472.1,10726.0,11473.6,11026.0,11474.7,10754.1,11475.8]:: -> p(n3,n4,n2),p(n4,n4,n2),p(n5,n4,n2),p(n6,n4,n2) % 1.75/0.89 10621:1:0:[10538.0,846.1]:: p(n3,n4,n9) -> % 1.75/0.89 11471:2:0:[10575.0,10314.0,10615.0,11465.2,11056.0,11466.3,10992.1,11467.4,10681.1,11468.5,11015.1,11469.6,10739.0,11470.7]:: -> p(n2,n3,n9),p(n9,n3,n9) % 1.75/0.89 11464:5:0:[10964.1,10313.2,10991.1,11461.4,10700.0,11462.5,11014.1,11463.6]:: -> p(n1,n3,n8),p(n2,n3,n8),p(n4,n3,n8),p(n8,n3,n8),p(n9,n3,n8) % 1.75/0.89 11460:3:0:[10573.0,10311.0,10963.1,11455.2,10990.1,11456.4,10699.0,11457.5,11013.0,11458.6,10766.0,11459.8]:: -> p(n2,n3,n6),p(n4,n3,n6),p(n8,n3,n6) % 1.75/0.89 10622:1:0:[10539.0,860.1]:: p(n3,n4,n5) -> % 1.75/0.89 11454:4:0:[10595.0,10310.1,10618.0,11450.2,10651.0,11451.3,10989.1,11452.4,10718.0,11453.6]:: -> p(n1,n3,n5),p(n6,n3,n5),p(n8,n3,n5),p(n9,n3,n5) % 1.75/0.89 11449:4:0:[10962.0,10307.2,10988.0,11445.4,10721.0,11446.6,11067.0,11447.7,10752.1,11448.8]:: -> p(n1,n3,n2),p(n2,n3,n2),p(n4,n3,n2),p(n6,n3,n2) % 1.75/0.89 11444:1:0:[10560.1,10306.0,11046.1,11437.1,10961.0,11438.2,11057.0,11439.3,10670.0,11440.4,10690.1,11441.5,11012.0,11442.6,10765.0,11443.8]:: -> p(n8,n3,n1) % 1.75/0.89 11436:3:0:[10572.0,10305.0,10611.0,11431.2,10980.1,11432.3,11058.0,11433.4,10680.1,11434.5,10737.0,11435.7]:: -> p(n2,n2,n9),p(n7,n2,n9),p(n9,n2,n9) % 1.75/0.89 11430:7:0:[10979.1,10304.3,10698.0,11429.5]:: -> p(n1,n2,n8),p(n2,n2,n8),p(n3,n2,n8),p(n5,n2,n8),p(n7,n2,n8),p(n8,n2,n8),p(n9,n2,n8) % 1.75/0.89 11428:5:0:[10570.0,10302.0,10978.0,11425.3,10696.0,11426.5,10763.0,11427.8]:: -> p(n2,n2,n6),p(n3,n2,n6),p(n5,n2,n6),p(n7,n2,n6),p(n8,n2,n6) % 1.75/0.89 11424:4:0:[10593.0,10301.1,10612.0,11420.2,10647.0,11421.3,11004.1,11422.5,10715.0,11423.6]:: -> p(n1,n2,n5),p(n5,n2,n5),p(n8,n2,n5),p(n9,n2,n5) % 1.75/0.89 11419:2:0:[10571.0,10300.0,11047.0,11413.1,10610.0,11414.2,10631.1,11415.3,11054.1,11416.4,11003.1,11417.5,10764.0,11418.8]:: -> p(n7,n2,n4),p(n8,n2,n4) % 1.75/0.89 10623:1:0:[10538.0,891.0]:: p(n3,n6,n9) -> % 1.75/0.89 11412:5:0:[10649.0,10299.3,10665.0,11409.4,11002.1,11410.5,10738.0,11411.7]:: -> p(n1,n2,n3),p(n2,n2,n3),p(n3,n2,n3),p(n7,n2,n3),p(n9,n2,n3) % 1.75/0.89 10624:1:0:[10539.0,896.1]:: p(n3,n5,n5) -> % 1.75/0.89 10625:1:0:[10538.0,900.0]:: p(n3,n7,n9) -> % 1.75/0.89 11408:4:0:[10977.0,10298.3,11001.1,11404.5,10716.0,11405.6,11066.0,11406.7,10751.1,11407.8]:: -> p(n1,n2,n2),p(n2,n2,n2),p(n3,n2,n2),p(n5,n2,n2) % 1.75/0.89 11403:5:0:[10942.1,10295.0,10976.1,11400.3,10688.0,11401.5,11037.1,11402.8]:: -> p(n2,n1,n8),p(n3,n1,n8),p(n5,n1,n8),p(n7,n1,n8),p(n8,n1,n8) % 1.75/0.89 10626:1:0:[10538.0,909.0]:: p(n3,n8,n9) -> % 1.75/0.89 11399:1:0:[10941.1,10294.0,10592.0,11392.1,10632.0,11393.3,11055.1,11394.4,11000.0,11395.5,10711.0,11396.6,11065.1,11397.7,11036.1,11398.8]:: -> p(n3,n1,n7) % 1.75/0.89 11391:5:0:[10562.0,10293.0,10975.1,11388.3,10686.0,11389.5,10757.0,11390.8]:: -> p(n2,n1,n6),p(n3,n1,n6),p(n5,n1,n6),p(n7,n1,n6),p(n8,n1,n6) % 1.75/0.89 10627:1:0:[10538.0,918.0]:: p(n3,n9,n9) -> % 1.75/0.89 11387:2:0:[10940.1,10292.0,10591.0,11381.1,10609.0,11382.2,10639.0,11383.3,10999.0,11384.5,10712.0,11385.6,11035.1,11386.8]:: -> p(n5,n1,n5),p(n8,n1,n5) % 1.75/0.89 10628:1:0:[10539.0,923.1]:: p(n3,n6,n5) -> % 1.75/0.89 11380:3:0:[10939.1,10290.0,10640.0,11375.3,10663.0,11376.4,10998.0,11377.5,10736.0,11378.7,11034.1,11379.8]:: -> p(n2,n1,n3),p(n3,n1,n3),p(n7,n1,n3) % 1.75/0.89 11374:4:0:[10803.1,10287.0,10853.1,11370.3,10859.1,11371.4,11043.1,11372.5,10921.1,11373.8]:: -> p(n9,n2,n9),p(n9,n3,n9),p(n9,n7,n9),p(n9,n8,n9) % 1.75/0.89 11369:5:0:[11037.1,10286.0,11040.1,11366.3,11042.1,11367.5,10936.1,11368.8]:: -> p(n9,n2,n8),p(n9,n3,n8),p(n9,n5,n8),p(n9,n7,n8),p(n9,n8,n8) % 1.75/0.89 11365:3:0:[11036.1,10285.0,10813.1,11360.1,10832.1,11361.2,11039.1,11362.3,10877.1,11363.5,11045.1,11364.8]:: -> p(n9,n5,n7),p(n9,n7,n7),p(n9,n8,n7) % 1.75/0.89 11359:2:0:[11035.1,10283.0,10845.1,11353.3,10863.1,11354.4,11041.0,11355.5,10896.1,11356.6,10911.1,11357.7,11044.1,11358.8]:: -> p(n9,n2,n5),p(n9,n3,n5) % 1.75/0.89 11352:3:0:[11034.1,10281.0,10829.1,11347.2,11038.1,11348.3,11073.1,11349.4,10885.1,11350.5,10930.1,11351.8]:: -> p(n9,n2,n3),p(n9,n7,n3),p(n9,n8,n3) % 1.75/0.89 11346:6:0:[11029.0,10277.3,11033.1,11344.5,10934.1,11345.8]:: -> p(n8,n1,n8),p(n8,n2,n8),p(n8,n3,n8),p(n8,n5,n8),p(n8,n7,n8),p(n8,n8,n8) % 1.75/0.89 11343:4:0:[11065.1,10276.0,10812.1,11339.1,10831.1,11340.2,11028.0,11341.3,10875.1,11342.5]:: -> p(n8,n5,n7),p(n8,n7,n7),p(n8,n8,n7),p(n8,n9,n7) % 1.75/0.89 10629:1:0:[10539.0,950.0]:: p(n3,n8,n5) -> % 1.75/0.89 11338:5:0:[10839.1,10275.3,11072.0,11335.4,10886.0,11336.5,10914.1,11337.7]:: -> p(n8,n1,n6),p(n8,n2,n6),p(n8,n3,n6),p(n8,n7,n6),p(n8,n9,n6) % 1.75/0.89 11334:4:0:[10842.1,10274.3,10862.1,11330.4,11032.1,11331.5,10895.1,11332.6,10910.1,11333.7]:: -> p(n8,n1,n5),p(n8,n2,n5),p(n8,n3,n5),p(n8,n9,n5) % 1.75/0.89 10630:1:0:[10539.0,959.0]:: p(n3,n9,n5) -> % 1.75/0.89 11329:2:0:[10797.1,10273.0,10825.1,11323.2,11027.0,11324.3,10870.1,11325.5,11077.0,11326.6,11078.0,11327.7,10938.0,11328.8]:: -> p(n8,n2,n4),p(n8,n5,n4) % 1.75/0.89 11322:1:0:[10804.0,10271.0,11066.0,11315.1,11067.0,11316.2,11026.0,11317.3,11031.0,11318.5,10903.1,11319.6,11074.1,11320.7,11075.1,11321.8]:: -> p(n8,n5,n2) % 1.75/0.89 11314:3:0:[10787.1,10270.0,10815.1,11309.1,10852.0,11310.3,11071.0,11311.4,11030.0,11312.5,10901.1,11313.6]:: -> p(n8,n3,n1),p(n8,n8,n1),p(n8,n9,n1) % 1.75/0.89 11308:2:0:[10801.1,10269.0,11015.1,11302.2,10850.0,11303.3,10858.1,11304.4,11069.0,11305.5,11025.1,11306.6,10920.1,11307.8]:: -> p(n7,n2,n9),p(n7,n8,n9) % 1.75/0.89 10631:1:0:[10540.0,976.0]:: p(n4,n2,n4) -> % 1.75/0.89 10632:1:0:[10541.0,979.1]:: p(n4,n1,n7) -> % 1.75/0.89 10633:1:0:[10540.0,985.0]:: p(n4,n3,n4) -> % 1.75/0.89 11301:5:0:[11014.1,10268.2,11020.1,11298.4,11024.1,11299.6,10933.1,11300.8]:: -> p(n7,n1,n8),p(n7,n2,n8),p(n7,n4,n8),p(n7,n6,n8),p(n7,n8,n8) % 1.75/0.89 10634:1:0:[10540.0,994.0]:: p(n4,n4,n4) -> % 1.75/0.89 11297:3:0:[11013.0,10266.2,10838.1,11292.3,11019.1,11293.4,10884.0,11294.5,11023.1,11295.6,10913.1,11296.7]:: -> p(n7,n1,n6),p(n7,n2,n6),p(n7,n9,n6) % 1.75/0.89 10635:1:0:[10540.0,1003.0]:: p(n4,n5,n4) -> % 1.75/0.89 11291:2:0:[10796.1,10264.0,10823.1,11285.2,11018.0,11286.4,10868.1,11287.5,11022.1,11288.6,11076.0,11289.7,10937.0,11290.8]:: -> p(n7,n2,n4),p(n7,n4,n4) % 1.75/0.89 10636:1:0:[10540.0,1012.0]:: p(n4,n6,n4) -> % 1.75/0.89 11284:3:0:[10827.1,10263.2,11068.0,11279.3,11017.0,11280.4,10883.0,11281.5,11021.1,11282.6,10929.1,11283.8]:: -> p(n7,n1,n3),p(n7,n2,n3),p(n7,n8,n3) % 1.75/0.89 10637:1:0:[10540.0,1021.0]:: p(n4,n7,n4) -> % 1.75/0.89 11278:2:0:[10786.1,10261.0,10814.1,11272.1,11012.0,11273.2,10851.0,11274.3,11016.0,11275.4,11070.0,11276.5,10899.1,11277.6]:: -> p(n7,n8,n1),p(n7,n9,n1) % 1.75/0.89 10638:1:0:[10540.0,1030.0]:: p(n4,n8,n4) -> % 1.75/0.89 10639:1:0:[10542.0,1031.1]:: p(n4,n1,n5) -> % 1.75/0.89 11271:3:0:[11000.0,10258.0,10811.1,11266.1,10830.0,11267.2,10873.1,11268.5,11008.1,11269.7,11011.0,11270.8]:: -> p(n6,n4,n7),p(n6,n5,n7),p(n6,n7,n7) % 1.75/0.89 10640:1:0:[10543.0,1038.1]:: p(n4,n1,n3) -> % 1.75/0.89 10641:1:0:[10540.0,1039.0]:: p(n4,n9,n4) -> % 1.75/0.89 11265:2:0:[10999.0,10256.0,11004.1,11259.1,10841.1,11260.3,10861.0,11261.4,10893.1,11262.6,10908.1,11263.7,11010.0,11264.8]:: -> p(n6,n3,n5),p(n6,n6,n5) % 1.75/0.89 11258:3:0:[10794.1,10255.0,11003.1,11253.1,10822.1,11254.2,10867.1,11255.5,11007.0,11256.7,10935.0,11257.8]:: -> p(n6,n4,n4),p(n6,n5,n4),p(n6,n7,n4) % 1.75/0.89 11252:2:0:[10998.0,10254.0,11002.1,11246.1,10826.1,11247.2,10882.0,11248.5,11062.1,11249.6,11006.0,11250.7,10927.1,11251.8]:: -> p(n6,n4,n3),p(n6,n5,n3) % 1.75/0.89 10642:1:0:[10541.0,1051.0]:: p(n4,n3,n7) -> % 1.75/0.89 11245:4:0:[10802.0,10253.0,11001.1,11241.1,10902.0,11242.6,11005.0,11243.7,11009.0,11244.8]:: -> p(n6,n3,n2),p(n6,n4,n2),p(n6,n5,n2),p(n6,n6,n2) % 1.75/0.89 10643:1:0:[10541.0,1060.0]:: p(n4,n4,n7) -> % 1.75/0.89 11240:2:0:[10799.0,10251.0,11058.0,11234.1,10992.1,11235.2,10849.0,11236.3,10857.1,11237.4,10997.1,11238.6,10918.1,11239.8]:: -> p(n5,n6,n9),p(n5,n8,n9) % 1.75/0.89 10644:1:0:[10541.0,1069.0]:: p(n4,n5,n7) -> % 1.75/0.89 11233:5:0:[10991.1,10250.2,10996.1,11230.6,11063.0,11231.7,10931.0,11232.8]:: -> p(n5,n1,n8),p(n5,n2,n8),p(n5,n4,n8),p(n5,n5,n8),p(n5,n6,n8) % 1.75/0.89 10645:1:0:[10541.0,1078.0]:: p(n4,n6,n7) -> % 1.75/0.89 11229:4:0:[11055.1,10249.0,10809.1,11225.1,10828.0,11226.2,10872.1,11227.5,10995.1,11228.6]:: -> p(n5,n4,n7),p(n5,n5,n7),p(n5,n8,n7),p(n5,n9,n7) % 1.75/0.89 10646:1:0:[10541.0,1087.0]:: p(n4,n7,n7) -> % 1.75/0.89 11224:3:0:[10990.1,10248.2,10837.1,11219.3,10881.0,11220.5,10994.1,11221.6,10912.0,11222.7,11064.0,11223.8]:: -> p(n5,n1,n6),p(n5,n2,n6),p(n5,n5,n6) % 1.75/0.89 10647:1:0:[10542.0,1094.1]:: p(n4,n2,n5) -> % 1.75/0.89 10648:1:0:[10541.0,1096.0]:: p(n4,n8,n7) -> % 1.75/0.89 10649:1:0:[10543.0,1101.1]:: p(n4,n2,n3) -> % 1.75/0.89 11218:3:0:[10989.1,10247.2,10840.1,11213.3,10860.0,11214.4,10892.1,11215.6,10907.1,11216.7,11061.1,11217.8]:: -> p(n5,n1,n5),p(n5,n2,n5),p(n5,n6,n5) % 1.75/0.89 11212:3:0:[10793.1,10246.0,11054.1,11207.1,10821.1,11208.2,10866.1,11209.5,10993.1,11210.6,10932.0,11211.8]:: -> p(n5,n4,n4),p(n5,n5,n4),p(n5,n8,n4) % 1.75/0.89 10650:1:0:[10541.0,1105.0]:: p(n4,n9,n7) -> % 1.75/0.89 11206:6:0:[10800.0,10244.0,10988.0,11204.2,10900.0,11205.6]:: -> p(n5,n2,n2),p(n5,n4,n2),p(n5,n5,n2),p(n5,n6,n2),p(n5,n8,n2),p(n5,n9,n2) % 1.75/0.89 11203:2:0:[10795.0,10242.0,10980.1,11197.1,11056.0,11198.2,10847.0,11199.3,10856.1,11200.4,10984.1,11201.7,10917.1,11202.8]:: -> p(n4,n6,n9),p(n4,n7,n9) % 1.75/0.89 11196:4:0:[10976.1,10241.0,10979.1,11192.1,11060.0,11193.6,10983.1,11194.7,10928.0,11195.8]:: -> p(n4,n3,n8),p(n4,n4,n8),p(n4,n5,n8),p(n4,n6,n8) % 1.75/0.89 11191:2:0:[10975.1,10239.0,10978.0,11185.1,10836.1,11186.3,10880.0,11187.5,11059.0,11188.6,10909.0,11189.7,10987.1,11190.8]:: -> p(n4,n3,n6),p(n4,n5,n6) % 1.75/0.89 11184:4:0:[10798.0,10235.0,10977.0,11180.1,10898.0,11181.6,10982.0,11182.7,10986.0,11183.8]:: -> p(n4,n3,n2),p(n4,n4,n2),p(n4,n5,n2),p(n4,n6,n2) % 1.75/0.89 11179:2:0:[10785.1,10234.0,10810.0,11173.1,11057.0,11174.2,10848.0,11175.3,10897.0,11176.6,10981.0,11177.7,10985.0,11178.8]:: -> p(n4,n5,n1),p(n4,n6,n1) % 1.75/0.89 11172:5:0:[10964.1,10232.2,10970.0,11169.4,10974.1,11170.6,10926.0,11171.8]:: -> p(n3,n1,n8),p(n3,n2,n8),p(n3,n4,n8),p(n3,n6,n8),p(n3,n8,n8) % 1.75/0.89 11168:3:0:[10807.0,10231.1,10824.0,11163.2,11051.1,11164.3,10969.0,11165.4,10871.1,11166.5,10973.1,11167.6]:: -> p(n3,n1,n7),p(n3,n8,n7),p(n3,n9,n7) % 1.75/0.89 11162:3:0:[10963.1,10230.2,10835.1,11157.3,10968.0,11158.4,10879.0,11159.5,10972.1,11160.6,10906.0,11161.7]:: -> p(n3,n1,n6),p(n3,n2,n6),p(n3,n9,n6) % 1.75/0.89 10651:1:0:[10542.0,1148.1]:: p(n4,n3,n5) -> % 1.75/0.89 11156:4:0:[10820.0,10227.2,10967.0,11152.4,10878.0,11153.5,10971.0,11154.6,10925.0,11155.8]:: -> p(n3,n1,n3),p(n3,n2,n3),p(n3,n4,n3),p(n3,n8,n3) % 1.75/0.89 10652:1:0:[10543.0,1155.1]:: p(n4,n3,n3) -> % 1.75/0.89 11151:5:0:[10792.0,10226.0,10962.0,11148.2,10966.0,11149.4,10894.0,11150.6]:: -> p(n3,n2,n2),p(n3,n4,n2),p(n3,n6,n2),p(n3,n8,n2),p(n3,n9,n2) % 1.75/0.89 11147:3:0:[10784.1,10225.0,10808.0,11142.1,10961.0,11143.2,10846.0,11144.3,10965.0,11145.4,10891.0,11146.6]:: -> p(n3,n6,n1),p(n3,n8,n1),p(n3,n9,n1) % 1.75/0.89 11141:2:0:[10790.0,10224.0,10843.0,11135.3,10855.0,11136.4,10960.1,11137.5,11052.1,11138.6,11053.1,11139.7,10915.1,11140.8]:: -> p(n2,n2,n9),p(n2,n3,n9) % 1.75/0.89 11134:6:0:[10956.1,10223.3,10959.1,11132.5,10923.0,11133.8]:: -> p(n2,n1,n8),p(n2,n2,n8),p(n2,n3,n8),p(n2,n5,n8),p(n2,n7,n8),p(n2,n8,n8) % 1.75/0.89 11131:5:0:[10834.1,10221.3,11048.1,11128.4,10876.0,11129.5,10905.0,11130.7]:: -> p(n2,n1,n6),p(n2,n2,n6),p(n2,n3,n6),p(n2,n7,n6),p(n2,n9,n6) % 1.75/0.89 11127:2:0:[10789.0,10219.0,11047.0,11121.1,10818.0,11122.2,10955.0,11123.3,11050.1,11124.4,10864.1,11125.5,10924.0,11126.8]:: -> p(n2,n7,n4),p(n2,n8,n4) % 1.75/0.89 11120:5:0:[10819.0,10218.2,10954.0,11117.3,10874.0,11118.5,10922.0,11119.8]:: -> p(n2,n1,n3),p(n2,n2,n3),p(n2,n5,n3),p(n2,n7,n3),p(n2,n8,n3) % 1.75/0.89 11116:5:0:[10791.0,10217.0,10953.0,11113.3,10958.0,11114.5,10890.0,11115.6]:: -> p(n2,n2,n2),p(n2,n3,n2),p(n2,n5,n2),p(n2,n8,n2),p(n2,n9,n2) % 1.75/0.89 11112:3:0:[10783.1,10216.0,10806.0,11107.1,11046.1,11108.2,10844.0,11109.3,10957.0,11110.5,10889.0,11111.6]:: -> p(n2,n5,n1),p(n2,n8,n1),p(n2,n9,n1) % 1.75/0.89 11106:5:0:[10942.1,10214.0,10946.1,11103.3,10949.1,11104.5,10919.0,11105.8]:: -> p(n1,n2,n8),p(n1,n3,n8),p(n1,n5,n8),p(n1,n7,n8),p(n1,n8,n8) % 1.75/0.89 10653:1:0:[10542.0,1193.1]:: p(n4,n4,n5) -> % 1.75/0.89 11102:2:0:[10941.1,10213.0,10805.0,11096.1,10817.0,11097.2,10945.1,11098.3,11049.0,11099.4,10865.0,11100.5,10952.0,11101.8]:: -> p(n1,n7,n7),p(n1,n8,n7) % 1.75/0.89 10654:1:0:[10543.0,1200.1]:: p(n4,n4,n3) -> % 1.75/0.89 11095:2:0:[10940.1,10211.0,10833.0,11089.3,10854.0,11090.4,10948.1,11091.5,10887.0,11092.6,10904.0,11093.7,10951.0,11094.8]:: -> p(n1,n2,n5),p(n1,n3,n5) % 1.75/0.89 11088:4:0:[10939.1,10209.0,10816.0,11084.2,10944.0,11085.3,10869.0,11086.5,10916.0,11087.8]:: -> p(n1,n2,n3),p(n1,n5,n3),p(n1,n7,n3),p(n1,n8,n3) % 1.75/0.89 11083:4:0:[10788.0,10208.0,10943.0,11079.3,10947.0,11080.5,10888.0,11081.6,10950.0,11082.8]:: -> p(n1,n2,n2),p(n1,n3,n2),p(n1,n5,n2),p(n1,n8,n2) % 1.75/0.89 11078:1:0:[10558.0,10183.1]:: p(n8,n8,n4) -> % 1.75/0.89 10655:1:0:[10542.0,1229.1]:: p(n4,n5,n5) -> % 1.75/0.89 11077:1:0:[10558.0,10165.1]:: p(n8,n7,n4) -> % 1.75/0.89 10656:1:0:[10543.0,1236.1]:: p(n4,n5,n3) -> % 1.75/0.89 11076:1:0:[10558.0,10111.1]:: p(n7,n8,n4) -> % 1.75/0.89 10657:1:0:[10542.0,1256.1]:: p(n4,n6,n5) -> % 1.75/0.89 10658:1:0:[10543.0,1263.1]:: p(n4,n6,n3) -> % 1.75/0.89 10659:1:0:[10542.0,1274.1]:: p(n4,n7,n5) -> % 1.75/0.89 11075:1:0:[10552.0,10055.0]:: p(n8,n9,n2) -> % 1.75/0.89 10660:1:0:[10543.0,1281.1]:: p(n4,n7,n3) -> % 1.75/0.89 11074:1:0:[10552.0,10046.0]:: p(n8,n8,n2) -> % 1.75/0.89 11073:1:0:[10554.0,10038.0]:: p(n9,n5,n3) -> % 1.75/0.89 11072:1:0:[10557.0,10023.1]:: p(n8,n5,n6) -> % 1.75/0.89 10661:1:0:[10543.0,1290.1]:: p(n4,n8,n3) -> % 1.75/0.89 11071:1:0:[10556.0,10009.1]:: p(n8,n5,n1) -> % 1.75/0.89 10662:1:0:[10542.0,1292.0]:: p(n4,n9,n5) -> % 1.75/0.89 10663:1:0:[10544.0,1308.1]:: p(n5,n1,n3) -> % 1.75/0.89 11070:1:0:[10556.0,9973.1]:: p(n7,n6,n1) -> % 1.75/0.89 10664:1:0:[10545.0,1342.1]:: p(n5,n1,n1) -> % 1.75/0.89 11069:1:0:[10553.0,9963.1]:: p(n7,n6,n9) -> % 1.75/0.89 11068:1:0:[10554.0,9894.1]:: p(n7,n4,n3) -> % 1.75/0.89 10665:1:0:[10544.0,1371.1]:: p(n5,n2,n3) -> % 1.75/0.89 11067:1:0:[10555.0,9866.1]:: p(n8,n3,n2) -> % 1.75/0.89 10666:1:0:[10545.0,1405.1]:: p(n5,n2,n1) -> % 1.75/0.89 11066:1:0:[10555.0,9848.1]:: p(n8,n2,n2) -> % 1.75/0.89 10667:1:0:[10544.0,1434.0]:: p(n5,n4,n3) -> % 1.75/0.89 10668:1:0:[10544.0,1443.0]:: p(n5,n5,n3) -> % 1.75/0.89 10669:1:0:[10544.0,1452.0]:: p(n5,n6,n3) -> % 1.75/0.89 10670:1:0:[10545.0,1459.1]:: p(n5,n3,n1) -> % 1.75/0.89 10671:1:0:[10544.0,1461.0]:: p(n5,n7,n3) -> % 1.75/0.89 10672:1:0:[10544.0,1470.0]:: p(n5,n8,n3) -> % 1.75/0.89 10673:1:0:[10544.0,1479.0]:: p(n5,n9,n3) -> % 1.75/0.89 11065:1:0:[10550.0,9799.0]:: p(n8,n1,n7) -> % 1.75/0.89 10674:1:0:[10545.0,1504.1]:: p(n5,n4,n1) -> % 1.75/0.89 10675:1:0:[10545.0,1540.1]:: p(n5,n5,n1) -> % 1.75/0.89 10676:1:0:[10545.0,1567.1]:: p(n5,n6,n1) -> % 1.75/0.89 11064:1:0:[10548.0,9717.1]:: p(n5,n9,n6) -> % 1.75/0.89 11063:1:0:[10549.0,9701.1]:: p(n5,n8,n8) -> % 1.75/0.89 10677:1:0:[10545.0,1594.0]:: p(n5,n8,n1) -> % 1.75/0.89 10678:1:0:[10545.0,1603.0]:: p(n5,n9,n1) -> % 1.75/0.89 11062:1:0:[10543.0,9651.0]:: p(n6,n7,n3) -> % 1.75/0.89 11061:1:0:[10542.0,9608.0]:: p(n5,n9,n5) -> % 1.75/0.89 11060:1:0:[10549.0,9593.1]:: p(n4,n7,n8) -> % 1.75/0.89 10679:1:0:[10547.0,1621.1]:: p(n6,n1,n1) -> % 1.75/0.89 10680:1:0:[10546.0,1629.0]:: p(n6,n2,n9) -> % 1.75/0.89 11059:1:0:[10548.0,9582.1]:: p(n4,n7,n6) -> % 1.75/0.89 10681:1:0:[10546.0,1638.0]:: p(n6,n3,n9) -> % 1.75/0.89 10682:1:0:[10546.0,1647.0]:: p(n6,n4,n9) -> % 1.75/0.89 10683:1:0:[10546.0,1656.0]:: p(n6,n5,n9) -> % 1.75/0.89 10684:1:0:[10546.0,1665.0]:: p(n6,n6,n9) -> % 1.75/0.89 10685:1:0:[10546.0,1674.0]:: p(n6,n7,n9) -> % 1.75/0.89 10686:1:0:[10548.0,1680.1]:: p(n6,n1,n6) -> % 1.75/0.89 10687:1:0:[10546.0,1683.0]:: p(n6,n8,n9) -> % 1.75/0.89 10688:1:0:[10549.0,1691.1]:: p(n6,n1,n8) -> % 1.75/0.89 10689:1:0:[10546.0,1692.0]:: p(n6,n9,n9) -> % 1.75/0.89 10690:1:0:[10547.0,1693.0]:: p(n6,n3,n1) -> % 1.75/0.89 10691:1:0:[10547.0,1702.0]:: p(n6,n4,n1) -> % 1.75/0.89 10692:1:0:[10547.0,1711.0]:: p(n6,n5,n1) -> % 1.75/0.89 10693:1:0:[10547.0,1720.0]:: p(n6,n6,n1) -> % 1.75/0.89 10694:1:0:[10547.0,1729.0]:: p(n6,n7,n1) -> % 1.75/0.89 10695:1:0:[10547.0,1738.0]:: p(n6,n8,n1) -> % 1.75/0.89 10696:1:0:[10548.0,1743.1]:: p(n6,n2,n6) -> % 1.75/0.89 10697:1:0:[10547.0,1747.0]:: p(n6,n9,n1) -> % 1.75/0.89 10698:1:0:[10549.0,1754.1]:: p(n6,n2,n8) -> % 1.75/0.89 10699:1:0:[10548.0,1797.1]:: p(n6,n3,n6) -> % 1.75/0.89 10700:1:0:[10549.0,1808.1]:: p(n6,n3,n8) -> % 1.75/0.89 11058:1:0:[10546.0,9369.1]:: p(n5,n2,n9) -> % 1.75/0.89 10701:1:0:[10548.0,1842.1]:: p(n6,n4,n6) -> % 1.75/0.89 11057:1:0:[10547.0,9334.1]:: p(n4,n3,n1) -> % 1.75/0.89 11056:1:0:[10546.0,9333.1]:: p(n4,n3,n9) -> % 1.75/0.89 10702:1:0:[10549.0,1853.1]:: p(n6,n4,n8) -> % 1.75/0.89 11055:1:0:[10541.0,9277.0]:: p(n5,n1,n7) -> % 1.75/0.89 10703:1:0:[10548.0,1878.1]:: p(n6,n5,n6) -> % 1.75/0.89 11054:1:0:[10540.0,9238.0]:: p(n5,n2,n4) -> % 1.75/0.89 10704:1:0:[10549.0,1889.1]:: p(n6,n5,n8) -> % 1.75/0.89 10705:1:0:[10548.0,1905.1]:: p(n6,n6,n6) -> % 1.75/0.89 11053:1:0:[10534.0,9162.0]:: p(n2,n8,n9) -> % 1.75/0.89 11052:1:0:[10534.0,9153.0]:: p(n2,n7,n9) -> % 1.75/0.89 10706:1:0:[10549.0,1916.1]:: p(n6,n6,n8) -> % 1.75/0.89 10707:1:0:[10548.0,1923.1]:: p(n6,n7,n6) -> % 1.75/0.89 10708:1:0:[10549.0,1934.1]:: p(n6,n7,n8) -> % 1.75/0.89 10709:1:0:[10548.0,1941.0]:: p(n6,n9,n6) -> % 1.75/0.89 10710:1:0:[10549.0,1943.1]:: p(n6,n8,n8) -> % 1.75/0.89 10711:1:0:[10550.0,1960.1]:: p(n7,n1,n7) -> % 1.75/0.89 10712:1:0:[10551.0,1976.1]:: p(n7,n1,n5) -> % 1.75/0.89 11051:1:0:[10536.0,9061.0]:: p(n3,n4,n7) -> % 1.75/0.89 10713:1:0:[10552.0,1991.1]:: p(n7,n1,n2) -> % 1.75/0.89 11050:1:0:[10533.0,8995.0]:: p(n2,n5,n4) -> % 1.75/0.89 10714:1:0:[10550.0,2023.1]:: p(n7,n2,n7) -> % 1.75/0.89 10715:1:0:[10551.0,2039.1]:: p(n7,n2,n5) -> % 1.75/0.89 10716:1:0:[10552.0,2054.1]:: p(n7,n2,n2) -> % 1.75/0.89 11049:1:0:[10536.0,8962.1]:: p(n1,n5,n7) -> % 1.75/0.89 11048:1:0:[10532.0,8916.0]:: p(n2,n5,n6) -> % 1.75/0.89 11047:1:0:[10537.0,8887.1]:: p(n2,n2,n4) -> % 1.75/0.89 10717:1:0:[10550.0,2086.0]:: p(n7,n4,n7) -> % 1.75/0.89 10718:1:0:[10551.0,2093.1]:: p(n7,n3,n5) -> % 1.75/0.89 10719:1:0:[10550.0,2095.0]:: p(n7,n5,n7) -> % 1.75/0.89 10720:1:0:[10550.0,2104.0]:: p(n7,n6,n7) -> % 1.75/0.89 10721:1:0:[10552.0,2108.1]:: p(n7,n3,n2) -> % 1.75/0.89 10722:1:0:[10550.0,2113.0]:: p(n7,n7,n7) -> % 1.75/0.89 10723:1:0:[10550.0,2122.0]:: p(n7,n8,n7) -> % 1.75/0.89 10724:1:0:[10550.0,2131.0]:: p(n7,n9,n7) -> % 1.75/0.89 10725:1:0:[10551.0,2138.1]:: p(n7,n4,n5) -> % 1.75/0.89 10726:1:0:[10552.0,2153.1]:: p(n7,n4,n2) -> % 1.75/0.89 10727:1:0:[10551.0,2183.0]:: p(n7,n6,n5) -> % 1.75/0.89 10728:1:0:[10552.0,2189.1]:: p(n7,n5,n2) -> % 1.75/0.89 10729:1:0:[10551.0,2192.0]:: p(n7,n7,n5) -> % 1.75/0.89 11046:1:0:[10531.0,8758.0]:: p(n2,n3,n1) -> % 1.75/0.89 11045:1:0:[10558.0,8736.0]:: p(n9,n9,n7) -> % 1.75/0.89 10730:1:0:[10551.0,2201.0]:: p(n7,n8,n5) -> % 1.75/0.89 11044:1:0:[10558.0,8734.0]:: p(n9,n9,n5) -> % 1.75/0.89 10731:1:0:[10551.0,2210.0]:: p(n7,n9,n5) -> % 1.75/0.89 10732:1:0:[10552.0,2216.1]:: p(n7,n6,n2) -> % 1.75/0.89 10733:1:0:[10552.0,2243.0]:: p(n7,n8,n2) -> % 1.75/0.89 10734:1:0:[10552.0,2252.0]:: p(n7,n9,n2) -> % 1.75/0.89 11043:1:0:[10557.0,8637.0]:: p(n9,n6,n9) -> % 1.75/0.89 11042:1:0:[10557.0,8636.0]:: p(n9,n6,n8) -> % 1.75/0.89 11041:1:0:[10557.0,8631.1]:: p(n9,n6,n5) -> % 1.75/0.89 10735:1:0:[10553.0,2295.1]:: p(n8,n1,n9) -> % 1.75/0.89 10736:1:0:[10554.0,2307.1]:: p(n8,n1,n3) -> % 1.75/0.89 11040:1:0:[10556.0,8539.0]:: p(n9,n4,n8) -> % 1.75/0.89 11039:1:0:[10556.0,8538.0]:: p(n9,n4,n7) -> % 1.75/0.89 11038:1:0:[10556.0,8534.0]:: p(n9,n4,n3) -> % 1.75/0.89 10737:1:0:[10553.0,2358.1]:: p(n8,n2,n9) -> % 1.75/0.89 10738:1:0:[10554.0,2370.1]:: p(n8,n2,n3) -> % 1.75/0.89 11037:1:0:[10555.0,8438.0]:: p(n9,n1,n8) -> % 1.75/0.89 11036:1:0:[10555.0,8437.0]:: p(n9,n1,n7) -> % 1.75/0.89 11035:1:0:[10555.0,8435.0]:: p(n9,n1,n5) -> % 1.75/0.89 10739:1:0:[10553.0,2412.1]:: p(n8,n3,n9) -> % 1.75/0.89 11034:1:0:[10555.0,8433.0]:: p(n9,n1,n3) -> % 1.75/0.89 10740:1:0:[10554.0,2424.1]:: p(n8,n3,n3) -> % 1.75/0.89 10741:1:0:[10553.0,2466.0]:: p(n8,n5,n9) -> % 1.75/0.89 10742:1:0:[10554.0,2469.1]:: p(n8,n4,n3) -> % 1.75/0.89 10743:1:0:[10553.0,2475.0]:: p(n8,n6,n9) -> % 1.75/0.89 10744:1:0:[10553.0,2484.0]:: p(n8,n7,n9) -> % 1.75/0.89 10745:1:0:[10553.0,2493.0]:: p(n8,n8,n9) -> % 1.75/0.89 10746:1:0:[10553.0,2502.0]:: p(n8,n9,n9) -> % 1.75/0.89 10747:1:0:[10554.0,2505.1]:: p(n8,n5,n3) -> % 1.75/0.89 10748:1:0:[10554.0,2541.0]:: p(n8,n7,n3) -> % 1.75/0.89 10749:1:0:[10554.0,2550.0]:: p(n8,n8,n3) -> % 1.75/0.89 10750:1:0:[10554.0,2559.0]:: p(n8,n9,n3) -> % 1.75/0.89 10751:1:0:[10555.0,2594.0]:: p(n9,n2,n2) -> % 1.75/0.89 10752:1:0:[10555.0,2603.0]:: p(n9,n3,n2) -> % 1.75/0.89 10753:1:0:[10556.0,2611.1]:: p(n9,n1,n1) -> % 1.75/0.89 10754:1:0:[10555.0,2612.0]:: p(n9,n4,n2) -> % 1.75/0.89 11033:1:0:[10554.0,8300.0]:: p(n8,n6,n8) -> % 1.75/0.89 10755:1:0:[10555.0,2621.0]:: p(n9,n5,n2) -> % 1.75/0.89 11032:1:0:[10554.0,8297.0]:: p(n8,n6,n5) -> % 1.75/0.89 10756:1:0:[10555.0,2630.0]:: p(n9,n6,n2) -> % 1.75/0.89 10757:1:0:[10557.0,2634.1]:: p(n9,n1,n6) -> % 1.75/0.89 11031:1:0:[10554.0,8289.1]:: p(n8,n6,n2) -> % 1.75/0.89 10758:1:0:[10555.0,2639.0]:: p(n9,n7,n2) -> % 1.75/0.89 11030:1:0:[10554.0,8282.1]:: p(n8,n6,n1) -> % 1.75/0.89 10759:1:0:[10555.0,2648.0]:: p(n9,n8,n2) -> % 1.75/0.89 10760:1:0:[10555.0,2657.0]:: p(n9,n9,n2) -> % 1.75/0.89 10761:1:0:[10558.0,2659.1]:: p(n9,n1,n4) -> % 1.75/0.89 10762:1:0:[10556.0,2674.1]:: p(n9,n2,n1) -> % 1.75/0.89 10763:1:0:[10557.0,2697.1]:: p(n9,n2,n6) -> % 1.75/0.89 11029:1:0:[10553.0,8244.1]:: p(n8,n4,n8) -> % 1.75/0.89 11028:1:0:[10553.0,8243.1]:: p(n8,n4,n7) -> % 1.75/0.89 10764:1:0:[10558.0,2722.1]:: p(n9,n2,n4) -> % 1.75/0.89 10765:1:0:[10556.0,2728.1]:: p(n9,n3,n1) -> % 1.75/0.89 11027:1:0:[10553.0,8234.1]:: p(n8,n4,n4) -> % 1.75/0.89 11026:1:0:[10553.0,8223.1]:: p(n8,n4,n2) -> % 1.75/0.89 10766:1:0:[10557.0,2751.1]:: p(n9,n3,n6) -> % 1.75/0.89 10767:1:0:[10558.0,2776.1]:: p(n9,n3,n4) -> % 1.75/0.89 10768:1:0:[10556.0,2782.0]:: p(n9,n5,n1) -> % 1.75/0.89 10769:1:0:[10556.0,2791.0]:: p(n9,n6,n1) -> % 1.75/0.89 10770:1:0:[10557.0,2796.1]:: p(n9,n4,n6) -> % 1.75/0.89 10771:1:0:[10556.0,2800.0]:: p(n9,n7,n1) -> % 1.75/0.89 10772:1:0:[10556.0,2809.0]:: p(n9,n8,n1) -> % 1.75/0.89 10773:1:0:[10556.0,2818.0]:: p(n9,n9,n1) -> % 1.75/0.89 10774:1:0:[10558.0,2821.1]:: p(n9,n4,n4) -> % 1.75/0.89 10775:1:0:[10557.0,2832.1]:: p(n9,n5,n6) -> % 1.75/0.89 10776:1:0:[10558.0,2857.1]:: p(n9,n5,n4) -> % 1.75/0.89 10777:1:0:[10557.0,2868.0]:: p(n9,n7,n6) -> % 1.75/0.89 10778:1:0:[10557.0,2877.0]:: p(n9,n8,n6) -> % 1.75/0.89 10779:1:0:[10558.0,2884.1]:: p(n9,n6,n4) -> % 1.75/0.89 10780:1:0:[10557.0,2886.0]:: p(n9,n9,n6) -> % 1.75/0.89 10781:1:0:[10558.0,2902.1]:: p(n9,n7,n4) -> % 1.75/0.89 11025:1:0:[10552.0,8007.0]:: p(n7,n7,n9) -> % 1.75/0.89 11024:1:0:[10552.0,8006.0]:: p(n7,n7,n8) -> % 1.75/0.89 11023:1:0:[10552.0,8004.0]:: p(n7,n7,n6) -> % 1.75/0.89 10782:1:0:[10558.0,2911.1]:: p(n9,n8,n4) -> % 1.75/0.89 11022:1:0:[10552.0,8002.0]:: p(n7,n7,n4) -> % 1.75/0.89 10783:1:0:[10531.0,2917.0]:: p(n2,n1,n1) -> % 1.75/0.89 11021:1:0:[10552.0,8001.0]:: p(n7,n7,n3) -> % 1.75/0.89 11020:1:0:[10551.0,7949.0]:: p(n7,n5,n8) -> % 1.75/0.89 10784:1:0:[10531.0,2926.0]:: p(n3,n1,n1) -> % 1.75/0.89 11019:1:0:[10551.0,7947.0]:: p(n7,n5,n6) -> % 1.75/0.89 11018:1:0:[10551.0,7942.1]:: p(n7,n5,n4) -> % 1.75/0.89 11017:1:0:[10551.0,7937.1]:: p(n7,n5,n3) -> % 1.75/0.89 10785:1:0:[10531.0,2935.0]:: p(n4,n1,n1) -> % 1.75/0.89 11016:1:0:[10551.0,7924.1]:: p(n7,n5,n1) -> % 1.75/0.89 11015:1:0:[10550.0,7883.0]:: p(n7,n3,n9) -> % 1.75/0.89 11014:1:0:[10550.0,7882.0]:: p(n7,n3,n8) -> % 1.75/0.89 11013:1:0:[10550.0,7879.1]:: p(n7,n3,n6) -> % 1.75/0.89 11012:1:0:[10550.0,7854.1]:: p(n7,n3,n1) -> % 1.75/0.89 10786:1:0:[10531.0,2962.0]:: p(n7,n1,n1) -> % 1.75/0.89 10787:1:0:[10531.0,2971.0]:: p(n8,n1,n1) -> % 1.75/0.89 11011:1:0:[10549.0,7774.1]:: p(n6,n9,n7) -> % 1.75/0.89 11010:1:0:[10549.0,7769.1]:: p(n6,n9,n5) -> % 1.75/0.89 10788:1:0:[10555.0,2981.1]:: p(n1,n1,n2) -> % 1.75/0.89 11009:1:0:[10549.0,7754.1]:: p(n6,n9,n2) -> % 1.75/0.89 11008:1:0:[10548.0,7735.0]:: p(n6,n8,n7) -> % 1.75/0.89 11007:1:0:[10548.0,7727.1]:: p(n6,n8,n4) -> % 1.75/0.89 11006:1:0:[10548.0,7722.1]:: p(n6,n8,n3) -> % 1.75/0.89 11005:1:0:[10548.0,7716.1]:: p(n6,n8,n2) -> % 1.75/0.89 10789:1:0:[10540.0,3001.1]:: p(n2,n1,n4) -> % 1.75/0.89 10790:1:0:[10546.0,3024.1]:: p(n2,n1,n9) -> % 1.75/0.89 11004:1:0:[10547.0,7492.0]:: p(n6,n2,n5) -> % 1.75/0.89 11003:1:0:[10547.0,7491.0]:: p(n6,n2,n4) -> % 1.75/0.89 11002:1:0:[10547.0,7490.0]:: p(n6,n2,n3) -> % 1.75/0.89 11001:1:0:[10547.0,7489.0]:: p(n6,n2,n2) -> % 1.75/0.89 11000:1:0:[10546.0,7487.1]:: p(n6,n1,n7) -> % 1.75/0.89 10999:1:0:[10546.0,7482.1]:: p(n6,n1,n5) -> % 1.75/0.89 10998:1:0:[10546.0,7473.1]:: p(n6,n1,n3) -> % 1.75/0.89 10791:1:0:[10555.0,3044.1]:: p(n2,n1,n2) -> % 1.75/0.89 10997:1:0:[10545.0,7352.0]:: p(n5,n7,n9) -> % 1.75/0.89 10996:1:0:[10545.0,7351.0]:: p(n5,n7,n8) -> % 1.75/0.89 10995:1:0:[10545.0,7350.0]:: p(n5,n7,n7) -> % 1.75/0.89 10994:1:0:[10545.0,7349.0]:: p(n5,n7,n6) -> % 1.75/0.89 10993:1:0:[10545.0,7347.0]:: p(n5,n7,n4) -> % 1.75/0.89 10792:1:0:[10555.0,3098.1]:: p(n3,n1,n2) -> % 0.70/0.90 10793:1:0:[10540.0,3109.0]:: p(n5,n1,n4) -> % 0.70/0.90 10794:1:0:[10540.0,3118.0]:: p(n6,n1,n4) -> % 0.70/0.90 10992:1:0:[10544.0,7221.0]:: p(n5,n3,n9) -> % 0.70/0.90 10991:1:0:[10544.0,7220.0]:: p(n5,n3,n8) -> % 0.70/0.90 10990:1:0:[10544.0,7218.0]:: p(n5,n3,n6) -> % 0.70/0.90 10989:1:0:[10544.0,7217.0]:: p(n5,n3,n5) -> % 0.70/0.90 10795:1:0:[10546.0,3123.1]:: p(n4,n1,n9) -> % 0.70/0.90 10988:1:0:[10544.0,7209.1]:: p(n5,n3,n2) -> % 0.70/0.90 10796:1:0:[10540.0,3127.0]:: p(n7,n1,n4) -> % 0.70/0.90 10797:1:0:[10540.0,3136.0]:: p(n8,n1,n4) -> % 0.70/0.90 10798:1:0:[10555.0,3143.1]:: p(n4,n1,n2) -> % 0.70/0.90 10987:1:0:[10543.0,7110.0]:: p(n4,n9,n6) -> % 0.70/0.90 10799:1:0:[10546.0,3159.1]:: p(n5,n1,n9) -> % 0.70/0.90 10986:1:0:[10543.0,7101.1]:: p(n4,n9,n2) -> % 0.70/0.90 10985:1:0:[10543.0,7094.1]:: p(n4,n9,n1) -> % 0.70/0.90 10984:1:0:[10542.0,7086.0]:: p(n4,n8,n9) -> % 0.70/0.90 10983:1:0:[10542.0,7085.0]:: p(n4,n8,n8) -> % 0.70/0.90 10982:1:0:[10542.0,7067.1]:: p(n4,n8,n2) -> % 0.70/0.90 10981:1:0:[10542.0,7060.1]:: p(n4,n8,n1) -> % 0.70/0.90 10800:1:0:[10555.0,3179.1]:: p(n5,n1,n2) -> % 0.70/0.90 10801:1:0:[10546.0,3195.0]:: p(n7,n1,n9) -> % 0.70/0.90 10802:1:0:[10555.0,3206.1]:: p(n6,n1,n2) -> % 0.70/0.90 10803:1:0:[10546.0,3213.0]:: p(n9,n1,n9) -> % 0.70/0.90 10980:1:0:[10541.0,6875.0]:: p(n4,n2,n9) -> % 0.70/0.90 10979:1:0:[10541.0,6874.0]:: p(n4,n2,n8) -> % 0.70/0.90 10978:1:0:[10541.0,6871.1]:: p(n4,n2,n6) -> % 0.70/0.90 10977:1:0:[10541.0,6853.1]:: p(n4,n2,n2) -> % 0.70/0.90 10976:1:0:[10540.0,6829.0]:: p(n4,n1,n8) -> % 0.70/0.90 10975:1:0:[10540.0,6827.0]:: p(n4,n1,n6) -> % 0.70/0.90 10804:1:0:[10555.0,3233.1]:: p(n8,n1,n2) -> % 0.70/0.90 10974:1:0:[10539.0,6725.0]:: p(n3,n7,n8) -> % 0.70/0.90 10973:1:0:[10539.0,6724.0]:: p(n3,n7,n7) -> % 0.70/0.90 10972:1:0:[10539.0,6723.0]:: p(n3,n7,n6) -> % 0.70/0.90 10971:1:0:[10539.0,6713.1]:: p(n3,n7,n3) -> % 0.70/0.90 10970:1:0:[10538.0,6660.1]:: p(n3,n5,n8) -> % 0.70/0.90 10969:1:0:[10538.0,6659.1]:: p(n3,n5,n7) -> % 0.70/0.90 10968:1:0:[10538.0,6657.1]:: p(n3,n5,n6) -> % 0.70/0.90 10805:1:0:[10541.0,3265.1]:: p(n1,n2,n7) -> % 0.70/0.90 10967:1:0:[10538.0,6645.1]:: p(n3,n5,n3) -> % 0.70/0.90 10966:1:0:[10538.0,6639.1]:: p(n3,n5,n2) -> % 0.70/0.90 10965:1:0:[10538.0,6632.1]:: p(n3,n5,n1) -> % 0.70/0.90 10964:1:0:[10537.0,6577.0]:: p(n3,n3,n8) -> % 0.70/0.90 10963:1:0:[10537.0,6575.0]:: p(n3,n3,n6) -> % 0.70/0.90 10962:1:0:[10537.0,6562.1]:: p(n3,n3,n2) -> % 0.70/0.90 10961:1:0:[10537.0,6555.1]:: p(n3,n3,n1) -> % 0.70/0.90 10806:1:0:[10547.0,3340.1]:: p(n2,n2,n1) -> % 0.70/0.90 10807:1:0:[10541.0,3382.1]:: p(n3,n2,n7) -> % 0.70/0.90 10960:1:0:[10536.0,6371.0]:: p(n2,n6,n9) -> % 0.70/0.90 10959:1:0:[10536.0,6370.0]:: p(n2,n6,n8) -> % 0.70/0.90 10958:1:0:[10536.0,6349.1]:: p(n2,n6,n2) -> % 0.70/0.90 10957:1:0:[10536.0,6342.1]:: p(n2,n6,n1) -> % 0.70/0.90 10808:1:0:[10547.0,3394.1]:: p(n3,n2,n1) -> % 0.70/0.90 10956:1:0:[10535.0,6293.0]:: p(n2,n4,n8) -> % 0.70/0.90 10955:1:0:[10535.0,6286.1]:: p(n2,n4,n4) -> % 0.70/0.90 10954:1:0:[10535.0,6281.1]:: p(n2,n4,n3) -> % 0.70/0.90 10953:1:0:[10535.0,6275.1]:: p(n2,n4,n2) -> % 0.70/0.90 10809:1:0:[10541.0,3436.0]:: p(n5,n2,n7) -> % 0.70/0.90 10810:1:0:[10547.0,3439.1]:: p(n4,n2,n1) -> % 0.70/0.90 10811:1:0:[10541.0,3445.0]:: p(n6,n2,n7) -> % 0.70/0.90 10812:1:0:[10541.0,3463.0]:: p(n8,n2,n7) -> % 0.70/0.90 10952:1:0:[10534.0,6155.1]:: p(n1,n9,n7) -> % 0.70/0.90 10951:1:0:[10534.0,6150.1]:: p(n1,n9,n5) -> % 0.70/0.90 10813:1:0:[10541.0,3472.0]:: p(n9,n2,n7) -> % 0.70/0.90 10950:1:0:[10534.0,6135.1]:: p(n1,n9,n2) -> % 0.70/0.90 10949:1:0:[10533.0,6037.0]:: p(n1,n6,n8) -> % 0.70/0.90 10948:1:0:[10533.0,6034.0]:: p(n1,n6,n5) -> % 0.70/0.90 10947:1:0:[10533.0,6022.1]:: p(n1,n6,n2) -> % 0.70/0.90 10814:1:0:[10547.0,3511.0]:: p(n7,n2,n1) -> % 0.70/0.90 10946:1:0:[10532.0,5972.0]:: p(n1,n4,n8) -> % 0.70/0.90 10945:1:0:[10532.0,5971.0]:: p(n1,n4,n7) -> % 0.70/0.90 10944:1:0:[10532.0,5958.1]:: p(n1,n4,n3) -> % 0.70/0.90 10943:1:0:[10532.0,5952.1]:: p(n1,n4,n2) -> % 0.70/0.90 10815:1:0:[10547.0,3520.0]:: p(n8,n2,n1) -> % 0.70/0.90 10942:1:0:[10531.0,5839.0]:: p(n1,n1,n8) -> % 0.70/0.90 10941:1:0:[10531.0,5838.0]:: p(n1,n1,n7) -> % 0.70/0.90 10940:1:0:[10531.0,5836.0]:: p(n1,n1,n5) -> % 0.70/0.90 10939:1:0:[10531.0,5834.0]:: p(n1,n1,n3) -> % 0.70/0.90 10938:1:0:[10558.0,5827.1]:: p(n8,n9,n4) -> % 0.70/0.90 10937:1:0:[10558.0,5818.1]:: p(n7,n9,n4) -> % 0.70/0.90 10936:1:0:[10549.0,5804.0]:: p(n9,n9,n8) -> % 0.70/0.90 10935:1:0:[10558.0,5800.1]:: p(n6,n9,n4) -> % 0.70/0.90 10934:1:0:[10549.0,5795.0]:: p(n8,n9,n8) -> % 0.70/0.90 10933:1:0:[10549.0,5786.0]:: p(n7,n9,n8) -> % 0.70/0.90 10932:1:0:[10558.0,5773.1]:: p(n5,n9,n4) -> % 0.70/0.90 10931:1:0:[10549.0,5750.1]:: p(n5,n9,n8) -> % 0.70/0.90 10930:1:0:[10543.0,5736.0]:: p(n9,n9,n3) -> % 0.70/0.90 10816:1:0:[10544.0,3594.1]:: p(n1,n3,n3) -> % 0.70/0.90 10929:1:0:[10543.0,5718.0]:: p(n7,n9,n3) -> % 0.70/0.90 10928:1:0:[10549.0,5714.1]:: p(n4,n9,n8) -> % 0.70/0.90 10927:1:0:[10543.0,5709.0]:: p(n6,n9,n3) -> % 0.70/0.90 10817:1:0:[10550.0,3616.1]:: p(n1,n3,n7) -> % 0.70/0.90 10926:1:0:[10549.0,5669.1]:: p(n3,n9,n8) -> % 0.70/0.90 10925:1:0:[10543.0,5646.1]:: p(n3,n9,n3) -> % 0.70/0.90 10924:1:0:[10558.0,5638.1]:: p(n2,n9,n4) -> % 0.70/0.90 10818:1:0:[10537.0,3640.1]:: p(n2,n3,n4) -> % 0.70/0.90 10923:1:0:[10549.0,5615.1]:: p(n2,n9,n8) -> % 0.70/0.90 10819:1:0:[10544.0,3657.1]:: p(n2,n3,n3) -> % 0.70/0.90 10922:1:0:[10543.0,5592.1]:: p(n2,n9,n3) -> % 0.70/0.90 10921:1:0:[10534.0,5580.0]:: p(n9,n9,n9) -> % 0.70/0.90 10920:1:0:[10534.0,5562.0]:: p(n7,n9,n9) -> % 0.70/0.90 10919:1:0:[10549.0,5552.1]:: p(n1,n9,n8) -> % 0.70/0.90 10918:1:0:[10534.0,5544.0]:: p(n5,n9,n9) -> % 0.70/0.90 10917:1:0:[10534.0,5535.0]:: p(n4,n9,n9) -> % 0.70/0.90 10916:1:0:[10543.0,5529.1]:: p(n1,n9,n3) -> % 0.70/0.90 10820:1:0:[10544.0,3711.1]:: p(n3,n3,n3) -> % 0.70/0.90 10821:1:0:[10537.0,3712.0]:: p(n5,n3,n4) -> % 0.70/0.90 10822:1:0:[10537.0,3721.0]:: p(n6,n3,n4) -> % 0.70/0.90 10915:1:0:[10534.0,5517.0]:: p(n2,n9,n9) -> % 0.70/0.90 10823:1:0:[10537.0,3730.0]:: p(n7,n3,n4) -> % 0.70/0.90 10824:1:0:[10550.0,3733.1]:: p(n3,n3,n7) -> % 0.70/0.90 10825:1:0:[10537.0,3739.0]:: p(n8,n3,n4) -> % 0.70/0.90 10914:1:0:[10548.0,5469.0]:: p(n8,n8,n6) -> % 0.70/0.90 10913:1:0:[10548.0,5460.0]:: p(n7,n8,n6) -> % 0.70/0.90 10912:1:0:[10548.0,5424.1]:: p(n5,n8,n6) -> % 0.70/0.90 10911:1:0:[10542.0,5414.0]:: p(n9,n8,n5) -> % 0.70/0.90 10910:1:0:[10542.0,5405.0]:: p(n8,n8,n5) -> % 0.70/0.90 10909:1:0:[10548.0,5388.1]:: p(n4,n8,n6) -> % 0.70/0.90 10908:1:0:[10542.0,5387.0]:: p(n6,n8,n5) -> % 0.70/0.90 10826:1:0:[10544.0,3801.0]:: p(n6,n3,n3) -> % 0.70/0.90 10907:1:0:[10542.0,5378.0]:: p(n5,n8,n5) -> % 0.70/0.90 10827:1:0:[10544.0,3810.0]:: p(n7,n3,n3) -> % 0.70/0.90 10828:1:0:[10550.0,3814.1]:: p(n5,n3,n7) -> % 0.70/0.90 10906:1:0:[10548.0,5343.1]:: p(n3,n8,n6) -> % 0.70/0.90 10829:1:0:[10544.0,3828.0]:: p(n9,n3,n3) -> % 0.70/0.90 10830:1:0:[10550.0,3841.1]:: p(n6,n3,n7) -> % 0.70/0.90 10905:1:0:[10548.0,5289.1]:: p(n2,n8,n6) -> % 0.70/0.90 10831:1:0:[10550.0,3868.0]:: p(n8,n3,n7) -> % 0.70/0.90 10832:1:0:[10550.0,3877.0]:: p(n9,n3,n7) -> % 0.70/0.90 10833:1:0:[10535.0,3893.1]:: p(n1,n4,n5) -> % 0.70/0.90 10834:1:0:[10532.0,3894.0]:: p(n2,n4,n6) -> % 0.70/0.90 10835:1:0:[10532.0,3903.0]:: p(n3,n4,n6) -> % 0.70/0.90 10836:1:0:[10532.0,3912.0]:: p(n4,n4,n6) -> % 0.70/0.90 10904:1:0:[10542.0,5207.1]:: p(n1,n8,n5) -> % 0.70/0.90 10837:1:0:[10532.0,3921.0]:: p(n5,n4,n6) -> % 0.70/0.90 10838:1:0:[10532.0,3939.0]:: p(n7,n4,n6) -> % 0.70/0.90 10903:1:0:[10552.0,5159.0]:: p(n8,n7,n2) -> % 0.70/0.90 10839:1:0:[10532.0,3948.0]:: p(n8,n4,n6) -> % 0.70/0.90 10902:1:0:[10552.0,5132.1]:: p(n6,n7,n2) -> % 0.70/0.90 10901:1:0:[10545.0,5113.0]:: p(n8,n7,n1) -> % 0.70/0.90 10900:1:0:[10552.0,5105.1]:: p(n5,n7,n2) -> % 0.70/0.90 10899:1:0:[10545.0,5104.0]:: p(n7,n7,n1) -> % 0.70/0.90 10840:1:0:[10535.0,3983.0]:: p(n5,n4,n5) -> % 0.70/0.90 10841:1:0:[10535.0,3992.0]:: p(n6,n4,n5) -> % 0.70/0.90 10898:1:0:[10552.0,5069.1]:: p(n4,n7,n2) -> % 0.70/0.90 10842:1:0:[10535.0,4010.0]:: p(n8,n4,n5) -> % 0.70/0.90 10897:1:0:[10545.0,5050.1]:: p(n4,n7,n1) -> % 0.70/0.90 10843:1:0:[10553.0,4014.1]:: p(n2,n4,n9) -> % 0.70/0.90 10844:1:0:[10556.0,4015.1]:: p(n2,n4,n1) -> % 0.70/0.90 10845:1:0:[10535.0,4019.0]:: p(n9,n4,n5) -> % 0.70/0.90 10896:1:0:[10539.0,5045.0]:: p(n9,n7,n5) -> % 0.70/0.90 10895:1:0:[10539.0,5036.0]:: p(n8,n7,n5) -> % 0.70/0.90 10894:1:0:[10552.0,5024.1]:: p(n3,n7,n2) -> % 0.70/0.90 10893:1:0:[10539.0,5018.0]:: p(n6,n7,n5) -> % 0.70/0.90 10892:1:0:[10539.0,5009.0]:: p(n5,n7,n5) -> % 0.70/0.90 10891:1:0:[10545.0,5005.1]:: p(n3,n7,n1) -> % 0.70/0.90 10846:1:0:[10556.0,4069.1]:: p(n3,n4,n1) -> % 0.70/0.90 10890:1:0:[10552.0,4970.1]:: p(n2,n7,n2) -> % 0.70/0.90 10889:1:0:[10545.0,4951.1]:: p(n2,n7,n1) -> % 0.70/0.90 10847:1:0:[10553.0,4113.1]:: p(n4,n4,n9) -> % 0.70/0.90 10848:1:0:[10556.0,4114.1]:: p(n4,n4,n1) -> % 0.70/0.90 10888:1:0:[10552.0,4907.1]:: p(n1,n7,n2) -> % 0.70/0.90 10887:1:0:[10539.0,4874.1]:: p(n1,n7,n5) -> % 0.70/0.90 10886:1:0:[10557.0,4857.1]:: p(n8,n6,n6) -> % 0.70/0.90 10885:1:0:[10554.0,4854.0]:: p(n9,n6,n3) -> % 0.70/0.90 10849:1:0:[10553.0,4149.1]:: p(n5,n4,n9) -> % 0.70/0.90 10884:1:0:[10557.0,4848.1]:: p(n7,n6,n6) -> % 0.70/0.90 10883:1:0:[10554.0,4836.1]:: p(n7,n6,n3) -> % 0.70/0.90 10882:1:0:[10554.0,4818.1]:: p(n6,n6,n3) -> % 0.70/0.90 10881:1:0:[10557.0,4803.1]:: p(n5,n6,n6) -> % 0.70/0.90 10880:1:0:[10557.0,4767.1]:: p(n4,n6,n6) -> % 0.70/0.90 10850:1:0:[10553.0,4194.1]:: p(n7,n4,n9) -> % 0.70/0.90 10851:1:0:[10556.0,4195.1]:: p(n7,n4,n1) -> % 0.70/0.90 10852:1:0:[10556.0,4204.1]:: p(n8,n4,n1) -> % 0.70/0.90 10879:1:0:[10557.0,4722.1]:: p(n3,n6,n6) -> % 0.70/0.90 10853:1:0:[10553.0,4212.0]:: p(n9,n4,n9) -> % 0.70/0.90 10878:1:0:[10554.0,4710.1]:: p(n3,n6,n3) -> % 0.70/0.90 10877:1:0:[10536.0,4669.0]:: p(n9,n6,n7) -> % 0.70/0.90 10876:1:0:[10557.0,4668.1]:: p(n2,n6,n6) -> % 0.70/0.90 10875:1:0:[10536.0,4660.0]:: p(n8,n6,n7) -> % 0.70/0.90 10874:1:0:[10554.0,4656.1]:: p(n2,n6,n3) -> % 0.70/0.90 10854:1:0:[10551.0,4262.1]:: p(n1,n5,n5) -> % 0.70/0.90 10873:1:0:[10536.0,4642.0]:: p(n6,n6,n7) -> % 0.70/0.90 10872:1:0:[10536.0,4633.0]:: p(n5,n6,n7) -> % 0.70/0.90 10871:1:0:[10536.0,4615.0]:: p(n3,n6,n7) -> % 0.70/0.90 10855:1:0:[10538.0,4293.1]:: p(n2,n5,n9) -> % 0.70/0.90 10870:1:0:[10533.0,4594.0]:: p(n8,n6,n4) -> % 0.70/0.90 10869:1:0:[10554.0,4593.1]:: p(n1,n6,n3) -> % 0.70/0.90 10868:1:0:[10533.0,4585.0]:: p(n7,n6,n4) -> % 0.70/0.90 10867:1:0:[10533.0,4576.0]:: p(n6,n6,n4) -> % 0.70/0.90 10866:1:0:[10533.0,4567.0]:: p(n5,n6,n4) -> % 0.70/0.90 10865:1:0:[10536.0,4543.1]:: p(n1,n6,n7) -> % 0.70/0.90 10864:1:0:[10533.0,4540.0]:: p(n2,n6,n4) -> % 0.70/0.90 10863:1:0:[10551.0,4523.0]:: p(n9,n5,n5) -> % 0.70/0.90 10856:1:0:[10538.0,4356.0]:: p(n4,n5,n9) -> % 0.70/0.90 10862:1:0:[10551.0,4514.0]:: p(n8,n5,n5) -> % 0.70/0.90 10857:1:0:[10538.0,4365.0]:: p(n5,n5,n9) -> % 0.70/0.90 10861:1:0:[10551.0,4487.1]:: p(n6,n5,n5) -> % 0.70/0.90 10858:1:0:[10538.0,4383.0]:: p(n7,n5,n9) -> % 0.70/0.90 10860:1:0:[10551.0,4460.1]:: p(n5,n5,n5) -> % 0.70/0.90 10859:1:0:[10538.0,4401.0]:: p(n9,n5,n9) -> % 0.70/0.90 % 0.70/0.90 Most General Atoms: 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,n3) p(n1,n4,n4) p(n1,n4,n5) p(n1,n4,n7) p(n1,n4,n8) p(n1,n4,n9) p(n1,n5,n1) p(n1,n5,n2) p(n1,n5,n3) p(n1,n5,n4) p(n1,n5,n5) p(n9,n9,n4) p(n1,n5,n7) p(n1,n5,n8) p(n1,n5,n9) p(n1,n6,n1) p(n1,n6,n2) p(n1,n6,n3) p(n1,n6,n5) p(n9,n6,n6) p(n1,n6,n7) p(n1,n6,n8) p(n1,n6,n9) p(n1,n7,n1) p(n1,n7,n2) p(n1,n7,n3) p(n9,n4,n1) p(n1,n7,n5) p(n9,n1,n2) p(n1,n7,n7) p(n1,n7,n8) p(n1,n7,n9) p(n1,n8,n1) p(n1,n8,n2) p(n1,n8,n3) p(n8,n6,n3) p(n1,n8,n5) p(n8,n4,n9) p(n1,n8,n7) p(n1,n8,n8) p(n1,n8,n9) p(n1,n9,n1) p(n1,n9,n2) p(n1,n9,n3) p(n7,n7,n2) p(n1,n9,n5) p(n7,n5,n5) p(n1,n9,n7) p(n1,n9,n8) p(n7,n3,n7) p(n6,n9,n8) p(n6,n8,n6) p(n6,n2,n1) p(n6,n1,n9) p(n5,n7,n1) p(n5,n3,n3) p(n4,n9,n3) p(n4,n8,n5) p(n4,n2,n7) p(n4,n1,n4) p(n3,n7,n5) p(n3,n5,n9) p(n3,n3,n4) p(n2,n6,n7) p(n2,n4,n5) p(n1,n9,n9) p(n1,n6,n4) p(n1,n4,n6) p(n1,n1,n1) p(n7,n8,n9) p(n9,n7,n9) p(n9,n8,n9) p(n7,n8,n8) p(n8,n7,n8) p(n8,n8,n8) p(n9,n7,n8) p(n9,n8,n8) p(n8,n7,n7) p(n8,n8,n7) p(n8,n9,n7) p(n9,n7,n7) p(n9,n8,n7) p(n7,n9,n6) p(n8,n7,n6) p(n8,n9,n6) p(n7,n8,n3) p(n9,n7,n3) p(n9,n8,n3) p(n8,n5,n7) p(n9,n5,n7) p(n7,n4,n4) p(n8,n5,n4) p(n7,n2,n9) p(n9,n2,n9) p(n9,n3,n9) p(n7,n1,n8) p(n7,n2,n8) p(n8,n1,n8) p(n8,n2,n8) p(n8,n3,n8) p(n9,n2,n8) p(n9,n3,n8) p(n7,n1,n6) p(n7,n2,n6) p(n8,n1,n6) p(n8,n2,n6) p(n8,n3,n6) p(n1,n5,n6) p(n7,n1,n3) p(n7,n2,n3) p(n9,n2,n3) p(n1,n6,n6) p(n5,n8,n7) p(n5,n9,n7) p(n6,n7,n7) p(n5,n8,n4) p(n6,n7,n4) p(n1,n7,n6) p(n5,n8,n2) p(n5,n9,n2) p(n4,n4,n8) p(n4,n5,n8) p(n4,n6,n8) p(n5,n4,n8) p(n5,n5,n8) p(n5,n6,n8) p(n1,n8,n6) p(n5,n4,n4) p(n5,n5,n4) p(n6,n4,n4) p(n6,n5,n4) p(n4,n4,n2) p(n4,n5,n2) p(n4,n6,n2) p(n5,n4,n2) p(n5,n5,n2) p(n5,n6,n2) p(n6,n4,n2) p(n6,n5,n2) p(n6,n6,n2) p(n1,n9,n6) p(n4,n3,n8) p(n5,n1,n8) p(n5,n2,n8) p(n4,n3,n6) p(n5,n1,n6) p(n5,n2,n6) p(n5,n1,n5) p(n5,n2,n5) p(n6,n3,n5) p(n4,n3,n2) p(n5,n2,n2) p(n6,n3,n2) p(n2,n7,n8) p(n2,n8,n8) p(n3,n8,n8) p(n2,n7,n6) p(n2,n9,n6) p(n3,n9,n6) p(n2,n7,n3) p(n2,n8,n3) p(n3,n8,n3) p(n2,n8,n2) p(n2,n9,n2) p(n3,n8,n2) p(n3,n9,n2) p(n2,n8,n1) p(n2,n9,n1) p(n3,n8,n1) p(n3,n9,n1) p(n2,n5,n8) p(n3,n4,n8) p(n3,n6,n8) p(n2,n5,n3) p(n3,n4,n3) p(n2,n5,n2) p(n3,n4,n2) p(n3,n6,n2) p(n1,n7,n4) p(n2,n5,n1) p(n3,n6,n1) p(n2,n1,n8) p(n2,n2,n8) p(n2,n3,n8) p(n3,n1,n8) p(n3,n2,n8) p(n1,n8,n4) p(n2,n1,n6) p(n2,n2,n6) p(n2,n3,n6) p(n3,n1,n6) p(n3,n2,n6) p(n2,n1,n3) p(n2,n2,n3) p(n3,n1,n3) p(n3,n2,n3) p(n1,n9,n4) p(n2,n2,n2) p(n2,n3,n2) p(n3,n2,n2) p(n9,n5,n8) p(n9,n3,n5) p(n9,n2,n5) p(n8,n8,n1) p(n8,n2,n4) p(n8,n2,n5) p(n8,n1,n5) p(n2,n1,n1) p(n2,n2,n1) p(n2,n1,n2) p(n2,n1,n4) p(n2,n2,n4) p(n2,n1,n5) p(n2,n2,n5) p(n2,n1,n7) p(n2,n2,n7) p(n2,n1,n9) p(n2,n2,n9) p(n2,n3,n1) p(n2,n3,n3) p(n2,n3,n4) p(n2,n3,n5) p(n2,n3,n7) p(n2,n3,n9) p(n2,n4,n1) p(n2,n4,n2) p(n2,n4,n3) p(n2,n4,n4) p(n2,n4,n6) p(n2,n4,n7) p(n2,n4,n8) p(n2,n4,n9) p(n2,n5,n4) p(n7,n9,n1) p(n2,n5,n6) p(n2,n5,n7) p(n2,n5,n9) p(n2,n6,n1) p(n2,n6,n2) p(n2,n6,n3) p(n2,n6,n4) p(n7,n8,n1) p(n2,n6,n6) p(n2,n6,n8) p(n2,n6,n9) p(n2,n7,n1) p(n2,n7,n2) p(n2,n7,n4) p(n7,n6,n8) p(n7,n4,n8) p(n2,n7,n9) p(n2,n8,n4) p(n7,n2,n4) p(n2,n8,n6) p(n2,n8,n9) p(n2,n9,n3) p(n2,n9,n4) p(n6,n6,n5) p(n2,n9,n8) p(n2,n9,n9) p(n6,n5,n3) p(n6,n5,n7) p(n6,n4,n3) p(n6,n4,n7) p(n5,n8,n9) p(n5,n6,n5) p(n5,n6,n9) p(n5,n5,n6) p(n5,n5,n7) p(n5,n4,n7) p(n4,n7,n9) p(n4,n6,n1) p(n4,n6,n9) p(n4,n5,n1) p(n4,n5,n6) p(n3,n9,n7) p(n2,n5,n5) p(n2,n6,n5) p(n2,n7,n5) p(n3,n8,n7) p(n2,n8,n5) p(n2,n9,n5) p(n2,n7,n7) p(n2,n8,n7) p(n2,n9,n7) p(n8,n9,n5) p(n3,n1,n1) p(n3,n2,n1) p(n3,n1,n2) p(n3,n1,n4) p(n3,n2,n4) p(n3,n1,n5) p(n3,n2,n5) p(n3,n1,n7) p(n3,n2,n7) p(n3,n1,n9) p(n3,n2,n9) p(n3,n3,n1) p(n3,n3,n2) p(n3,n3,n3) p(n3,n3,n5) p(n3,n3,n6) p(n3,n3,n7) p(n3,n3,n8) p(n3,n3,n9) p(n3,n4,n1) p(n3,n4,n5) p(n3,n4,n6) p(n3,n4,n7) p(n3,n4,n9) p(n3,n5,n1) p(n3,n5,n2) p(n3,n5,n3) p(n8,n9,n1) p(n3,n5,n5) p(n3,n5,n6) p(n3,n5,n7) p(n3,n5,n8) p(n3,n6,n3) p(n3,n6,n5) p(n3,n6,n6) p(n3,n6,n7) p(n3,n7,n1) p(n3,n7,n2) p(n3,n7,n3) p(n3,n7,n6) p(n3,n7,n7) p(n3,n7,n8) p(n3,n8,n6) p(n3,n9,n3) p(n3,n9,n8) p(n8,n5,n8) p(n3,n4,n4) p(n3,n5,n4) p(n3,n6,n4) p(n3,n7,n4) p(n3,n8,n4) p(n3,n9,n4) p(n8,n3,n5) p(n8,n3,n1) p(n3,n6,n9) p(n3,n7,n9) p(n3,n8,n9) p(n3,n9,n9) p(n3,n8,n5) p(n3,n9,n5) p(n8,n5,n2) p(n4,n1,n1) p(n4,n2,n1) p(n4,n1,n2) p(n4,n2,n2) p(n4,n1,n3) p(n4,n2,n3) p(n4,n2,n4) p(n4,n1,n5) p(n4,n2,n5) p(n4,n1,n6) p(n4,n2,n6) p(n4,n1,n7) p(n4,n1,n8) p(n4,n2,n8) p(n4,n1,n9) p(n4,n2,n9) p(n4,n3,n1) p(n4,n3,n3) p(n4,n3,n4) p(n4,n3,n5) p(n4,n3,n9) p(n4,n4,n1) p(n4,n4,n3) p(n4,n4,n4) p(n4,n4,n5) p(n4,n4,n6) p(n4,n4,n9) p(n4,n5,n3) p(n4,n5,n4) p(n4,n5,n5) p(n4,n5,n9) p(n4,n6,n3) p(n4,n6,n4) p(n4,n6,n5) p(n4,n6,n6) p(n4,n7,n1) p(n4,n7,n2) p(n4,n7,n3) p(n4,n7,n4) p(n4,n7,n5) p(n4,n7,n6) p(n4,n7,n8) p(n4,n8,n1) p(n4,n8,n2) p(n4,n8,n3) p(n4,n8,n4) p(n4,n8,n6) p(n4,n8,n8) p(n4,n8,n9) p(n4,n9,n1) p(n4,n9,n2) p(n4,n9,n4) p(n4,n9,n6) p(n4,n9,n8) p(n4,n9,n9) p(n4,n3,n7) p(n4,n4,n7) p(n4,n5,n7) p(n4,n6,n7) p(n4,n7,n7) p(n4,n8,n7) p(n4,n9,n7) p(n8,n8,n4) p(n8,n7,n4) p(n7,n8,n4) p(n8,n9,n2) p(n8,n8,n2) p(n9,n5,n3) p(n8,n5,n6) p(n8,n5,n1) p(n4,n9,n5) p(n5,n1,n1) p(n5,n2,n1) p(n5,n1,n2) p(n5,n1,n3) p(n5,n2,n3) p(n5,n1,n4) p(n5,n2,n4) p(n5,n1,n7) p(n5,n2,n7) p(n5,n1,n9) p(n5,n2,n9) p(n5,n3,n1) p(n5,n3,n2) p(n5,n3,n4) p(n5,n3,n5) p(n5,n3,n6) p(n5,n3,n7) p(n5,n3,n8) p(n5,n3,n9) p(n5,n4,n1) p(n7,n6,n1) p(n5,n4,n5) p(n5,n4,n6) p(n5,n4,n9) p(n5,n5,n1) p(n5,n5,n5) p(n5,n5,n9) p(n5,n6,n1) p(n5,n6,n4) p(n5,n6,n6) p(n5,n6,n7) p(n5,n7,n2) p(n7,n6,n9) p(n5,n7,n4) p(n5,n7,n5) p(n5,n7,n6) p(n5,n7,n7) p(n5,n7,n8) p(n5,n7,n9) p(n7,n4,n3) p(n5,n8,n5) p(n5,n8,n6) p(n5,n8,n8) p(n5,n9,n4) p(n5,n9,n5) p(n5,n9,n6) p(n5,n9,n8) p(n5,n9,n9) p(n8,n3,n2) p(n8,n2,n2) p(n5,n4,n3) p(n5,n5,n3) p(n5,n6,n3) p(n5,n7,n3) p(n5,n8,n3) p(n5,n9,n3) p(n8,n1,n7) p(n5,n8,n1) p(n5,n9,n1) p(n6,n7,n3) p(n6,n1,n1) p(n6,n1,n2) p(n6,n2,n2) p(n6,n1,n3) p(n6,n2,n3) p(n6,n1,n4) p(n6,n2,n4) p(n6,n1,n5) p(n6,n2,n5) p(n6,n1,n6) p(n6,n2,n6) p(n6,n1,n7) p(n6,n2,n7) p(n6,n1,n8) p(n6,n2,n8) p(n6,n2,n9) p(n6,n3,n3) p(n6,n3,n4) p(n6,n3,n6) p(n6,n3,n7) p(n6,n3,n8) p(n6,n3,n9) p(n6,n4,n5) p(n6,n4,n6) p(n6,n4,n8) p(n6,n4,n9) p(n6,n5,n5) p(n6,n5,n6) p(n6,n5,n8) p(n6,n5,n9) p(n6,n6,n3) p(n6,n6,n4) p(n6,n6,n6) p(n6,n6,n7) p(n6,n6,n8) p(n6,n6,n9) p(n6,n7,n2) p(n6,n7,n5) p(n6,n7,n6) p(n6,n7,n8) p(n6,n7,n9) p(n6,n8,n2) p(n6,n8,n3) p(n6,n8,n4) p(n6,n8,n5) p(n6,n8,n7) p(n6,n8,n8) p(n6,n8,n9) p(n6,n9,n2) p(n6,n9,n3) p(n6,n9,n4) p(n6,n9,n5) p(n6,n9,n7) p(n6,n9,n9) p(n6,n3,n1) p(n6,n4,n1) p(n6,n5,n1) p(n6,n6,n1) p(n6,n7,n1) p(n6,n8,n1) p(n6,n9,n1) p(n6,n9,n6) p(n7,n1,n1) p(n7,n2,n1) p(n7,n1,n2) p(n7,n2,n2) p(n7,n1,n4) p(n7,n1,n5) p(n7,n2,n5) p(n7,n1,n7) p(n7,n2,n7) 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,n6) p(n7,n3,n8) p(n7,n3,n9) p(n7,n4,n1) p(n7,n4,n2) p(n7,n4,n5) p(n7,n4,n6) p(n7,n4,n9) p(n7,n5,n1) p(n7,n5,n2) p(n7,n5,n3) p(n7,n5,n4) p(n7,n5,n6) p(n7,n5,n8) p(n7,n5,n9) p(n7,n6,n2) p(n7,n6,n3) p(n7,n6,n4) p(n7,n6,n6) p(n7,n7,n1) p(n7,n7,n3) p(n7,n7,n4) p(n7,n7,n6) p(n7,n7,n8) p(n7,n7,n9) p(n7,n8,n6) p(n7,n9,n3) p(n7,n9,n4) p(n7,n9,n8) p(n7,n9,n9) p(n7,n4,n7) p(n7,n5,n7) p(n7,n6,n7) p(n7,n7,n7) p(n7,n8,n7) p(n7,n9,n7) p(n7,n6,n5) p(n7,n7,n5) p(n9,n9,n7) p(n7,n8,n5) p(n9,n9,n5) p(n7,n9,n5) p(n7,n8,n2) p(n7,n9,n2) p(n9,n6,n9) p(n9,n6,n8) p(n9,n6,n5) p(n8,n1,n1) p(n8,n2,n1) p(n8,n1,n2) p(n8,n1,n3) p(n8,n2,n3) p(n8,n1,n4) p(n8,n2,n7) p(n8,n1,n9) p(n8,n2,n9) p(n8,n3,n3) p(n8,n3,n4) p(n8,n3,n7) p(n8,n3,n9) p(n8,n4,n1) p(n8,n4,n2) p(n8,n4,n3) p(n8,n4,n4) p(n8,n4,n5) p(n8,n4,n6) p(n8,n4,n7) p(n8,n4,n8) p(n8,n5,n3) p(n8,n5,n5) p(n8,n6,n1) p(n8,n6,n2) p(n8,n6,n4) p(n8,n6,n5) p(n8,n6,n6) p(n8,n6,n7) p(n8,n6,n8) p(n9,n4,n8) p(n8,n7,n1) p(n8,n7,n2) p(n9,n4,n7) p(n8,n7,n5) p(n9,n4,n3) p(n8,n8,n5) p(n8,n8,n6) p(n8,n9,n4) p(n8,n9,n8) p(n9,n1,n8) p(n9,n1,n7) p(n9,n1,n5) p(n9,n1,n3) p(n8,n5,n9) p(n8,n6,n9) p(n8,n7,n9) p(n8,n8,n9) p(n8,n9,n9) p(n8,n7,n3) p(n8,n8,n3) p(n8,n9,n3) p(n9,n1,n1) p(n9,n2,n1) p(n9,n2,n2) p(n9,n1,n4) p(n9,n2,n4) p(n9,n1,n6) p(n9,n2,n6) p(n9,n2,n7) p(n9,n1,n9) p(n9,n3,n1) p(n9,n3,n2) p(n9,n3,n3) p(n9,n3,n4) p(n9,n3,n6) p(n9,n3,n7) p(n9,n4,n2) p(n9,n4,n4) p(n9,n4,n5) p(n9,n4,n6) p(n9,n4,n9) p(n9,n5,n2) p(n9,n5,n4) p(n9,n5,n5) p(n9,n5,n6) p(n9,n5,n9) p(n9,n6,n2) p(n9,n6,n3) p(n9,n6,n4) p(n9,n6,n7) p(n9,n7,n2) p(n9,n7,n4) p(n9,n7,n5) p(n9,n8,n2) p(n9,n8,n4) p(n9,n8,n5) p(n9,n9,n2) p(n9,n9,n3) p(n9,n9,n8) p(n9,n9,n9) p(n9,n5,n1) p(n9,n6,n1) p(n9,n7,n1) p(n9,n8,n1) p(n9,n9,n1) p(n9,n7,n6) p(n9,n8,n6) p(n9,n9,n6) % 0.70/0.90 % 0.70/0.90 === Starting SPASS-SCL-FOL A Little Less Naive, considering 729 atoms initially, heuristics mode: lmodel_grow === % 0.70/0.90 % 0.70/0.90 % 0.70/0.90 Linear Model Building succeeded. % 0.70/0.90 SZS status Satisfiable % 0.70/0.90 % 0.70/0.90 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.70/0.90 % 0.70/0.90 SPASS-SCL-FOL Statistics: % 0.70/0.90 Number of learned clauses: 0 % 0.70/0.90 Number of propagations: 724 % 0.70/0.90 Number of decisions: 5 % 0.70/0.90 Number of resolutions: 0 % 0.70/0.90 Number of condensations: 0 % 0.70/0.90 Number of sub resolutions: 1555 % 0.70/0.90 Number of input literals (deduplicated): 729 % 0.70/0.90 Number of grows: 0 % 0.70/0.90 Number of considered ground atoms: 729 % 0.70/0.90 % 0.70/0.90 Needed: 0:00:00.35 % 0.70/0.90 %------------------------------------------------------------------------------