%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PUZ069+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 : n006.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:31 PM UTC 2026
% Result : Satisfiable 2.28s 1.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ069+2 : TPTP v9.2.1. Bugfixed v5.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n006.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 12:58:31 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]
% 2.28/1.03 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.28/1.03 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.28/1.03 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.28/1.03 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.28/1.03 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.28/1.03 Execution normal ended with status: satisfiable
% 2.28/1.03 Used heuristic: normal
% 2.28/1.03
% 2.28/1.03 Input Clauses:
% 2.28/1.05
% 2.28/1.05 Predicates: p
% 2.28/1.05 Fol Constants: n1 n2 n3 n4 n5 n6 n7 n8 n9
% 2.28/1.05 Fol Functions:
% 2.28/1.05 Problem Properties:
% 2.28/1.05 This is a first-order ground problem without equality.
% 2.28/1.05
% 2.28/1.05 After reduction: Problem Properties:
% 2.28/1.05 This is a first-order ground problem without equality.
% 2.28/1.05
% 2.28/1.05
% 2.28/1.05 Reduced Input Clauses:
% 2.28/1.05 10548:1:0:[10531.0,1.0]:: p(n1,n2,n1) ->
% 2.28/1.05 10549:1:0:[10531.0,10.0]:: p(n1,n3,n1) ->
% 2.28/1.05 10550:1:0:[10532.0,16.1]:: p(n1,n1,n7) ->
% 2.28/1.05 10551:1:0:[10531.0,19.0]:: p(n1,n4,n1) ->
% 2.28/1.05 10552:1:0:[10533.0,24.1]:: p(n1,n1,n6) ->
% 2.28/1.05 10553:1:0:[10531.0,28.0]:: p(n1,n5,n1) ->
% 2.28/1.05 10554:1:0:[10531.0,37.0]:: p(n1,n6,n1) ->
% 2.28/1.05 10555:1:0:[10531.0,46.0]:: p(n1,n7,n1) ->
% 2.28/1.05 10556:1:0:[10531.0,55.0]:: p(n1,n8,n1) ->
% 2.28/1.05 10557:1:0:[10531.0,64.0]:: p(n1,n9,n1) ->
% 2.28/1.05 10558:1:0:[10532.0,79.1]:: p(n1,n2,n7) ->
% 2.28/1.05 10559:1:0:[10533.0,87.1]:: p(n1,n2,n6) ->
% 2.28/1.05 11998:7:0:[10885.1,10530.1,10898.1,11997.3]:: -> p(n7,n7,n9),p(n7,n9,n9),p(n8,n8,n9),p(n8,n9,n9),p(n9,n7,n9),p(n9,n8,n9),p(n9,n9,n9)
% 2.28/1.05 11996:7:0:[10884.1,10529.1,10897.1,11995.3]:: -> p(n7,n7,n8),p(n7,n9,n8),p(n8,n8,n8),p(n8,n9,n8),p(n9,n7,n8),p(n9,n8,n8),p(n9,n9,n8)
% 2.28/1.05 11994:5:0:[10660.1,10528.0,10662.1,11991.1,10663.1,11992.2,10896.1,11993.3]:: -> p(n8,n8,n7),p(n8,n9,n7),p(n9,n7,n7),p(n9,n8,n7),p(n9,n9,n7)
% 2.28/1.05 11990:5:0:[10774.1,10526.0,10883.1,11987.1,10776.1,11988.3,10777.1,11989.6]:: -> p(n7,n9,n5),p(n8,n8,n5),p(n8,n9,n5),p(n9,n8,n5),p(n9,n9,n5)
% 2.28/1.05 11986:7:0:[10882.1,10525.1,10894.1,11985.3]:: -> p(n7,n7,n4),p(n7,n9,n4),p(n8,n8,n4),p(n8,n9,n4),p(n9,n7,n4),p(n9,n8,n4),p(n9,n9,n4)
% 2.28/1.05 11984:3:0:[10780.1,10524.0,10881.1,11979.1,10675.1,11980.3,10676.1,11981.4,10677.1,11982.5,10781.1,11983.6]:: -> p(n7,n9,n3),p(n9,n8,n3),p(n9,n9,n3)
% 2.28/1.05 11978:8:0:[10879.1,10521.0]:: -> p(n7,n5,n9),p(n7,n6,n9),p(n8,n4,n9),p(n8,n5,n9),p(n8,n6,n9),p(n9,n4,n9),p(n9,n5,n9),p(n9,n6,n9)
% 2.28/1.05 11977:5:0:[10878.1,10520.0,10760.1,11974.2,10761.1,11975.5,10762.1,11976.8]:: -> p(n7,n5,n8),p(n8,n4,n8),p(n8,n5,n8),p(n9,n4,n8),p(n9,n5,n8)
% 2.28/1.05 11973:5:0:[10877.0,10517.0,10750.1,11970.1,10751.1,11971.4,10752.1,11972.7]:: -> p(n7,n6,n5),p(n8,n4,n5),p(n8,n6,n5),p(n9,n4,n5),p(n9,n6,n5)
% 2.28/1.05 11969:5:0:[10876.0,10516.0,10746.1,11966.1,10747.1,11967.4,10748.1,11968.7]:: -> p(n7,n6,n4),p(n8,n4,n4),p(n8,n6,n4),p(n9,n4,n4),p(n9,n6,n4)
% 2.28/1.05 11965:3:0:[10875.0,10515.0,10765.1,11960.2,10671.1,11961.3,10672.1,11962.4,10673.1,11963.5,10766.1,11964.8]:: -> p(n7,n5,n3),p(n9,n4,n3),p(n9,n5,n3)
% 2.28/1.05 11959:4:0:[10731.1,10514.0,10679.0,11955.3,10680.0,11956.4,10681.0,11957.5,10733.1,11958.6]:: -> p(n7,n5,n2),p(n7,n6,n2),p(n9,n5,n2),p(n9,n6,n2)
% 2.28/1.05 11954:6:0:[10661.0,10513.0,10664.0,11952.1,10665.0,11953.2]:: -> p(n8,n4,n1),p(n8,n5,n1),p(n8,n6,n1),p(n9,n4,n1),p(n9,n5,n1),p(n9,n6,n1)
% 2.28/1.05 10560:1:0:[10533.0,141.1]:: p(n1,n3,n6) ->
% 2.28/1.05 10561:1:0:[10532.0,142.0]:: p(n1,n4,n7) ->
% 2.28/1.05 11951:5:0:[10696.1,10512.0,10697.1,11948.3,10892.1,11949.4,10698.1,11950.6]:: -> p(n7,n2,n9),p(n7,n3,n9),p(n8,n3,n9),p(n9,n2,n9),p(n9,n3,n9)
% 2.28/1.05 11947:8:0:[10891.1,10511.4]:: -> p(n7,n1,n8),p(n7,n2,n8),p(n7,n3,n8),p(n8,n1,n8),p(n8,n3,n8),p(n9,n1,n8),p(n9,n2,n8),p(n9,n3,n8)
% 2.28/1.05 10562:1:0:[10532.0,151.0]:: p(n1,n5,n7) ->
% 2.28/1.05 11946:3:0:[10652.0,10510.0,10654.0,11941.1,10656.0,11942.2,10890.1,11943.4,10716.1,11944.5,10717.1,11945.8]:: -> p(n8,n1,n7),p(n9,n1,n7),p(n9,n2,n7)
% 2.28/1.05 11940:8:0:[10889.1,10509.4]:: -> p(n7,n1,n6),p(n7,n2,n6),p(n7,n3,n6),p(n8,n1,n6),p(n8,n3,n6),p(n9,n1,n6),p(n9,n2,n6),p(n9,n3,n6)
% 2.28/1.05 10563:1:0:[10532.0,160.0]:: p(n1,n6,n7) ->
% 2.28/1.05 11939:8:0:[10888.1,10508.4]:: -> p(n7,n1,n5),p(n7,n2,n5),p(n7,n3,n5),p(n8,n1,n5),p(n8,n3,n5),p(n9,n1,n5),p(n9,n2,n5),p(n9,n3,n5)
% 2.28/1.05 11938:8:0:[10887.1,10507.4]:: -> p(n7,n1,n4),p(n7,n2,n4),p(n7,n3,n4),p(n8,n1,n4),p(n8,n3,n4),p(n9,n1,n4),p(n9,n2,n4),p(n9,n3,n4)
% 2.28/1.05 10564:1:0:[10532.0,169.0]:: p(n1,n7,n7) ->
% 2.28/1.05 11937:4:0:[10705.1,10505.1,10669.0,11933.3,10674.0,11934.4,10678.0,11935.5,10706.1,11936.7]:: -> p(n7,n1,n2),p(n7,n3,n2),p(n9,n1,n2),p(n9,n3,n2)
% 2.28/1.05 11932:3:0:[10653.0,10504.0,10655.0,11927.1,10657.0,11928.2,10690.1,11929.3,10886.0,11930.4,10691.1,11931.6]:: -> p(n8,n3,n1),p(n9,n2,n1),p(n9,n3,n1)
% 2.28/1.05 10565:1:0:[10532.0,178.0]:: p(n1,n8,n7) ->
% 2.28/1.05 11926:6:0:[10625.1,10503.3,10627.1,11924.4,10628.1,11925.5]:: -> p(n4,n7,n9),p(n4,n8,n9),p(n4,n9,n9),p(n6,n7,n9),p(n6,n8,n9),p(n6,n9,n9)
% 2.28/1.05 11923:8:0:[10862.1,10502.4]:: -> p(n4,n7,n8),p(n4,n8,n8),p(n4,n9,n8),p(n5,n7,n8),p(n5,n9,n8),p(n6,n7,n8),p(n6,n8,n8),p(n6,n9,n8)
% 2.28/1.05 10566:1:0:[10532.0,187.0]:: p(n1,n9,n7) ->
% 2.28/1.05 11922:8:0:[10861.1,10501.4]:: -> p(n4,n7,n7),p(n4,n8,n7),p(n4,n9,n7),p(n5,n7,n7),p(n5,n9,n7),p(n6,n7,n7),p(n6,n8,n7),p(n6,n9,n7)
% 2.28/1.05 10567:1:0:[10533.0,195.0]:: p(n1,n5,n6) ->
% 2.28/1.05 11921:3:0:[10772.1,10499.0,10773.1,11916.3,10860.0,11917.4,10646.1,11918.6,10647.1,11919.7,10648.1,11920.8]:: -> p(n4,n8,n5),p(n4,n9,n5),p(n5,n9,n5)
% 2.28/1.05 11915:5:0:[10617.1,10498.0,10618.1,11912.1,10619.1,11913.2,10859.0,11914.4]:: -> p(n5,n7,n4),p(n5,n9,n4),p(n6,n7,n4),p(n6,n8,n4),p(n6,n9,n4)
% 2.28/1.05 10568:1:0:[10533.0,204.0]:: p(n1,n6,n6) ->
% 2.28/1.05 11911:3:0:[10778.1,10497.0,10779.1,11906.3,10858.0,11907.4,10649.1,11908.6,10650.1,11909.7,10651.1,11910.8]:: -> p(n4,n8,n3),p(n4,n9,n3),p(n5,n9,n3)
% 2.28/1.05 11905:3:0:[10613.1,10496.0,10614.1,11900.1,10615.1,11901.2,10782.0,11902.3,10857.0,11903.4,10783.0,11904.6]:: -> p(n5,n9,n2),p(n6,n8,n2),p(n6,n9,n2)
% 2.28/1.05 10569:1:0:[10533.0,213.0]:: p(n1,n7,n6) ->
% 2.28/1.05 11899:2:0:[10844.1,10494.0,10850.1,11893.1,10622.1,11894.3,10623.1,11895.4,10624.1,11896.5,10868.1,11897.7,10874.1,11898.8]:: -> p(n4,n6,n9),p(n6,n4,n9)
% 2.28/1.05 11892:3:0:[10843.1,10493.0,10849.1,11887.1,10756.1,11888.2,10757.1,11889.5,10867.1,11890.7,10759.1,11891.8]:: -> p(n5,n4,n8),p(n5,n5,n8),p(n6,n4,n8)
% 2.28/1.05 10570:1:0:[10533.0,222.0]:: p(n1,n8,n6) ->
% 2.28/1.05 11886:3:0:[10732.0,10492.0,10848.1,11881.1,10734.0,11882.3,10735.0,11883.6,10866.1,11884.7,10873.1,11885.8]:: -> p(n4,n6,n7),p(n5,n5,n7),p(n5,n6,n7)
% 2.28/1.05 11880:1:0:[10721.1,10491.0,10847.1,11873.1,10631.0,11874.3,10632.0,11875.4,10633.0,11876.5,10722.1,11877.6,10865.1,11878.7,10872.1,11879.8]:: -> p(n4,n6,n6)
% 2.28/1.05 10571:1:0:[10533.0,231.0]:: p(n1,n9,n6) ->
% 2.28/1.05 11872:5:0:[10840.0,10486.0,10845.0,11869.1,10863.0,11870.7,10869.0,11871.8]:: -> p(n4,n6,n1),p(n5,n4,n1),p(n5,n5,n1),p(n5,n6,n1),p(n6,n4,n1)
% 2.28/1.05 11868:8:0:[10856.0,10484.3]:: -> p(n4,n1,n8),p(n4,n2,n8),p(n4,n3,n8),p(n5,n2,n8),p(n5,n3,n8),p(n6,n1,n8),p(n6,n2,n8),p(n6,n3,n8)
% 2.28/1.05 11867:5:0:[10713.1,10483.2,10855.0,11864.3,10714.1,11865.5,10715.1,11866.8]:: -> p(n4,n1,n7),p(n4,n2,n7),p(n5,n2,n7),p(n6,n1,n7),p(n6,n2,n7)
% 2.28/1.05 11863:5:0:[10854.0,10481.3,10636.0,11860.6,10638.0,11861.7,10640.0,11862.8]:: -> p(n4,n1,n5),p(n4,n2,n5),p(n4,n3,n5),p(n5,n2,n5),p(n5,n3,n5)
% 2.28/1.05 11859:5:0:[10605.0,10480.0,10607.0,11856.1,10609.0,11857.2,10853.0,11858.3]:: -> p(n5,n2,n4),p(n5,n3,n4),p(n6,n1,n4),p(n6,n2,n4),p(n6,n3,n4)
% 2.28/1.05 11855:3:0:[10707.0,10479.1,10852.0,11850.3,10708.0,11851.4,10637.0,11852.6,10639.0,11853.7,10641.0,11854.8]:: -> p(n4,n1,n3),p(n4,n3,n3),p(n5,n3,n3)
% 2.28/1.05 11849:3:0:[10604.0,10478.0,10606.0,11844.1,10608.0,11845.2,10851.0,11846.3,10703.1,11847.4,10704.1,11848.7]:: -> p(n5,n3,n2),p(n6,n1,n2),p(n6,n3,n2)
% 2.28/1.05 11843:6:0:[10686.1,10477.0,10687.1,11841.3,10689.1,11842.6]:: -> p(n4,n2,n1),p(n4,n3,n1),p(n5,n2,n1),p(n5,n3,n1),p(n6,n2,n1),p(n6,n3,n1)
% 2.28/1.05 11840:7:0:[10826.1,10476.3,10839.1,11839.6]:: -> p(n1,n7,n9),p(n1,n8,n9),p(n1,n9,n9),p(n2,n8,n9),p(n2,n9,n9),p(n3,n8,n9),p(n3,n9,n9)
% 2.28/1.05 11838:5:0:[10583.1,10475.3,10584.1,11835.4,10585.1,11836.5,10838.1,11837.6]:: -> p(n1,n7,n8),p(n1,n8,n8),p(n1,n9,n8),p(n3,n8,n8),p(n3,n9,n8)
% 2.28/1.05 11834:4:0:[10564.1,10474.0,10565.1,11830.1,10566.1,11831.2,10825.1,11832.3,10837.1,11833.6]:: -> p(n2,n8,n7),p(n2,n9,n7),p(n3,n8,n7),p(n3,n9,n7)
% 2.28/1.05 11829:2:0:[10569.1,10473.0,10570.1,11823.1,10571.1,11824.2,10824.1,11825.3,10786.0,11826.4,10836.1,11827.6,10788.0,11828.7]:: -> p(n2,n9,n6),p(n3,n9,n6)
% 2.28/1.05 11822:7:0:[10823.0,10471.3,10835.1,11821.6]:: -> p(n1,n7,n4),p(n1,n8,n4),p(n1,n9,n4),p(n2,n8,n4),p(n2,n9,n4),p(n3,n8,n4),p(n3,n9,n4)
% 2.28/1.05 11820:4:0:[10769.0,10469.0,10775.0,11816.3,10594.1,11817.6,10596.1,11818.7,10597.1,11819.8]:: -> p(n1,n8,n2),p(n1,n9,n2),p(n2,n8,n2),p(n2,n9,n2)
% 2.28/1.05 11815:2:0:[10555.1,10468.0,10556.1,11809.1,10557.1,11810.2,10822.0,11811.3,10787.0,11812.4,10834.0,11813.6,10789.0,11814.7]:: -> p(n2,n9,n1),p(n3,n9,n1)
% 2.28/1.05 11808:7:0:[10815.1,10467.0,10821.1,11807.5]:: -> p(n1,n5,n9),p(n1,n6,n9),p(n2,n4,n9),p(n2,n5,n9),p(n3,n4,n9),p(n3,n5,n9),p(n3,n6,n9)
% 2.28/1.05 11806:3:0:[10561.1,10465.0,10562.1,11801.1,10563.1,11802.2,10727.0,11803.3,10820.0,11804.5,10728.0,11805.6]:: -> p(n2,n5,n7),p(n3,n5,n7),p(n3,n6,n7)
% 2.28/1.05 11800:3:0:[10813.0,10463.0,10739.0,11795.1,10579.0,11796.3,10581.0,11797.4,10582.0,11798.5,10742.0,11799.7]:: -> p(n1,n6,n5),p(n3,n4,n5),p(n3,n6,n5)
% 2.28/1.05 11794:4:0:[10812.0,10462.0,10738.0,11790.1,10740.0,11791.4,10818.0,11792.5,10741.0,11793.7]:: -> p(n1,n6,n4),p(n2,n4,n4),p(n3,n4,n4),p(n3,n6,n4)
% 2.28/1.05 11789:3:0:[10720.0,10460.0,10726.0,11784.3,10817.0,11785.5,10591.1,11786.6,10592.1,11787.7,10593.1,11788.8]:: -> p(n1,n5,n2),p(n1,n6,n2),p(n2,n5,n2)
% 2.28/1.05 11783:5:0:[10551.1,10459.0,10553.1,11780.1,10554.1,11781.2,10816.0,11782.5]:: -> p(n2,n4,n1),p(n2,n5,n1),p(n3,n4,n1),p(n3,n5,n1),p(n3,n6,n1)
% 2.28/1.05 11779:4:0:[10688.0,10458.0,10810.1,11775.2,10692.0,11776.3,10693.0,11777.6,10833.1,11778.7]:: -> p(n1,n2,n9),p(n2,n2,n9),p(n2,n3,n9),p(n3,n3,n9)
% 2.28/1.05 11774:3:0:[10804.1,10457.0,10809.1,11769.2,10572.0,11770.3,10574.0,11771.4,10576.0,11772.5,10832.1,11773.7]:: -> p(n1,n2,n8),p(n3,n1,n8),p(n3,n3,n8)
% 2.28/1.05 11768:5:0:[10552.0,10455.0,10559.0,11765.1,10560.0,11766.2,10830.1,11767.7]:: -> p(n2,n1,n6),p(n2,n2,n6),p(n2,n3,n6),p(n3,n1,n6),p(n3,n3,n6)
% 2.28/1.05 11764:3:0:[10803.1,10454.0,10808.0,11759.2,10573.0,11760.3,10575.0,11761.4,10577.0,11762.5,10829.1,11763.7]:: -> p(n1,n2,n5),p(n3,n1,n5),p(n3,n3,n5)
% 2.28/1.05 11758:6:0:[10802.1,10453.0,10807.0,11756.2,10828.1,11757.7]:: -> p(n1,n2,n4),p(n2,n1,n4),p(n2,n2,n4),p(n2,n3,n4),p(n3,n1,n4),p(n3,n3,n4)
% 2.28/1.05 11755:2:0:[10801.1,10452.0,10700.0,11749.1,10806.0,11750.2,10702.0,11751.4,10589.0,11752.6,10595.0,11753.7,10598.0,11754.8]:: -> p(n2,n1,n3),p(n2,n3,n3)
% 2.28/1.05 11748:7:0:[10949.1,10449.0,10952.1,11747.1]:: -> p(n9,n9,n3),p(n9,n9,n4),p(n9,n9,n5),p(n9,n9,n6),p(n9,n9,n7),p(n9,n9,n8),p(n9,n9,n9)
% 2.28/1.05 11746:6:0:[10799.1,10448.0,10951.1,11744.1,10796.1,11745.5]:: -> p(n9,n8,n3),p(n9,n8,n4),p(n9,n8,n5),p(n9,n8,n7),p(n9,n8,n8),p(n9,n8,n9)
% 2.28/1.05 11743:5:0:[10948.1,10447.0,10785.1,11740.1,10781.1,11741.2,10777.1,11742.4]:: -> p(n9,n7,n4),p(n9,n7,n6),p(n9,n7,n7),p(n9,n7,n8),p(n9,n7,n9)
% 2.28/1.05 11739:6:0:[10766.1,10446.2,10946.1,11737.6,10762.1,11738.7]:: -> p(n9,n6,n1),p(n9,n6,n2),p(n9,n6,n4),p(n9,n6,n5),p(n9,n6,n6),p(n9,n6,n9)
% 2.28/1.05 10572:1:0:[10534.0,368.1]:: p(n2,n1,n8) ->
% 2.28/1.05 10573:1:0:[10535.0,374.1]:: p(n2,n1,n5) ->
% 2.28/1.05 11736:6:0:[10748.1,10445.3,10752.1,11734.4,10945.1,11735.6]:: -> p(n9,n5,n1),p(n9,n5,n2),p(n9,n5,n3),p(n9,n5,n6),p(n9,n5,n8),p(n9,n5,n9)
% 2.28/1.05 11733:6:0:[10733.1,10444.1,10725.1,11731.5,10737.1,11732.6]:: -> p(n9,n4,n1),p(n9,n4,n3),p(n9,n4,n4),p(n9,n4,n5),p(n9,n4,n8),p(n9,n4,n9)
% 2.28/1.05 11730:7:0:[10942.1,10443.2,10717.1,11729.6]:: -> p(n9,n3,n1),p(n9,n3,n2),p(n9,n3,n4),p(n9,n3,n5),p(n9,n3,n6),p(n9,n3,n8),p(n9,n3,n9)
% 2.28/1.05 11728:7:0:[10706.1,10442.1,10710.1,11727.2]:: -> p(n9,n2,n1),p(n9,n2,n4),p(n9,n2,n5),p(n9,n2,n6),p(n9,n2,n7),p(n9,n2,n8),p(n9,n2,n9)
% 2.28/1.05 11726:6:0:[10691.1,10441.0,10941.1,11724.2,10698.1,11725.8]:: -> p(n9,n1,n2),p(n9,n1,n4),p(n9,n1,n5),p(n9,n1,n6),p(n9,n1,n7),p(n9,n1,n8)
% 2.28/1.05 10574:1:0:[10534.0,431.1]:: p(n2,n2,n8) ->
% 2.28/1.05 10575:1:0:[10535.0,437.1]:: p(n2,n2,n5) ->
% 2.28/1.05 11723:6:0:[10947.1,10440.0,10683.1,11721.1,10677.1,11722.2]:: -> p(n8,n9,n4),p(n8,n9,n5),p(n8,n9,n6),p(n8,n9,n7),p(n8,n9,n8),p(n8,n9,n9)
% 2.28/1.05 11720:5:0:[10798.1,10439.0,10682.1,11717.1,10676.1,11718.2,10795.1,11719.5]:: -> p(n8,n8,n4),p(n8,n8,n5),p(n8,n8,n7),p(n8,n8,n8),p(n8,n8,n9)
% 2.28/1.05 11716:5:0:[10681.0,10437.1,10673.1,11713.2,10944.1,11714.6,10761.1,11715.7]:: -> p(n8,n6,n1),p(n8,n6,n4),p(n8,n6,n5),p(n8,n6,n6),p(n8,n6,n9)
% 2.28/1.05 11712:4:0:[10680.0,10436.1,10672.1,11708.2,10747.1,11709.3,10751.1,11710.4,10943.1,11711.6]:: -> p(n8,n5,n1),p(n8,n5,n6),p(n8,n5,n8),p(n8,n5,n9)
% 2.28/1.05 11707:5:0:[10679.0,10435.1,10671.1,11704.2,10724.1,11705.5,10736.1,11706.6]:: -> p(n8,n4,n1),p(n8,n4,n4),p(n8,n4,n5),p(n8,n4,n8),p(n8,n4,n9)
% 2.28/1.05 10576:1:0:[10534.0,485.1]:: p(n2,n3,n8) ->
% 2.28/1.05 10577:1:0:[10535.0,491.1]:: p(n2,n3,n5) ->
% 2.28/1.05 11703:6:0:[10678.0,10434.1,10670.1,11701.2,10716.1,11702.6]:: -> p(n8,n3,n1),p(n8,n3,n4),p(n8,n3,n5),p(n8,n3,n6),p(n8,n3,n8),p(n8,n3,n9)
% 2.28/1.05 11700:5:0:[10690.1,10432.0,10669.0,11697.1,10668.0,11698.2,10697.1,11699.8]:: -> p(n8,n1,n4),p(n8,n1,n5),p(n8,n1,n6),p(n8,n1,n7),p(n8,n1,n8)
% 2.28/1.05 11696:6:0:[10667.1,10431.0,10950.0,11694.1,10663.1,11695.6]:: -> p(n7,n9,n3),p(n7,n9,n4),p(n7,n9,n5),p(n7,n9,n6),p(n7,n9,n8),p(n7,n9,n9)
% 2.28/1.05 11693:4:0:[10666.0,10429.0,10784.0,11689.1,10780.1,11690.2,10774.1,11691.4,10660.1,11692.6]:: -> p(n7,n7,n4),p(n7,n7,n6),p(n7,n7,n8),p(n7,n7,n9)
% 2.28/1.05 11688:5:0:[10665.0,10428.0,10765.1,11685.2,10659.1,11686.6,10760.1,11687.7]:: -> p(n7,n6,n2),p(n7,n6,n4),p(n7,n6,n5),p(n7,n6,n6),p(n7,n6,n9)
% 2.28/1.05 10578:1:0:[10534.0,530.1]:: p(n2,n4,n8) ->
% 2.28/1.05 10579:1:0:[10535.0,536.1]:: p(n2,n4,n5) ->
% 2.28/1.05 11684:5:0:[10664.0,10427.0,10746.1,11681.3,10750.1,11682.4,10658.1,11683.6]:: -> p(n7,n5,n2),p(n7,n5,n3),p(n7,n5,n6),p(n7,n5,n8),p(n7,n5,n9)
% 2.28/1.05 11680:6:0:[10657.0,10425.0,10940.0,11678.2,10656.0,11679.6]:: -> p(n7,n3,n2),p(n7,n3,n4),p(n7,n3,n5),p(n7,n3,n6),p(n7,n3,n8),p(n7,n3,n9)
% 2.28/1.05 11677:5:0:[10655.0,10424.0,10705.1,11674.1,10709.0,11675.2,10654.0,11676.6]:: -> p(n7,n2,n4),p(n7,n2,n5),p(n7,n2,n6),p(n7,n2,n8),p(n7,n2,n9)
% 2.28/1.05 11673:5:0:[10653.0,10423.0,10939.0,11670.2,10652.0,11671.6,10696.1,11672.8]:: -> p(n7,n1,n2),p(n7,n1,n4),p(n7,n1,n5),p(n7,n1,n6),p(n7,n1,n8)
% 2.28/1.05 11669:6:0:[10651.1,10422.2,10648.1,11667.4,10938.1,11668.5]:: -> p(n6,n9,n1),p(n6,n9,n2),p(n6,n9,n4),p(n6,n9,n7),p(n6,n9,n8),p(n6,n9,n9)
% 2.28/1.05 10580:1:0:[10534.0,566.1]:: p(n2,n5,n8) ->
% 2.28/1.05 10581:1:0:[10535.0,572.1]:: p(n2,n5,n5) ->
% 2.28/1.05 11666:5:0:[10797.0,10421.0,10650.1,11663.2,10647.1,11664.4,10792.1,11665.5]:: -> p(n6,n8,n2),p(n6,n8,n4),p(n6,n8,n7),p(n6,n8,n8),p(n6,n8,n9)
% 2.28/1.05 11662:5:0:[10783.0,10420.1,10649.1,11659.2,10646.1,11660.4,10937.1,11661.5]:: -> p(n6,n7,n1),p(n6,n7,n4),p(n6,n7,n7),p(n6,n7,n8),p(n6,n7,n9)
% 2.28/1.05 11658:3:0:[10730.1,10417.1,10643.0,11653.2,10929.1,11654.3,10642.0,11655.4,10722.1,11656.5,10735.0,11657.6]:: -> p(n6,n4,n1),p(n6,n4,n8),p(n6,n4,n9)
% 2.28/1.05 11652:5:0:[10641.0,10416.2,10640.0,11649.4,10715.1,11650.6,10924.1,11651.8]:: -> p(n6,n3,n1),p(n6,n3,n2),p(n6,n3,n4),p(n6,n3,n6),p(n6,n3,n8)
% 2.28/1.05 11648:5:0:[10704.1,10415.1,10639.0,11645.2,10638.0,11646.4,10923.1,11647.8]:: -> p(n6,n2,n1),p(n6,n2,n4),p(n6,n2,n6),p(n6,n2,n7),p(n6,n2,n8)
% 2.28/1.05 10582:1:0:[10535.0,599.1]:: p(n2,n6,n5) ->
% 2.28/1.05 10583:1:0:[10534.0,602.0]:: p(n2,n7,n8) ->
% 2.28/1.05 11644:5:0:[10689.1,10414.0,10637.0,11641.2,10636.0,11642.4,10695.1,11643.8]:: -> p(n6,n1,n2),p(n6,n1,n4),p(n6,n1,n6),p(n6,n1,n7),p(n6,n1,n8)
% 2.28/1.05 10584:1:0:[10534.0,611.0]:: p(n2,n8,n8) ->
% 2.28/1.05 11640:7:0:[10635.1,10413.5,10628.1,11639.8]:: -> p(n5,n9,n1),p(n5,n9,n2),p(n5,n9,n3),p(n5,n9,n4),p(n5,n9,n5),p(n5,n9,n7),p(n5,n9,n8)
% 2.28/1.05 10585:1:0:[10534.0,620.0]:: p(n2,n9,n8) ->
% 2.28/1.05 10586:1:0:[10535.0,626.0]:: p(n2,n8,n5) ->
% 2.28/1.05 11638:4:0:[10782.0,10411.1,10779.1,11634.2,10773.1,11635.4,10634.0,11636.5,10625.1,11637.8]:: -> p(n5,n7,n1),p(n5,n7,n4),p(n5,n7,n7),p(n5,n7,n8)
% 2.28/1.05 10587:1:0:[10535.0,635.0]:: p(n2,n9,n5) ->
% 2.28/1.05 11633:2:0:[10926.1,10410.1,10764.0,11627.2,10928.1,11628.3,10934.0,11629.4,10633.0,11630.5,10757.1,11631.7,10624.1,11632.8]:: -> p(n5,n6,n1),p(n5,n6,n7)
% 2.28/1.05 11626:3:0:[10925.1,10409.1,10933.0,11621.2,10743.1,11622.3,10749.0,11623.4,10632.0,11624.5,10623.1,11625.8]:: -> p(n5,n5,n1),p(n5,n5,n7),p(n5,n5,n8)
% 2.28/1.05 11620:2:0:[10729.1,10408.1,10932.0,11614.2,10927.1,11615.3,10931.0,11616.4,10631.0,11617.5,10734.0,11618.6,10622.1,11619.8]:: -> p(n5,n4,n1),p(n5,n4,n8)
% 2.28/1.05 10588:1:0:[10536.0,650.1]:: p(n3,n1,n2) ->
% 2.28/1.05 11613:6:0:[10630.0,10407.5,10714.1,11611.6,10621.1,11612.8]:: -> p(n5,n3,n1),p(n5,n3,n2),p(n5,n3,n3),p(n5,n3,n4),p(n5,n3,n5),p(n5,n3,n8)
% 2.28/1.05 11610:5:0:[10703.1,10406.1,10708.0,11607.2,10629.0,11608.5,10620.1,11609.8]:: -> p(n5,n2,n1),p(n5,n2,n4),p(n5,n2,n5),p(n5,n2,n7),p(n5,n2,n8)
% 2.28/1.05 11606:6:0:[10615.1,10404.1,10619.1,11604.3,10936.0,11605.5]:: -> p(n4,n9,n1),p(n4,n9,n3),p(n4,n9,n5),p(n4,n9,n7),p(n4,n9,n8),p(n4,n9,n9)
% 2.28/1.05 11603:5:0:[10791.0,10403.0,10614.1,11600.1,10618.1,11601.3,10790.0,11602.5]:: -> p(n4,n8,n3),p(n4,n8,n5),p(n4,n8,n7),p(n4,n8,n8),p(n4,n8,n9)
% 2.28/1.05 11599:4:0:[10613.1,10402.1,10778.1,11595.2,10617.1,11596.3,10772.1,11597.4,10935.0,11598.5]:: -> p(n4,n7,n1),p(n4,n7,n7),p(n4,n7,n8),p(n4,n7,n9)
% 2.28/1.05 10589:1:0:[10537.0,696.1]:: p(n3,n1,n3) ->
% 2.28/1.05 11594:4:0:[10612.1,10401.1,10763.0,11590.2,10616.1,11591.3,10930.0,11592.4,10756.1,11593.7]:: -> p(n4,n6,n1),p(n4,n6,n6),p(n4,n6,n7),p(n4,n6,n9)
% 2.28/1.05 11589:5:0:[10608.0,10398.1,10609.0,11586.3,10713.1,11587.6,10922.0,11588.8]:: -> p(n4,n3,n1),p(n4,n3,n3),p(n4,n3,n5),p(n4,n3,n6),p(n4,n3,n8)
% 2.28/1.05 11585:5:0:[10606.0,10397.1,10707.0,11582.2,10607.0,11583.3,10921.0,11584.8]:: -> p(n4,n2,n1),p(n4,n2,n5),p(n4,n2,n6),p(n4,n2,n7),p(n4,n2,n8)
% 2.28/1.05 11581:5:0:[10686.1,10396.0,10604.0,11578.1,10605.0,11579.3,10694.0,11580.8]:: -> p(n4,n1,n3),p(n4,n1,n5),p(n4,n1,n6),p(n4,n1,n7),p(n4,n1,n8)
% 2.28/1.05 10590:1:0:[10536.0,722.0]:: p(n3,n3,n2) ->
% 2.28/1.05 10591:1:0:[10536.0,731.0]:: p(n3,n4,n2) ->
% 2.28/1.05 10592:1:0:[10536.0,740.0]:: p(n3,n5,n2) ->
% 2.28/1.05 10593:1:0:[10536.0,749.0]:: p(n3,n6,n2) ->
% 2.28/1.05 10594:1:0:[10536.0,758.0]:: p(n3,n7,n2) ->
% 2.28/1.05 10595:1:0:[10537.0,759.1]:: p(n3,n2,n3) ->
% 2.28/1.05 10596:1:0:[10536.0,767.0]:: p(n3,n8,n2) ->
% 2.28/1.05 11577:6:0:[10597.1,10395.1,10603.1,11575.2,10918.1,11576.4]:: -> p(n3,n9,n1),p(n3,n9,n4),p(n3,n9,n6),p(n3,n9,n7),p(n3,n9,n8),p(n3,n9,n9)
% 2.28/1.05 10597:1:0:[10536.0,776.0]:: p(n3,n9,n2) ->
% 2.28/1.05 11574:4:0:[10789.0,10394.0,10596.1,11570.1,10602.1,11571.2,10917.1,11572.4,10788.0,11573.5]:: -> p(n3,n8,n4),p(n3,n8,n7),p(n3,n8,n8),p(n3,n8,n9)
% 2.28/1.05 11569:5:0:[10593.1,10392.1,10601.0,11566.2,10909.1,11567.5,10755.1,11568.7]:: -> p(n3,n6,n1),p(n3,n6,n4),p(n3,n6,n5),p(n3,n6,n7),p(n3,n6,n9)
% 2.28/1.05 11565:3:0:[10592.1,10391.1,10600.0,11560.2,10741.0,11561.3,10742.0,11562.4,10908.1,11563.5,10912.1,11564.7]:: -> p(n3,n5,n1),p(n3,n5,n7),p(n3,n5,n9)
% 2.28/1.05 11559:4:0:[10591.1,10390.1,10599.0,11555.2,10719.1,11556.5,10728.0,11557.6,10911.1,11558.7]:: -> p(n3,n4,n1),p(n3,n4,n4),p(n3,n4,n5),p(n3,n4,n9)
% 2.28/1.05 11554:5:0:[10901.1,10389.0,10590.1,11551.1,10598.0,11552.2,10712.1,11553.6]:: -> p(n3,n3,n4),p(n3,n3,n5),p(n3,n3,n6),p(n3,n3,n8),p(n3,n3,n9)
% 2.28/1.05 10598:1:0:[10537.0,813.1]:: p(n3,n3,n3) ->
% 2.28/1.05 11550:4:0:[10685.1,10387.0,10588.0,11546.1,10589.0,11547.2,10904.1,11548.6,10693.0,11549.8]:: -> p(n3,n1,n4),p(n3,n1,n5),p(n3,n1,n6),p(n3,n1,n8)
% 2.28/1.05 11545:6:0:[10920.0,10386.2,10587.1,11543.4,10585.1,11544.7]:: -> p(n2,n9,n1),p(n2,n9,n2),p(n2,n9,n4),p(n2,n9,n6),p(n2,n9,n7),p(n2,n9,n9)
% 2.28/1.05 11542:4:0:[10787.0,10385.0,10919.0,11538.2,10586.1,11539.4,10786.0,11540.5,10584.1,11541.7]:: -> p(n2,n8,n2),p(n2,n8,n4),p(n2,n8,n7),p(n2,n8,n9)
% 2.28/1.05 11537:5:0:[10740.0,10382.3,10581.0,11534.4,10907.1,11535.5,10580.0,11536.7]:: -> p(n2,n5,n1),p(n2,n5,n2),p(n2,n5,n3),p(n2,n5,n7),p(n2,n5,n9)
% 2.28/1.05 11533:4:0:[10726.0,10381.1,10579.0,11529.4,10718.1,11530.5,10727.0,11531.6,10578.0,11532.7]:: -> p(n2,n4,n1),p(n2,n4,n3),p(n2,n4,n4),p(n2,n4,n9)
% 2.28/1.05 11528:4:0:[10900.1,10380.0,10906.0,11524.1,10577.0,11525.4,10711.1,11526.6,10576.0,11527.7]:: -> p(n2,n3,n3),p(n2,n3,n4),p(n2,n3,n6),p(n2,n3,n9)
% 2.28/1.05 11523:3:0:[10899.1,10379.0,10701.0,11518.1,10702.0,11519.2,10575.0,11520.4,10903.1,11521.6,10574.0,11522.7]:: -> p(n2,n2,n4),p(n2,n2,n6),p(n2,n2,n9)
% 2.28/1.05 10599:1:0:[10537.0,858.1]:: p(n3,n4,n3) ->
% 2.28/1.05 11517:3:0:[10684.1,10378.0,10905.0,11512.1,10573.0,11513.4,10902.1,11514.6,10572.0,11515.7,10692.0,11516.8]:: -> p(n2,n1,n3),p(n2,n1,n4),p(n2,n1,n6)
% 2.28/1.05 11511:4:0:[10557.1,10377.0,10916.0,11507.2,10915.0,11508.4,10571.1,11509.5,10566.1,11510.6]:: -> p(n1,n9,n2),p(n1,n9,n4),p(n1,n9,n8),p(n1,n9,n9)
% 2.28/1.05 11506:4:0:[10556.1,10376.0,10914.0,11502.2,10913.0,11503.4,10570.1,11504.5,10565.1,11505.6]:: -> p(n1,n8,n2),p(n1,n8,n4),p(n1,n8,n8),p(n1,n8,n9)
% 2.28/1.05 11501:3:0:[10555.1,10375.0,10769.0,11496.1,10768.0,11497.2,10767.0,11498.4,10569.1,11499.5,10564.1,11500.6]:: -> p(n1,n7,n4),p(n1,n7,n8),p(n1,n7,n9)
% 2.28/1.05 11495:4:0:[10554.1,10374.0,10754.0,11491.2,10568.1,11492.5,10563.1,11493.6,10753.0,11494.7]:: -> p(n1,n6,n2),p(n1,n6,n4),p(n1,n6,n5),p(n1,n6,n9)
% 2.28/1.05 11490:4:0:[10548.1,10370.0,10699.0,11486.1,10700.0,11487.2,10559.0,11488.5,10558.0,11489.6]:: -> p(n1,n2,n4),p(n1,n2,n5),p(n1,n2,n8),p(n1,n2,n9)
% 2.28/1.05 10600:1:0:[10537.0,894.1]:: p(n3,n5,n3) ->
% 2.28/1.05 11485:8:0:[10628.1,10368.4]:: -> p(n1,n9,n9),p(n2,n9,n9),p(n3,n9,n9),p(n4,n9,n9),p(n6,n9,n9),p(n7,n9,n9),p(n8,n9,n9),p(n9,n9,n9)
% 2.28/1.05 11484:8:0:[10585.1,10367.1]:: -> p(n1,n9,n8),p(n3,n9,n8),p(n4,n9,n8),p(n5,n9,n8),p(n6,n9,n8),p(n7,n9,n8),p(n8,n9,n8),p(n9,n9,n8)
% 2.28/1.05 11483:7:0:[10566.1,10366.0,10663.1,11482.6]:: -> p(n2,n9,n7),p(n3,n9,n7),p(n4,n9,n7),p(n5,n9,n7),p(n6,n9,n7),p(n8,n9,n7),p(n9,n9,n7)
% 2.28/1.05 11481:5:0:[10571.1,10365.0,10936.0,11478.3,10635.1,11479.4,10938.1,11480.5]:: -> p(n2,n9,n6),p(n3,n9,n6),p(n7,n9,n6),p(n8,n9,n6),p(n9,n9,n6)
% 2.28/1.05 11477:5:0:[10915.0,10364.0,10587.1,11474.1,10918.1,11475.2,10648.1,11476.5]:: -> p(n4,n9,n5),p(n5,n9,n5),p(n7,n9,n5),p(n8,n9,n5),p(n9,n9,n5)
% 2.28/1.05 10601:1:0:[10537.0,921.1]:: p(n3,n6,n3) ->
% 2.28/1.05 11473:8:0:[10619.1,10363.3]:: -> p(n1,n9,n4),p(n2,n9,n4),p(n3,n9,n4),p(n5,n9,n4),p(n6,n9,n4),p(n7,n9,n4),p(n8,n9,n4),p(n9,n9,n4)
% 2.28/1.05 11472:4:0:[10916.0,10362.0,10920.0,11468.1,10603.1,11469.2,10651.1,11470.5,10677.1,11471.7]:: -> p(n4,n9,n3),p(n5,n9,n3),p(n7,n9,n3),p(n9,n9,n3)
% 2.28/1.05 11467:4:0:[10597.1,10361.2,10615.1,11463.3,10950.0,11464.6,10683.1,11465.7,10952.1,11466.8]:: -> p(n1,n9,n2),p(n2,n9,n2),p(n5,n9,n2),p(n6,n9,n2)
% 2.28/1.05 11462:5:0:[10557.1,10360.0,10667.1,11459.6,10947.1,11460.7,10949.1,11461.8]:: -> p(n2,n9,n1),p(n3,n9,n1),p(n4,n9,n1),p(n5,n9,n1),p(n6,n9,n1)
% 2.28/1.05 11458:7:0:[10627.1,10359.4,10885.1,11457.6]:: -> p(n1,n8,n9),p(n2,n8,n9),p(n3,n8,n9),p(n4,n8,n9),p(n6,n8,n9),p(n8,n8,n9),p(n9,n8,n9)
% 2.28/1.05 10602:1:0:[10537.0,948.0]:: p(n3,n8,n3) ->
% 2.28/1.05 11456:6:0:[10584.1,10358.1,10862.1,11454.4,10884.1,11455.6]:: -> p(n1,n8,n8),p(n3,n8,n8),p(n4,n8,n8),p(n6,n8,n8),p(n8,n8,n8),p(n9,n8,n8)
% 2.28/1.05 10603:1:0:[10537.0,957.0]:: p(n3,n9,n3) ->
% 2.28/1.05 11453:6:0:[10565.1,10357.0,10861.1,11451.4,10662.1,11452.6]:: -> p(n2,n8,n7),p(n3,n8,n7),p(n4,n8,n7),p(n6,n8,n7),p(n8,n8,n7),p(n9,n8,n7)
% 2.28/1.05 11450:3:0:[10913.0,10355.0,10586.1,11445.1,10917.1,11446.2,10860.0,11447.4,10647.1,11448.5,10883.1,11449.6]:: -> p(n4,n8,n5),p(n8,n8,n5),p(n9,n8,n5)
% 2.28/1.05 10604:1:0:[10538.0,992.1]:: p(n4,n1,n2) ->
% 2.28/1.05 11444:6:0:[10618.1,10354.3,10859.0,11442.4,10882.1,11443.6]:: -> p(n1,n8,n4),p(n2,n8,n4),p(n3,n8,n4),p(n6,n8,n4),p(n8,n8,n4),p(n9,n8,n4)
% 2.28/1.05 10605:1:0:[10539.0,1003.1]:: p(n4,n1,n4) ->
% 2.28/1.05 11441:2:0:[10914.0,10353.0,10919.0,11435.1,10602.1,11436.2,10858.0,11437.4,10650.1,11438.5,10881.1,11439.6,10676.1,11440.7]:: -> p(n4,n8,n3),p(n9,n8,n3)
% 2.28/1.05 11434:3:0:[10596.1,10352.2,10614.1,11429.3,10857.0,11430.4,10880.1,11431.6,10682.1,11432.7,10951.1,11433.8]:: -> p(n1,n8,n2),p(n2,n8,n2),p(n6,n8,n2)
% 2.28/1.05 11428:5:0:[10826.1,10350.1,10839.1,11425.2,10625.1,11426.4,10898.1,11427.7]:: -> p(n1,n7,n9),p(n4,n7,n9),p(n6,n7,n9),p(n7,n7,n9),p(n9,n7,n9)
% 2.28/1.05 11424:6:0:[10583.1,10349.1,10838.1,11422.2,10897.1,11423.7]:: -> p(n1,n7,n8),p(n4,n7,n8),p(n5,n7,n8),p(n6,n7,n8),p(n7,n7,n8),p(n9,n7,n8)
% 2.28/1.05 11421:4:0:[10564.1,10348.0,10825.1,11417.1,10837.1,11418.2,10660.1,11419.6,10896.1,11420.7]:: -> p(n4,n7,n7),p(n5,n7,n7),p(n6,n7,n7),p(n9,n7,n7)
% 2.28/1.05 11416:2:0:[10569.1,10347.0,10824.1,11410.1,10836.1,11411.2,10935.0,11412.3,10634.0,11413.4,10937.1,11414.5,10895.1,11415.7]:: -> p(n7,n7,n6),p(n9,n7,n6)
% 2.28/1.05 11409:5:0:[10823.0,10345.1,10835.1,11406.2,10617.1,11407.3,10894.1,11408.7]:: -> p(n1,n7,n4),p(n5,n7,n4),p(n6,n7,n4),p(n7,n7,n4),p(n9,n7,n4)
% 2.28/1.05 11405:3:0:[10555.1,10342.0,10822.0,11400.1,10834.0,11401.2,10666.0,11402.6,10893.0,11403.7,10948.1,11404.8]:: -> p(n4,n7,n1),p(n5,n7,n1),p(n6,n7,n1)
% 2.28/1.05 10606:1:0:[10538.0,1055.1]:: p(n4,n2,n2) ->
% 2.28/1.05 11399:6:0:[10821.1,10341.1,10624.1,11397.4,10874.1,11398.5]:: -> p(n1,n6,n9),p(n3,n6,n9),p(n4,n6,n9),p(n7,n6,n9),p(n8,n6,n9),p(n9,n6,n9)
% 2.28/1.05 10607:1:0:[10539.0,1066.1]:: p(n4,n2,n4) ->
% 2.28/1.05 11396:3:0:[10563.1,10339.0,10820.0,11391.1,10873.1,11392.5,10659.1,11393.6,10944.1,11394.7,10946.1,11395.8]:: -> p(n3,n6,n7),p(n4,n6,n7),p(n5,n6,n7)
% 2.28/1.05 11390:4:0:[10568.1,10338.0,10819.0,11386.1,10909.1,11387.2,10633.0,11388.4,10872.1,11389.5]:: -> p(n4,n6,n6),p(n7,n6,n6),p(n8,n6,n6),p(n9,n6,n6)
% 2.28/1.05 11385:5:0:[10582.0,10337.1,10930.0,11382.3,10934.0,11383.4,10645.1,11384.5]:: -> p(n1,n6,n5),p(n3,n6,n5),p(n7,n6,n5),p(n8,n6,n5),p(n9,n6,n5)
% 2.28/1.05 11381:5:0:[10818.0,10336.1,10616.1,11378.3,10928.1,11379.4,10871.1,11380.5]:: -> p(n1,n6,n4),p(n3,n6,n4),p(n7,n6,n4),p(n8,n6,n4),p(n9,n6,n4)
% 2.28/1.05 11377:3:0:[10817.0,10334.1,10593.1,11372.2,10612.1,11373.3,10926.1,11374.4,10870.0,11375.5,10681.0,11376.7]:: -> p(n1,n6,n2),p(n7,n6,n2),p(n9,n6,n2)
% 2.28/1.05 11371:5:0:[10554.1,10333.0,10816.0,11368.1,10869.0,11369.5,10665.0,11370.6]:: -> p(n3,n6,n1),p(n4,n6,n1),p(n5,n6,n1),p(n8,n6,n1),p(n9,n6,n1)
% 2.28/1.05 11367:6:0:[10850.1,10332.3,10623.1,11365.4,10868.1,11366.5]:: -> p(n1,n5,n9),p(n2,n5,n9),p(n3,n5,n9),p(n7,n5,n9),p(n8,n5,n9),p(n9,n5,n9)
% 2.28/1.05 11364:4:0:[10910.0,10331.0,10580.0,11360.1,10912.1,11361.2,10849.1,11362.3,10867.1,11363.5]:: -> p(n5,n5,n8),p(n7,n5,n8),p(n8,n5,n8),p(n9,n5,n8)
% 2.28/1.05 10608:1:0:[10538.0,1109.1]:: p(n4,n3,n2) ->
% 2.28/1.05 11359:3:0:[10562.1,10330.0,10848.1,11354.3,10866.1,11355.5,10658.1,11356.6,10943.1,11357.7,10945.1,11358.8]:: -> p(n2,n5,n7),p(n3,n5,n7),p(n5,n5,n7)
% 2.28/1.05 10609:1:0:[10539.0,1120.1]:: p(n4,n3,n4) ->
% 2.28/1.05 11353:3:0:[10567.1,10329.0,10907.1,11348.1,10908.1,11349.2,10847.1,11350.3,10632.0,11351.4,10865.1,11352.5]:: -> p(n7,n5,n6),p(n8,n5,n6),p(n9,n5,n6)
% 2.28/1.05 11347:4:0:[10592.1,10325.2,10610.1,11343.3,10925.1,11344.4,10864.0,11345.5,10680.0,11346.7]:: -> p(n1,n5,n2),p(n2,n5,n2),p(n7,n5,n2),p(n9,n5,n2)
% 2.28/1.05 11342:5:0:[10553.1,10324.0,10845.0,11339.3,10863.0,11340.5,10664.0,11341.6]:: -> p(n2,n5,n1),p(n3,n5,n1),p(n5,n5,n1),p(n8,n5,n1),p(n9,n5,n1)
% 2.28/1.05 11338:5:0:[10815.1,10323.0,10844.1,11335.3,10622.1,11336.4,10879.1,11337.6]:: -> p(n2,n4,n9),p(n3,n4,n9),p(n6,n4,n9),p(n8,n4,n9),p(n9,n4,n9)
% 2.28/1.05 11334:4:0:[10814.1,10322.0,10578.0,11330.1,10911.1,11331.2,10843.1,11332.3,10878.1,11333.6]:: -> p(n5,n4,n8),p(n6,n4,n8),p(n8,n4,n8),p(n9,n4,n8)
% 2.28/1.05 11329:3:0:[10813.0,10319.0,10579.0,11324.1,10842.1,11325.3,10931.0,11326.4,10642.0,11327.5,10877.0,11328.6]:: -> p(n3,n4,n5),p(n8,n4,n5),p(n9,n4,n5)
% 2.28/1.05 11323:4:0:[10812.0,10318.0,10611.0,11319.3,10927.1,11320.4,10929.1,11321.5,10876.0,11322.6]:: -> p(n2,n4,n4),p(n3,n4,n4),p(n8,n4,n4),p(n9,n4,n4)
% 2.28/1.05 11318:2:0:[10811.0,10317.0,10599.0,11312.2,10841.1,11313.3,10932.0,11314.4,10643.0,11315.5,10875.0,11316.6,10671.1,11317.7]:: -> p(n2,n4,n3),p(n9,n4,n3)
% 2.28/1.05 10610:1:0:[10538.0,1163.0]:: p(n4,n5,n2) ->
% 2.28/1.05 10611:1:0:[10539.0,1165.1]:: p(n4,n4,n4) ->
% 2.28/1.05 10612:1:0:[10538.0,1172.0]:: p(n4,n6,n2) ->
% 2.28/1.05 11311:6:0:[10551.1,10315.0,10840.0,11309.3,10661.0,11310.6]:: -> p(n2,n4,n1),p(n3,n4,n1),p(n5,n4,n1),p(n6,n4,n1),p(n8,n4,n1),p(n9,n4,n1)
% 2.28/1.05 10613:1:0:[10538.0,1181.0]:: p(n4,n7,n2) ->
% 2.28/1.05 11308:5:0:[10810.1,10314.0,10922.0,11305.3,10621.1,11306.4,10924.1,11307.5]:: -> p(n2,n3,n9),p(n3,n3,n9),p(n7,n3,n9),p(n8,n3,n9),p(n9,n3,n9)
% 2.28/1.05 10614:1:0:[10538.0,1190.0]:: p(n4,n8,n2) ->
% 2.28/1.05 11304:7:0:[10809.1,10313.0,10576.0,11303.1]:: -> p(n3,n3,n8),p(n4,n3,n8),p(n5,n3,n8),p(n6,n3,n8),p(n7,n3,n8),p(n8,n3,n8),p(n9,n3,n8)
% 2.28/1.05 10615:1:0:[10538.0,1199.0]:: p(n4,n9,n2) ->
% 2.28/1.05 11302:7:0:[10560.0,10311.0,10630.0,11301.4]:: -> p(n2,n3,n6),p(n3,n3,n6),p(n4,n3,n6),p(n6,n3,n6),p(n7,n3,n6),p(n8,n3,n6),p(n9,n3,n6)
% 2.28/1.05 11300:6:0:[10808.0,10310.0,10577.0,11298.1,10640.0,11299.5]:: -> p(n3,n3,n5),p(n4,n3,n5),p(n5,n3,n5),p(n7,n3,n5),p(n8,n3,n5),p(n9,n3,n5)
% 2.28/1.05 10616:1:0:[10539.0,1210.0]:: p(n4,n6,n4) ->
% 2.28/1.05 11297:7:0:[10807.0,10309.0,10609.0,11296.3]:: -> p(n2,n3,n4),p(n3,n3,n4),p(n5,n3,n4),p(n6,n3,n4),p(n7,n3,n4),p(n8,n3,n4),p(n9,n3,n4)
% 2.28/1.05 10617:1:0:[10539.0,1219.0]:: p(n4,n7,n4) ->
% 2.28/1.05 11295:3:0:[10806.0,10308.0,10598.0,11290.2,10641.0,11291.5,10940.0,11292.6,10670.1,11293.7,10942.1,11294.8]:: -> p(n2,n3,n3),p(n4,n3,n3),p(n5,n3,n3)
% 2.28/1.05 10618:1:0:[10539.0,1228.0]:: p(n4,n8,n4) ->
% 2.28/1.05 11289:4:0:[10805.0,10307.0,10906.0,11285.1,10590.1,11286.2,10608.0,11287.3,10678.0,11288.7]:: -> p(n5,n3,n2),p(n6,n3,n2),p(n7,n3,n2),p(n9,n3,n2)
% 2.28/1.05 10619:1:0:[10539.0,1237.0]:: p(n4,n9,n4) ->
% 2.28/1.05 11284:5:0:[10549.1,10306.0,10900.1,11281.1,10901.1,11282.2,10657.0,11283.6]:: -> p(n4,n3,n1),p(n5,n3,n1),p(n6,n3,n1),p(n8,n3,n1),p(n9,n3,n1)
% 2.28/1.05 11280:4:0:[10833.1,10305.2,10921.0,11276.3,10620.1,11277.4,10923.1,11278.5,10892.1,11279.7]:: -> p(n1,n2,n9),p(n2,n2,n9),p(n7,n2,n9),p(n9,n2,n9)
% 2.28/1.05 11275:6:0:[10574.0,10304.1,10832.1,11273.2,10891.1,11274.7]:: -> p(n1,n2,n8),p(n4,n2,n8),p(n5,n2,n8),p(n6,n2,n8),p(n7,n2,n8),p(n9,n2,n8)
% 2.28/1.05 11272:4:0:[10558.0,10303.0,10903.1,11268.1,10831.1,11269.2,10654.0,11270.6,10890.1,11271.7]:: -> p(n4,n2,n7),p(n5,n2,n7),p(n6,n2,n7),p(n9,n2,n7)
% 2.28/1.05 11267:5:0:[10559.0,10302.0,10830.1,11264.2,10629.0,11265.4,10889.1,11266.7]:: -> p(n2,n2,n6),p(n4,n2,n6),p(n6,n2,n6),p(n7,n2,n6),p(n9,n2,n6)
% 2.28/1.05 11263:5:0:[10575.0,10301.1,10829.1,11260.2,10638.0,11261.5,10888.1,11262.7]:: -> p(n1,n2,n5),p(n4,n2,n5),p(n5,n2,n5),p(n7,n2,n5),p(n9,n2,n5)
% 2.28/1.05 11259:6:0:[10828.1,10300.2,10607.0,11257.3,10887.1,11258.7]:: -> p(n1,n2,n4),p(n2,n2,n4),p(n5,n2,n4),p(n6,n2,n4),p(n7,n2,n4),p(n9,n2,n4)
% 2.28/1.05 11256:4:0:[10548.1,10297.0,10899.1,11252.1,10827.0,11253.2,10655.0,11254.6,10886.0,11255.7]:: -> p(n4,n2,n1),p(n5,n2,n1),p(n6,n2,n1),p(n9,n2,n1)
% 2.28/1.05 11251:6:0:[10804.1,10295.0,10572.0,11249.1,10856.0,11250.4]:: -> p(n3,n1,n8),p(n4,n1,n8),p(n6,n1,n8),p(n7,n1,n8),p(n8,n1,n8),p(n9,n1,n8)
% 2.28/1.05 11248:4:0:[10550.0,10294.0,10902.1,11244.1,10904.1,11245.2,10855.0,11246.4,10652.0,11247.6]:: -> p(n4,n1,n7),p(n6,n1,n7),p(n8,n1,n7),p(n9,n1,n7)
% 2.28/1.05 11243:7:0:[10552.0,10293.0,10626.0,11242.4]:: -> p(n2,n1,n6),p(n3,n1,n6),p(n4,n1,n6),p(n6,n1,n6),p(n7,n1,n6),p(n8,n1,n6),p(n9,n1,n6)
% 2.28/1.05 11241:5:0:[10803.1,10292.0,10573.0,11238.1,10854.0,11239.4,10636.0,11240.5]:: -> p(n3,n1,n5),p(n4,n1,n5),p(n7,n1,n5),p(n8,n1,n5),p(n9,n1,n5)
% 2.28/1.05 10620:1:0:[10540.0,1305.0]:: p(n5,n2,n9) ->
% 2.28/1.05 10621:1:0:[10540.0,1314.0]:: p(n5,n3,n9) ->
% 2.28/1.05 10622:1:0:[10540.0,1323.0]:: p(n5,n4,n9) ->
% 2.28/1.05 10623:1:0:[10540.0,1332.0]:: p(n5,n5,n9) ->
% 2.28/1.05 10624:1:0:[10540.0,1341.0]:: p(n5,n6,n9) ->
% 2.28/1.05 10625:1:0:[10540.0,1350.0]:: p(n5,n7,n9) ->
% 2.28/1.05 10626:1:0:[10541.0,1356.1]:: p(n5,n1,n6) ->
% 2.28/1.05 10627:1:0:[10540.0,1359.0]:: p(n5,n8,n9) ->
% 2.28/1.05 11237:6:0:[10802.1,10291.0,10605.0,11235.3,10853.0,11236.4]:: -> p(n2,n1,n4),p(n3,n1,n4),p(n6,n1,n4),p(n7,n1,n4),p(n8,n1,n4),p(n9,n1,n4)
% 2.28/1.05 10628:1:0:[10540.0,1368.0]:: p(n5,n9,n9) ->
% 2.28/1.05 11234:2:0:[10801.1,10290.0,10589.0,11228.2,10852.0,11229.4,10637.0,11230.5,10939.0,11231.6,10668.0,11232.7,10941.1,11233.8]:: -> p(n2,n1,n3),p(n4,n1,n3)
% 2.28/1.05 11227:3:0:[10800.1,10289.0,10905.0,11222.1,10588.0,11223.2,10604.0,11224.3,10851.0,11225.4,10669.0,11226.7]:: -> p(n6,n1,n2),p(n7,n1,n2),p(n9,n1,n2)
% 2.28/1.05 11221:8:0:[10698.1,10287.0]:: -> p(n9,n2,n9),p(n9,n3,n9),p(n9,n4,n9),p(n9,n5,n9),p(n9,n6,n9),p(n9,n7,n9),p(n9,n8,n9),p(n9,n9,n9)
% 2.28/1.05 11220:8:0:[10762.1,10286.5]:: -> p(n9,n1,n8),p(n9,n2,n8),p(n9,n3,n8),p(n9,n4,n8),p(n9,n5,n8),p(n9,n7,n8),p(n9,n8,n8),p(n9,n9,n8)
% 2.28/1.05 11219:5:0:[10717.1,10285.2,10737.1,11216.3,10945.1,11217.4,10946.1,11218.5]:: -> p(n9,n1,n7),p(n9,n2,n7),p(n9,n7,n7),p(n9,n8,n7),p(n9,n9,n7)
% 2.28/1.05 10629:1:0:[10541.0,1419.1]:: p(n5,n2,n6) ->
% 2.28/1.05 11215:7:0:[10725.1,10284.3,10796.1,11214.7]:: -> p(n9,n1,n6),p(n9,n2,n6),p(n9,n3,n6),p(n9,n5,n6),p(n9,n6,n6),p(n9,n7,n6),p(n9,n9,n6)
% 2.28/1.05 11213:7:0:[10752.1,10283.4,10777.1,11212.6]:: -> p(n9,n1,n5),p(n9,n2,n5),p(n9,n3,n5),p(n9,n4,n5),p(n9,n6,n5),p(n9,n8,n5),p(n9,n9,n5)
% 2.28/1.05 11211:8:0:[10748.1,10282.4]:: -> p(n9,n1,n4),p(n9,n2,n4),p(n9,n3,n4),p(n9,n4,n4),p(n9,n6,n4),p(n9,n7,n4),p(n9,n8,n4),p(n9,n9,n4)
% 2.28/1.05 11210:4:0:[10941.1,10281.0,10710.1,11206.1,10942.1,11207.2,10766.1,11208.5,10781.1,11209.6]:: -> p(n9,n4,n3),p(n9,n5,n3),p(n9,n8,n3),p(n9,n9,n3)
% 2.28/1.05 11205:4:0:[10706.1,10280.1,10733.1,11201.3,10785.1,11202.6,10951.1,11203.7,10952.1,11204.8]:: -> p(n9,n1,n2),p(n9,n3,n2),p(n9,n5,n2),p(n9,n6,n2)
% 2.28/1.05 11200:5:0:[10691.1,10279.0,10948.1,11197.6,10799.1,11198.7,10949.1,11199.8]:: -> p(n9,n2,n1),p(n9,n3,n1),p(n9,n4,n1),p(n9,n5,n1),p(n9,n6,n1)
% 2.28/1.05 11196:6:0:[10697.1,10278.0,10892.1,11194.1,10898.1,11195.6]:: -> p(n8,n3,n9),p(n8,n4,n9),p(n8,n5,n9),p(n8,n6,n9),p(n8,n8,n9),p(n8,n9,n9)
% 2.28/1.05 10630:1:0:[10541.0,1473.1]:: p(n5,n3,n6) ->
% 2.28/1.05 11193:6:0:[10891.1,10277.1,10761.1,11191.5,10897.1,11192.6]:: -> p(n8,n1,n8),p(n8,n3,n8),p(n8,n4,n8),p(n8,n5,n8),p(n8,n8,n8),p(n8,n9,n8)
% 2.28/1.05 11190:3:0:[10890.1,10276.1,10716.1,11185.2,10736.1,11186.3,10943.1,11187.4,10944.1,11188.5,10896.1,11189.6]:: -> p(n8,n1,n7),p(n8,n8,n7),p(n8,n9,n7)
% 2.28/1.05 11184:5:0:[10889.1,10275.1,10724.1,11181.3,10895.1,11182.6,10795.1,11183.7]:: -> p(n8,n1,n6),p(n8,n3,n6),p(n8,n5,n6),p(n8,n6,n6),p(n8,n9,n6)
% 2.28/1.05 11180:6:0:[10888.1,10274.1,10751.1,11178.4,10776.1,11179.6]:: -> p(n8,n1,n5),p(n8,n3,n5),p(n8,n4,n5),p(n8,n6,n5),p(n8,n8,n5),p(n8,n9,n5)
% 2.28/1.05 11177:6:0:[10887.1,10273.1,10747.1,11175.4,10894.1,11176.6]:: -> p(n8,n1,n4),p(n8,n3,n4),p(n8,n4,n4),p(n8,n6,n4),p(n8,n8,n4),p(n8,n9,n4)
% 2.28/1.05 11174:4:0:[10690.1,10270.0,10886.0,11170.1,10893.0,11171.6,10798.1,11172.7,10947.1,11173.8]:: -> p(n8,n3,n1),p(n8,n4,n1),p(n8,n5,n1),p(n8,n6,n1)
% 2.28/1.05 10631:1:0:[10541.0,1518.1]:: p(n5,n4,n6) ->
% 2.28/1.05 11169:6:0:[10696.1,10269.0,10879.1,11167.3,10885.1,11168.7]:: -> p(n7,n2,n9),p(n7,n3,n9),p(n7,n5,n9),p(n7,n6,n9),p(n7,n7,n9),p(n7,n9,n9)
% 2.28/1.05 11166:6:0:[10878.1,10268.3,10760.1,11164.5,10884.1,11165.7]:: -> p(n7,n1,n8),p(n7,n2,n8),p(n7,n3,n8),p(n7,n5,n8),p(n7,n7,n8),p(n7,n9,n8)
% 2.28/1.05 11163:7:0:[10723.1,10266.3,10794.1,11162.7]:: -> p(n7,n1,n6),p(n7,n2,n6),p(n7,n3,n6),p(n7,n5,n6),p(n7,n6,n6),p(n7,n7,n6),p(n7,n9,n6)
% 2.28/1.05 11161:5:0:[10877.0,10265.3,10750.1,11158.4,10774.1,11159.6,10883.1,11160.7]:: -> p(n7,n1,n5),p(n7,n2,n5),p(n7,n3,n5),p(n7,n6,n5),p(n7,n9,n5)
% 2.28/1.05 11157:6:0:[10876.0,10264.3,10746.1,11155.4,10882.1,11156.7]:: -> p(n7,n1,n4),p(n7,n2,n4),p(n7,n3,n4),p(n7,n6,n4),p(n7,n7,n4),p(n7,n9,n4)
% 2.28/1.05 10632:1:0:[10541.0,1554.1]:: p(n5,n5,n6) ->
% 2.28/1.05 11154:2:0:[10939.0,10263.0,10709.0,11148.1,10940.0,11149.2,10875.0,11150.3,10765.1,11151.5,10780.1,11152.6,10881.1,11153.7]:: -> p(n7,n5,n3),p(n7,n9,n3)
% 2.28/1.05 11147:4:0:[10705.1,10262.1,10731.1,11143.3,10784.0,11144.6,10880.1,11145.7,10950.0,11146.8]:: -> p(n7,n1,n2),p(n7,n3,n2),p(n7,n5,n2),p(n7,n6,n2)
% 2.28/1.05 11142:4:0:[10695.1,10260.0,10923.1,11138.1,10924.1,11139.2,10868.1,11140.4,10874.1,11141.5]:: -> p(n6,n4,n9),p(n6,n7,n9),p(n6,n8,n9),p(n6,n9,n9)
% 2.28/1.05 11137:7:0:[10867.1,10259.4,10759.1,11136.5]:: -> p(n6,n1,n8),p(n6,n2,n8),p(n6,n3,n8),p(n6,n4,n8),p(n6,n7,n8),p(n6,n8,n8),p(n6,n9,n8)
% 2.28/1.05 10633:1:0:[10541.0,1581.1]:: p(n5,n6,n6) ->
% 2.28/1.05 11135:5:0:[10715.1,10258.2,10735.0,11132.3,10866.1,11133.4,10873.1,11134.5]:: -> p(n6,n1,n7),p(n6,n2,n7),p(n6,n7,n7),p(n6,n8,n7),p(n6,n9,n7)
% 2.28/1.05 11131:3:0:[10722.1,10257.3,10865.1,11126.4,10872.1,11127.5,10937.1,11128.6,10792.1,11129.7,10938.1,11130.8]:: -> p(n6,n1,n6),p(n6,n2,n6),p(n6,n3,n6)
% 2.28/1.05 11125:6:0:[10929.1,10255.3,10744.1,11123.4,10871.1,11124.5]:: -> p(n6,n1,n4),p(n6,n2,n4),p(n6,n3,n4),p(n6,n7,n4),p(n6,n8,n4),p(n6,n9,n4)
% 2.28/1.05 10634:1:0:[10541.0,1599.1]:: p(n5,n7,n6) ->
% 2.28/1.05 11122:4:0:[10704.1,10253.1,10730.1,11118.3,10864.0,11119.4,10870.0,11120.5,10783.0,11121.6]:: -> p(n6,n1,n2),p(n6,n3,n2),p(n6,n8,n2),p(n6,n9,n2)
% 2.28/1.05 11117:5:0:[10689.1,10252.0,10863.0,11114.4,10869.0,11115.5,10797.0,11116.7]:: -> p(n6,n2,n1),p(n6,n3,n1),p(n6,n4,n1),p(n6,n7,n1),p(n6,n9,n1)
% 2.28/1.05 11113:6:0:[10856.0,10250.0,10757.1,11111.5,10862.1,11112.7]:: -> p(n5,n2,n8),p(n5,n3,n8),p(n5,n4,n8),p(n5,n5,n8),p(n5,n7,n8),p(n5,n9,n8)
% 2.28/1.05 10635:1:0:[10541.0,1617.0]:: p(n5,n9,n6) ->
% 2.28/1.05 11110:5:0:[10855.0,10249.0,10714.1,11107.2,10734.0,11108.3,10861.1,11109.7]:: -> p(n5,n2,n7),p(n5,n5,n7),p(n5,n6,n7),p(n5,n7,n7),p(n5,n9,n7)
% 2.28/1.05 10636:1:0:[10542.0,1652.1]:: p(n6,n1,n5) ->
% 2.28/1.05 10637:1:0:[10543.0,1659.1]:: p(n6,n1,n3) ->
% 2.28/1.05 11106:3:0:[10854.0,10247.0,10931.0,11101.3,10749.0,11102.4,10934.0,11103.5,10773.1,11104.6,10860.0,11105.7]:: -> p(n5,n2,n5),p(n5,n3,n5),p(n5,n9,n5)
% 2.28/1.05 11100:4:0:[10853.0,10246.0,10927.1,11096.3,10743.1,11097.4,10928.1,11098.5,10859.0,11099.7]:: -> p(n5,n2,n4),p(n5,n3,n4),p(n5,n7,n4),p(n5,n9,n4)
% 2.28/1.05 11095:2:0:[10852.0,10245.0,10708.0,11089.1,10932.0,11090.3,10933.0,11091.4,10764.0,11092.5,10779.1,11093.6,10858.0,11094.7]:: -> p(n5,n3,n3),p(n5,n9,n3)
% 2.28/1.05 11088:2:0:[10851.0,10244.0,10703.1,11082.1,10729.1,11083.3,10925.1,11084.4,10926.1,11085.5,10782.0,11086.6,10857.0,11087.7]:: -> p(n5,n3,n2),p(n5,n9,n2)
% 2.28/1.05 11081:7:0:[10687.1,10243.0,10793.0,11080.7]:: -> p(n5,n2,n1),p(n5,n3,n1),p(n5,n4,n1),p(n5,n5,n1),p(n5,n6,n1),p(n5,n7,n1),p(n5,n9,n1)
% 2.28/1.05 11079:4:0:[10694.0,10242.0,10921.0,11075.1,10922.0,11076.2,10844.1,11077.3,10850.1,11078.4]:: -> p(n4,n6,n9),p(n4,n7,n9),p(n4,n8,n9),p(n4,n9,n9)
% 2.28/1.05 11074:6:0:[10843.1,10241.3,10849.1,11072.4,10756.1,11073.5]:: -> p(n4,n1,n8),p(n4,n2,n8),p(n4,n3,n8),p(n4,n7,n8),p(n4,n8,n8),p(n4,n9,n8)
% 2.28/1.05 10638:1:0:[10542.0,1715.1]:: p(n6,n2,n5) ->
% 2.28/1.05 10639:1:0:[10543.0,1722.1]:: p(n6,n2,n3) ->
% 2.28/1.05 11071:6:0:[10713.1,10240.2,10732.0,11069.3,10848.1,11070.4]:: -> p(n4,n1,n7),p(n4,n2,n7),p(n4,n6,n7),p(n4,n7,n7),p(n4,n8,n7),p(n4,n9,n7)
% 2.28/1.05 11068:4:0:[10721.1,10239.3,10847.1,11064.4,10935.0,11065.6,10790.0,11066.7,10936.0,11067.8]:: -> p(n4,n1,n6),p(n4,n2,n6),p(n4,n3,n6),p(n4,n6,n6)
% 2.28/1.05 11063:5:0:[10842.1,10238.3,10745.0,11060.4,10930.0,11061.5,10772.1,11062.6]:: -> p(n4,n1,n5),p(n4,n2,n5),p(n4,n3,n5),p(n4,n8,n5),p(n4,n9,n5)
% 2.28/1.05 11059:4:0:[10707.0,10236.1,10841.1,11055.3,10846.0,11056.4,10763.0,11057.5,10778.1,11058.6]:: -> p(n4,n1,n3),p(n4,n3,n3),p(n4,n8,n3),p(n4,n9,n3)
% 2.28/1.05 11054:5:0:[10686.1,10234.0,10840.0,11051.3,10845.0,11052.4,10791.0,11053.7]:: -> p(n4,n2,n1),p(n4,n3,n1),p(n4,n6,n1),p(n4,n7,n1),p(n4,n9,n1)
% 2.28/1.05 11050:6:0:[10693.0,10233.0,10833.1,11048.1,10839.1,11049.6]:: -> p(n3,n3,n9),p(n3,n4,n9),p(n3,n5,n9),p(n3,n6,n9),p(n3,n8,n9),p(n3,n9,n9)
% 2.28/1.05 11047:4:0:[10832.1,10232.1,10911.1,11043.3,10912.1,11044.4,10755.1,11045.5,10838.1,11046.6]:: -> p(n3,n1,n8),p(n3,n3,n8),p(n3,n8,n8),p(n3,n9,n8)
% 2.28/1.05 10640:1:0:[10542.0,1769.1]:: p(n6,n3,n5) ->
% 2.28/1.05 10641:1:0:[10543.0,1776.1]:: p(n6,n3,n3) ->
% 2.28/1.05 11042:4:0:[10904.1,10231.0,10831.1,11038.1,10712.1,11039.2,10728.0,11040.3,10837.1,11041.6]:: -> p(n3,n5,n7),p(n3,n6,n7),p(n3,n8,n7),p(n3,n9,n7)
% 2.28/1.05 11037:3:0:[10830.1,10230.1,10719.1,11032.3,10908.1,11033.4,10909.1,11034.5,10836.1,11035.6,10788.0,11036.7]:: -> p(n3,n1,n6),p(n3,n3,n6),p(n3,n9,n6)
% 2.28/1.05 11031:4:0:[10829.1,10229.1,10742.0,11027.4,10771.1,11028.6,10917.1,11029.7,10918.1,11030.8]:: -> p(n3,n1,n5),p(n3,n3,n5),p(n3,n4,n5),p(n3,n6,n5)
% 2.28/1.05 11026:6:0:[10828.1,10228.1,10741.0,11024.4,10835.1,11025.6]:: -> p(n3,n1,n4),p(n3,n3,n4),p(n3,n4,n4),p(n3,n6,n4),p(n3,n8,n4),p(n3,n9,n4)
% 2.28/1.05 11023:4:0:[10685.1,10225.0,10827.0,11019.1,10901.1,11020.2,10834.0,11021.6,10789.0,11022.7]:: -> p(n3,n4,n1),p(n3,n5,n1),p(n3,n6,n1),p(n3,n9,n1)
% 2.28/1.05 11018:6:0:[10692.0,10224.0,10821.1,11016.5,10826.1,11017.6]:: -> p(n2,n2,n9),p(n2,n3,n9),p(n2,n4,n9),p(n2,n5,n9),p(n2,n8,n9),p(n2,n9,n9)
% 2.28/1.05 11015:3:0:[10902.1,10222.0,10903.1,11010.1,10711.1,11011.2,10727.0,11012.3,10820.0,11013.5,10825.1,11014.6]:: -> p(n2,n5,n7),p(n2,n8,n7),p(n2,n9,n7)
% 2.28/1.05 10642:1:0:[10542.0,1814.1]:: p(n6,n4,n5) ->
% 2.28/1.05 10643:1:0:[10543.0,1821.1]:: p(n6,n4,n3) ->
% 2.28/1.05 11009:4:0:[10718.1,10221.3,10907.1,11005.4,10819.0,11006.5,10824.1,11007.6,10786.0,11008.7]:: -> p(n2,n1,n6),p(n2,n2,n6),p(n2,n3,n6),p(n2,n9,n6)
% 2.28/1.05 11004:6:0:[10740.0,10219.4,10818.0,11002.5,10823.0,11003.6]:: -> p(n2,n1,n4),p(n2,n2,n4),p(n2,n3,n4),p(n2,n4,n4),p(n2,n8,n4),p(n2,n9,n4)
% 2.28/1.05 11001:4:0:[10702.0,10218.1,10758.0,10997.5,10770.0,10998.6,10919.0,10999.7,10920.0,11000.8]:: -> p(n2,n1,n3),p(n2,n3,n3),p(n2,n4,n3),p(n2,n5,n3)
% 2.28/1.05 10996:3:0:[10905.0,10217.0,10701.0,10991.1,10906.0,10992.2,10726.0,10993.3,10817.0,10994.5,10775.0,10995.6]:: -> p(n2,n5,n2),p(n2,n8,n2),p(n2,n9,n2)
% 2.28/1.05 10990:3:0:[10684.1,10216.0,10899.1,10985.1,10900.1,10986.2,10816.0,10987.5,10822.0,10988.6,10787.0,10989.7]:: -> p(n2,n4,n1),p(n2,n5,n1),p(n2,n9,n1)
% 2.28/1.05 10984:6:0:[10688.0,10215.0,10810.1,10982.2,10815.1,10983.3]:: -> p(n1,n2,n9),p(n1,n5,n9),p(n1,n6,n9),p(n1,n7,n9),p(n1,n8,n9),p(n1,n9,n9)
% 2.28/1.05 10981:4:0:[10804.1,10214.0,10809.1,10977.2,10814.1,10978.3,10910.0,10979.4,10753.0,10980.5]:: -> p(n1,n2,n8),p(n1,n7,n8),p(n1,n8,n8),p(n1,n9,n8)
% 2.28/1.05 10644:1:0:[10543.0,1857.1]:: p(n6,n5,n3) ->
% 2.28/1.05 10645:1:0:[10542.0,1859.0]:: p(n6,n6,n5) ->
% 2.28/1.05 10976:2:0:[10803.1,10211.0,10808.0,10970.2,10813.0,10971.3,10739.0,10972.4,10767.0,10973.6,10913.0,10974.7,10915.0,10975.8]:: -> p(n1,n2,n5),p(n1,n6,n5)
% 2.28/1.05 10646:1:0:[10542.0,1868.0]:: p(n6,n7,n5) ->
% 2.28/1.05 10969:5:0:[10802.1,10210.0,10807.0,10966.2,10812.0,10967.3,10738.0,10968.4]:: -> p(n1,n2,n4),p(n1,n6,n4),p(n1,n7,n4),p(n1,n8,n4),p(n1,n9,n4)
% 2.28/1.05 10647:1:0:[10542.0,1877.0]:: p(n6,n8,n5) ->
% 2.28/1.05 10965:1:0:[10801.1,10209.0,10700.0,10958.1,10806.0,10959.2,10811.0,10960.3,10754.0,10961.5,10768.0,10962.6,10914.0,10963.7,10916.0,10964.8]:: -> p(n1,n5,n3)
% 2.28/1.05 10648:1:0:[10542.0,1886.0]:: p(n6,n9,n5) ->
% 2.28/1.05 10649:1:0:[10543.0,1893.0]:: p(n6,n7,n3) ->
% 2.28/1.05 10957:4:0:[10800.1,10208.0,10699.0,10953.1,10805.0,10954.2,10720.0,10955.3,10769.0,10956.6]:: -> p(n1,n5,n2),p(n1,n6,n2),p(n1,n8,n2),p(n1,n9,n2)
% 2.28/1.05 10650:1:0:[10543.0,1902.0]:: p(n6,n8,n3) ->
% 2.28/1.05 10651:1:0:[10543.0,1911.0]:: p(n6,n9,n3) ->
% 2.28/1.05 10652:1:0:[10544.0,1969.1]:: p(n7,n1,n7) ->
% 2.28/1.05 10653:1:0:[10545.0,1999.1]:: p(n7,n1,n1) ->
% 2.28/1.05 10654:1:0:[10544.0,2032.1]:: p(n7,n2,n7) ->
% 2.28/1.05 10655:1:0:[10545.0,2062.1]:: p(n7,n2,n1) ->
% 2.28/1.05 10952:1:0:[10547.0,10163.0]:: p(n9,n9,n2) ->
% 2.28/1.05 10656:1:0:[10544.0,2086.1]:: p(n7,n3,n7) ->
% 2.28/1.05 10951:1:0:[10547.0,10154.0]:: p(n9,n8,n2) ->
% 2.28/1.05 10657:1:0:[10545.0,2116.1]:: p(n7,n3,n1) ->
% 2.28/1.05 10658:1:0:[10544.0,2140.0]:: p(n7,n5,n7) ->
% 2.28/1.05 10659:1:0:[10544.0,2149.0]:: p(n7,n6,n7) ->
% 2.28/1.05 10660:1:0:[10544.0,2158.0]:: p(n7,n7,n7) ->
% 2.28/1.05 10661:1:0:[10545.0,2161.1]:: p(n7,n4,n1) ->
% 2.28/1.05 10662:1:0:[10544.0,2167.0]:: p(n7,n8,n7) ->
% 2.28/1.05 10663:1:0:[10544.0,2176.0]:: p(n7,n9,n7) ->
% 2.28/1.05 10664:1:0:[10545.0,2197.1]:: p(n7,n5,n1) ->
% 2.28/1.05 10665:1:0:[10545.0,2224.1]:: p(n7,n6,n1) ->
% 2.28/1.05 10950:1:0:[10547.0,10118.1]:: p(n7,n9,n2) ->
% 2.28/1.05 10949:1:0:[10545.0,10108.0]:: p(n9,n9,n1) ->
% 2.28/1.05 10666:1:0:[10545.0,2242.1]:: p(n7,n7,n1) ->
% 2.28/1.05 10948:1:0:[10545.0,10099.0]:: p(n9,n7,n1) ->
% 2.28/1.05 10947:1:0:[10545.0,10090.0]:: p(n8,n9,n1) ->
% 2.28/1.05 10667:1:0:[10545.0,2260.0]:: p(n7,n9,n1) ->
% 2.28/1.05 10668:1:0:[10546.0,2271.1]:: p(n8,n1,n3) ->
% 2.28/1.05 10669:1:0:[10547.0,2315.1]:: p(n8,n1,n2) ->
% 2.28/1.05 10670:1:0:[10546.0,2343.0]:: p(n8,n3,n3) ->
% 2.28/1.05 10671:1:0:[10546.0,2352.0]:: p(n8,n4,n3) ->
% 2.28/1.05 10672:1:0:[10546.0,2361.0]:: p(n8,n5,n3) ->
% 2.28/1.05 10673:1:0:[10546.0,2370.0]:: p(n8,n6,n3) ->
% 2.28/1.05 10674:1:0:[10547.0,2378.1]:: p(n8,n2,n2) ->
% 2.28/1.05 10675:1:0:[10546.0,2379.0]:: p(n8,n7,n3) ->
% 2.28/1.05 10676:1:0:[10546.0,2388.0]:: p(n8,n8,n3) ->
% 2.28/1.05 10677:1:0:[10546.0,2397.0]:: p(n8,n9,n3) ->
% 2.28/1.05 10678:1:0:[10547.0,2432.1]:: p(n8,n3,n2) ->
% 2.28/1.05 10679:1:0:[10547.0,2477.1]:: p(n8,n4,n2) ->
% 2.28/1.05 10680:1:0:[10547.0,2513.1]:: p(n8,n5,n2) ->
% 2.28/1.05 10681:1:0:[10547.0,2540.1]:: p(n8,n6,n2) ->
% 2.28/1.05 10682:1:0:[10547.0,2567.0]:: p(n8,n8,n2) ->
% 2.28/1.05 10683:1:0:[10547.0,2576.0]:: p(n8,n9,n2) ->
% 2.28/1.05 10684:1:0:[10531.0,2917.0]:: p(n2,n1,n1) ->
% 2.28/1.05 10685:1:0:[10531.0,2926.0]:: p(n3,n1,n1) ->
% 2.28/1.05 10686:1:0:[10531.0,2935.0]:: p(n4,n1,n1) ->
% 2.28/1.05 10687:1:0:[10531.0,2944.0]:: p(n5,n1,n1) ->
% 2.28/1.05 10946:1:0:[10544.0,9916.0]:: p(n9,n6,n7) ->
% 2.28/1.05 10945:1:0:[10544.0,9907.0]:: p(n9,n5,n7) ->
% 2.28/1.05 10688:1:0:[10540.0,2952.1]:: p(n1,n1,n9) ->
% 2.28/1.05 10689:1:0:[10531.0,2953.0]:: p(n6,n1,n1) ->
% 2.28/1.05 10944:1:0:[10544.0,9898.0]:: p(n8,n6,n7) ->
% 2.28/1.05 10943:1:0:[10544.0,9889.0]:: p(n8,n5,n7) ->
% 2.28/1.05 10690:1:0:[10531.0,2971.0]:: p(n8,n1,n1) ->
% 2.28/1.05 10942:1:0:[10546.0,9858.0]:: p(n9,n3,n3) ->
% 2.28/1.05 10941:1:0:[10546.0,9849.0]:: p(n9,n1,n3) ->
% 2.28/1.05 10691:1:0:[10531.0,2980.0]:: p(n9,n1,n1) ->
% 2.28/1.05 10692:1:0:[10540.0,3015.1]:: p(n2,n1,n9) ->
% 2.28/1.05 10940:1:0:[10546.0,9804.1]:: p(n7,n3,n3) ->
% 2.28/1.05 10693:1:0:[10540.0,3069.1]:: p(n3,n1,n9) ->
% 2.28/1.05 10939:1:0:[10546.0,9723.1]:: p(n7,n1,n3) ->
% 2.28/1.05 10938:1:0:[10541.0,9699.0]:: p(n6,n9,n6) ->
% 2.28/1.05 10937:1:0:[10541.0,9690.0]:: p(n6,n7,n6) ->
% 2.28/1.05 10694:1:0:[10540.0,3114.1]:: p(n4,n1,n9) ->
% 2.28/1.05 10936:1:0:[10541.0,9645.1]:: p(n4,n9,n6) ->
% 2.28/1.05 10695:1:0:[10540.0,3159.0]:: p(n6,n1,n9) ->
% 2.28/1.05 10696:1:0:[10540.0,3168.0]:: p(n7,n1,n9) ->
% 2.28/1.05 10697:1:0:[10540.0,3177.0]:: p(n8,n1,n9) ->
% 2.28/1.05 10698:1:0:[10540.0,3186.0]:: p(n9,n1,n9) ->
% 2.28/1.05 10935:1:0:[10541.0,9564.1]:: p(n4,n7,n6) ->
% 2.28/1.05 10934:1:0:[10542.0,9554.1]:: p(n5,n6,n5) ->
% 2.28/1.05 10933:1:0:[10543.0,9534.1]:: p(n5,n5,n3) ->
% 2.28/1.05 10932:1:0:[10543.0,9516.1]:: p(n5,n4,n3) ->
% 2.28/1.05 10931:1:0:[10542.0,9509.1]:: p(n5,n4,n5) ->
% 2.28/1.05 10930:1:0:[10542.0,9500.1]:: p(n4,n6,n5) ->
% 2.28/1.05 10929:1:0:[10539.0,9454.0]:: p(n6,n4,n4) ->
% 2.28/1.05 10928:1:0:[10539.0,9445.0]:: p(n5,n6,n4) ->
% 2.28/1.05 10927:1:0:[10539.0,9436.0]:: p(n5,n4,n4) ->
% 2.28/1.05 10926:1:0:[10538.0,9407.0]:: p(n5,n6,n2) ->
% 2.28/1.05 10925:1:0:[10538.0,9398.0]:: p(n5,n5,n2) ->
% 2.28/1.05 10699:1:0:[10536.0,3251.1]:: p(n1,n2,n2) ->
% 2.28/1.05 10924:1:0:[10540.0,9360.0]:: p(n6,n3,n9) ->
% 2.28/1.05 10923:1:0:[10540.0,9351.0]:: p(n6,n2,n9) ->
% 2.28/1.05 10922:1:0:[10540.0,9315.1]:: p(n4,n3,n9) ->
% 2.28/1.05 10700:1:0:[10546.0,3297.1]:: p(n1,n2,n3) ->
% 2.28/1.05 10921:1:0:[10540.0,9279.1]:: p(n4,n2,n9) ->
% 2.28/1.05 10701:1:0:[10536.0,3314.1]:: p(n2,n2,n2) ->
% 2.28/1.05 10920:1:0:[10537.0,9219.1]:: p(n2,n9,n3) ->
% 2.28/1.05 10919:1:0:[10537.0,9201.1]:: p(n2,n8,n3) ->
% 2.28/1.05 10918:1:0:[10535.0,9194.0]:: p(n3,n9,n5) ->
% 2.28/1.05 10917:1:0:[10535.0,9185.0]:: p(n3,n8,n5) ->
% 2.28/1.05 10916:1:0:[10537.0,9165.1]:: p(n1,n9,n3) ->
% 2.28/1.05 10702:1:0:[10546.0,3360.1]:: p(n2,n2,n3) ->
% 2.28/1.05 10915:1:0:[10535.0,9149.1]:: p(n1,n9,n5) ->
% 2.28/1.05 10914:1:0:[10537.0,9129.1]:: p(n1,n8,n3) ->
% 2.28/1.05 10703:1:0:[10536.0,3386.0]:: p(n5,n2,n2) ->
% 2.28/1.05 10913:1:0:[10535.0,9113.1]:: p(n1,n8,n5) ->
% 2.28/1.05 10704:1:0:[10536.0,3395.0]:: p(n6,n2,n2) ->
% 2.28/1.05 10705:1:0:[10536.0,3404.0]:: p(n7,n2,n2) ->
% 2.28/1.05 10706:1:0:[10536.0,3422.0]:: p(n9,n2,n2) ->
% 2.28/1.05 10912:1:0:[10534.0,9071.0]:: p(n3,n5,n8) ->
% 2.28/1.05 10911:1:0:[10534.0,9062.0]:: p(n3,n4,n8) ->
% 2.28/1.05 10707:1:0:[10546.0,3459.1]:: p(n4,n2,n3) ->
% 2.28/1.05 10910:1:0:[10534.0,8963.1]:: p(n1,n5,n8) ->
% 2.28/1.05 10909:1:0:[10533.0,8943.0]:: p(n3,n6,n6) ->
% 2.28/1.05 10708:1:0:[10546.0,3495.1]:: p(n5,n2,n3) ->
% 2.28/1.05 10908:1:0:[10533.0,8934.0]:: p(n3,n5,n6) ->
% 2.28/1.05 10907:1:0:[10533.0,8916.0]:: p(n2,n5,n6) ->
% 2.28/1.05 10906:1:0:[10536.0,8903.1]:: p(n2,n3,n2) ->
% 2.28/1.05 10905:1:0:[10536.0,8858.1]:: p(n2,n1,n2) ->
% 2.28/1.05 10904:1:0:[10532.0,8845.0]:: p(n3,n1,n7) ->
% 2.28/1.05 10903:1:0:[10532.0,8836.0]:: p(n2,n2,n7) ->
% 2.28/1.05 10902:1:0:[10532.0,8827.0]:: p(n2,n1,n7) ->
% 2.28/1.05 10709:1:0:[10546.0,3540.1]:: p(n7,n2,n3) ->
% 2.28/1.05 10710:1:0:[10546.0,3558.0]:: p(n9,n2,n3) ->
% 2.28/1.05 10901:1:0:[10531.0,8776.0]:: p(n3,n3,n1) ->
% 2.28/1.05 10900:1:0:[10531.0,8758.0]:: p(n2,n3,n1) ->
% 2.28/1.05 10711:1:0:[10532.0,3571.0]:: p(n2,n3,n7) ->
% 2.28/1.05 10899:1:0:[10531.0,8749.0]:: p(n2,n2,n1) ->
% 2.28/1.05 10712:1:0:[10532.0,3580.0]:: p(n3,n3,n7) ->
% 2.28/1.05 10713:1:0:[10532.0,3589.0]:: p(n4,n3,n7) ->
% 2.28/1.05 10714:1:0:[10532.0,3598.0]:: p(n5,n3,n7) ->
% 2.28/1.05 10715:1:0:[10532.0,3607.0]:: p(n6,n3,n7) ->
% 2.28/1.05 10716:1:0:[10532.0,3625.0]:: p(n8,n3,n7) ->
% 2.28/1.05 10717:1:0:[10532.0,3634.0]:: p(n9,n3,n7) ->
% 2.28/1.05 10718:1:0:[10533.0,3894.0]:: p(n2,n4,n6) ->
% 2.28/1.05 10719:1:0:[10533.0,3903.0]:: p(n3,n4,n6) ->
% 2.28/1.05 10720:1:0:[10538.0,3908.1]:: p(n1,n4,n2) ->
% 2.28/1.05 10721:1:0:[10533.0,3912.0]:: p(n4,n4,n6) ->
% 2.28/1.05 10722:1:0:[10533.0,3930.0]:: p(n6,n4,n6) ->
% 2.28/1.05 10723:1:0:[10533.0,3939.0]:: p(n7,n4,n6) ->
% 2.28/1.05 10724:1:0:[10533.0,3948.0]:: p(n8,n4,n6) ->
% 2.28/1.05 10725:1:0:[10533.0,3957.0]:: p(n9,n4,n6) ->
% 2.28/1.05 10726:1:0:[10538.0,3971.1]:: p(n2,n4,n2) ->
% 2.28/1.05 10727:1:0:[10544.0,4003.1]:: p(n2,n4,n7) ->
% 2.28/1.05 10728:1:0:[10544.0,4057.1]:: p(n3,n4,n7) ->
% 2.28/1.05 10729:1:0:[10538.0,4079.0]:: p(n5,n4,n2) ->
% 2.28/1.05 10730:1:0:[10538.0,4088.0]:: p(n6,n4,n2) ->
% 2.28/1.05 10898:1:0:[10547.0,8331.0]:: p(n8,n7,n9) ->
% 2.28/1.05 10897:1:0:[10547.0,8330.0]:: p(n8,n7,n8) ->
% 2.28/1.05 10896:1:0:[10547.0,8329.0]:: p(n8,n7,n7) ->
% 2.28/1.05 10895:1:0:[10547.0,8328.0]:: p(n8,n7,n6) ->
% 2.28/1.05 10731:1:0:[10538.0,4097.0]:: p(n7,n4,n2) ->
% 2.28/1.05 10894:1:0:[10547.0,8326.0]:: p(n8,n7,n4) ->
% 2.28/1.05 10893:1:0:[10547.0,8317.1]:: p(n8,n7,n1) ->
% 2.28/1.05 10732:1:0:[10544.0,4102.1]:: p(n4,n4,n7) ->
% 2.28/1.05 10733:1:0:[10538.0,4115.0]:: p(n9,n4,n2) ->
% 2.28/1.05 10734:1:0:[10544.0,4138.1]:: p(n5,n4,n7) ->
% 2.28/1.05 10735:1:0:[10544.0,4165.1]:: p(n6,n4,n7) ->
% 2.28/1.05 10736:1:0:[10544.0,4192.0]:: p(n8,n4,n7) ->
% 2.28/1.05 10737:1:0:[10544.0,4201.0]:: p(n9,n4,n7) ->
% 2.28/1.05 10892:1:0:[10546.0,8157.0]:: p(n8,n2,n9) ->
% 2.28/1.05 10891:1:0:[10546.0,8156.0]:: p(n8,n2,n8) ->
% 2.28/1.05 10890:1:0:[10546.0,8155.0]:: p(n8,n2,n7) ->
% 2.28/1.05 10889:1:0:[10546.0,8154.0]:: p(n8,n2,n6) ->
% 2.28/1.05 10888:1:0:[10546.0,8153.0]:: p(n8,n2,n5) ->
% 2.28/1.05 10887:1:0:[10546.0,8152.0]:: p(n8,n2,n4) ->
% 2.28/1.05 10886:1:0:[10546.0,8138.1]:: p(n8,n2,n1) ->
% 2.28/1.05 10738:1:0:[10539.0,4234.1]:: p(n1,n5,n4) ->
% 2.28/1.05 10739:1:0:[10542.0,4253.1]:: p(n1,n5,n5) ->
% 2.28/1.05 10885:1:0:[10545.0,8036.0]:: p(n7,n8,n9) ->
% 2.28/1.05 10884:1:0:[10545.0,8035.0]:: p(n7,n8,n8) ->
% 2.28/1.06 10883:1:0:[10545.0,8032.0]:: p(n7,n8,n5) ->
% 2.28/1.06 10882:1:0:[10545.0,8031.0]:: p(n7,n8,n4) ->
% 2.28/1.06 10881:1:0:[10545.0,8030.0]:: p(n7,n8,n3) ->
% 2.28/1.06 10880:1:0:[10545.0,8029.0]:: p(n7,n8,n2) ->
% 2.28/1.06 10740:1:0:[10539.0,4297.1]:: p(n2,n5,n4) ->
% 2.28/1.06 10879:1:0:[10544.0,7919.0]:: p(n7,n4,n9) ->
% 2.28/1.06 10878:1:0:[10544.0,7918.0]:: p(n7,n4,n8) ->
% 2.28/1.06 10877:1:0:[10544.0,7912.1]:: p(n7,n4,n5) ->
% 2.28/1.06 10876:1:0:[10544.0,7908.1]:: p(n7,n4,n4) ->
% 2.28/1.06 10741:1:0:[10539.0,4351.1]:: p(n3,n5,n4) ->
% 2.28/1.06 10875:1:0:[10544.0,7903.1]:: p(n7,n4,n3) ->
% 2.28/1.06 10742:1:0:[10542.0,4370.1]:: p(n3,n5,n5) ->
% 2.28/1.06 10743:1:0:[10539.0,4405.0]:: p(n5,n5,n4) ->
% 2.28/1.06 10744:1:0:[10539.0,4414.0]:: p(n6,n5,n4) ->
% 2.28/1.06 10745:1:0:[10542.0,4415.1]:: p(n4,n5,n5) ->
% 2.28/1.06 10746:1:0:[10539.0,4423.0]:: p(n7,n5,n4) ->
% 2.28/1.06 10747:1:0:[10539.0,4432.0]:: p(n8,n5,n4) ->
% 2.28/1.06 10748:1:0:[10539.0,4441.0]:: p(n9,n5,n4) ->
% 2.28/1.06 10749:1:0:[10542.0,4451.1]:: p(n5,n5,n5) ->
% 2.28/1.06 10750:1:0:[10542.0,4487.0]:: p(n7,n5,n5) ->
% 2.28/1.06 10751:1:0:[10542.0,4496.0]:: p(n8,n5,n5) ->
% 2.28/1.06 10752:1:0:[10542.0,4505.0]:: p(n9,n5,n5) ->
% 2.28/1.06 10753:1:0:[10534.0,4544.1]:: p(n1,n6,n8) ->
% 2.28/1.06 10874:1:0:[10543.0,7653.0]:: p(n6,n6,n9) ->
% 2.28/1.06 10873:1:0:[10543.0,7651.0]:: p(n6,n6,n7) ->
% 2.28/1.06 10872:1:0:[10543.0,7650.0]:: p(n6,n6,n6) ->
% 2.28/1.06 10871:1:0:[10543.0,7648.0]:: p(n6,n6,n4) ->
% 2.28/1.06 10870:1:0:[10543.0,7641.1]:: p(n6,n6,n2) ->
% 2.28/1.06 10754:1:0:[10543.0,4575.1]:: p(n1,n6,n3) ->
% 2.28/1.06 10869:1:0:[10543.0,7634.1]:: p(n6,n6,n1) ->
% 2.28/1.06 10868:1:0:[10542.0,7626.0]:: p(n6,n5,n9) ->
% 2.28/1.06 10867:1:0:[10542.0,7625.0]:: p(n6,n5,n8) ->
% 2.28/1.06 10866:1:0:[10542.0,7624.0]:: p(n6,n5,n7) ->
% 2.28/1.06 10865:1:0:[10542.0,7623.0]:: p(n6,n5,n6) ->
% 2.28/1.06 10864:1:0:[10542.0,7607.1]:: p(n6,n5,n2) ->
% 2.28/1.06 10863:1:0:[10542.0,7600.1]:: p(n6,n5,n1) ->
% 2.28/1.06 10755:1:0:[10534.0,4616.0]:: p(n3,n6,n8) ->
% 2.28/1.06 10756:1:0:[10534.0,4625.0]:: p(n4,n6,n8) ->
% 2.28/1.06 10757:1:0:[10534.0,4634.0]:: p(n5,n6,n8) ->
% 2.28/1.06 10758:1:0:[10543.0,4638.1]:: p(n2,n6,n3) ->
% 2.28/1.06 10759:1:0:[10534.0,4643.0]:: p(n6,n6,n8) ->
% 2.28/1.06 10760:1:0:[10534.0,4652.0]:: p(n7,n6,n8) ->
% 2.28/1.06 10761:1:0:[10534.0,4661.0]:: p(n8,n6,n8) ->
% 2.28/1.06 10762:1:0:[10534.0,4670.0]:: p(n9,n6,n8) ->
% 2.28/1.06 10763:1:0:[10543.0,4737.1]:: p(n4,n6,n3) ->
% 2.28/1.06 10862:1:0:[10541.0,7412.0]:: p(n5,n8,n8) ->
% 2.28/1.06 10861:1:0:[10541.0,7411.0]:: p(n5,n8,n7) ->
% 2.28/1.06 10860:1:0:[10541.0,7407.1]:: p(n5,n8,n5) ->
% 2.28/1.06 10859:1:0:[10541.0,7403.1]:: p(n5,n8,n4) ->
% 2.28/1.06 10858:1:0:[10541.0,7398.1]:: p(n5,n8,n3) ->
% 2.28/1.06 10857:1:0:[10541.0,7392.1]:: p(n5,n8,n2) ->
% 2.28/1.06 10764:1:0:[10543.0,4773.1]:: p(n5,n6,n3) ->
% 2.28/1.06 10765:1:0:[10543.0,4809.0]:: p(n7,n6,n3) ->
% 2.28/1.06 10766:1:0:[10543.0,4827.0]:: p(n9,n6,n3) ->
% 2.28/1.06 10767:1:0:[10535.0,4865.1]:: p(n1,n7,n5) ->
% 2.28/1.06 10768:1:0:[10537.0,4872.1]:: p(n1,n7,n3) ->
% 2.28/1.06 10856:1:0:[10540.0,7164.1]:: p(n5,n1,n8) ->
% 2.28/1.06 10855:1:0:[10540.0,7163.1]:: p(n5,n1,n7) ->
% 2.28/1.06 10854:1:0:[10540.0,7158.1]:: p(n5,n1,n5) ->
% 2.28/1.06 10853:1:0:[10540.0,7154.1]:: p(n5,n1,n4) ->
% 2.28/1.06 10852:1:0:[10540.0,7149.1]:: p(n5,n1,n3) ->
% 2.28/1.06 10769:1:0:[10547.0,4916.1]:: p(n1,n7,n2) ->
% 2.28/1.06 10851:1:0:[10540.0,7143.1]:: p(n5,n1,n2) ->
% 2.28/1.06 10770:1:0:[10537.0,4935.1]:: p(n2,n7,n3) ->
% 2.28/1.06 10771:1:0:[10535.0,4937.0]:: p(n3,n7,n5) ->
% 2.28/1.06 10772:1:0:[10535.0,4946.0]:: p(n4,n7,n5) ->
% 2.28/1.06 10773:1:0:[10535.0,4955.0]:: p(n5,n7,n5) ->
% 2.28/1.06 10774:1:0:[10535.0,4973.0]:: p(n7,n7,n5) ->
% 2.28/1.06 10775:1:0:[10547.0,4979.1]:: p(n2,n7,n2) ->
% 2.28/1.06 10776:1:0:[10535.0,4982.0]:: p(n8,n7,n5) ->
% 2.28/1.06 10777:1:0:[10535.0,4991.0]:: p(n9,n7,n5) ->
% 2.28/1.06 10778:1:0:[10537.0,4998.0]:: p(n4,n7,n3) ->
% 2.28/1.06 10779:1:0:[10537.0,5007.0]:: p(n5,n7,n3) ->
% 2.28/1.06 10780:1:0:[10537.0,5025.0]:: p(n7,n7,n3) ->
% 2.28/1.06 10781:1:0:[10537.0,5043.0]:: p(n9,n7,n3) ->
% 2.28/1.06 10850:1:0:[10539.0,6974.0]:: p(n4,n5,n9) ->
% 2.28/1.06 10849:1:0:[10539.0,6973.0]:: p(n4,n5,n8) ->
% 2.28/1.06 10848:1:0:[10539.0,6972.0]:: p(n4,n5,n7) ->
% 2.28/1.06 10847:1:0:[10539.0,6971.0]:: p(n4,n5,n6) ->
% 2.28/1.06 10846:1:0:[10539.0,6964.1]:: p(n4,n5,n3) ->
% 2.28/1.06 10845:1:0:[10539.0,6951.1]:: p(n4,n5,n1) ->
% 2.28/1.06 10844:1:0:[10538.0,6927.0]:: p(n4,n4,n9) ->
% 2.28/1.06 10843:1:0:[10538.0,6926.0]:: p(n4,n4,n8) ->
% 2.28/1.06 10842:1:0:[10538.0,6923.0]:: p(n4,n4,n5) ->
% 2.28/1.06 10841:1:0:[10538.0,6921.0]:: p(n4,n4,n3) ->
% 2.28/1.06 10840:1:0:[10538.0,6913.1]:: p(n4,n4,n1) ->
% 2.28/1.06 10782:1:0:[10547.0,5114.1]:: p(n5,n7,n2) ->
% 2.28/1.06 10783:1:0:[10547.0,5141.1]:: p(n6,n7,n2) ->
% 2.28/1.06 10784:1:0:[10547.0,5159.1]:: p(n7,n7,n2) ->
% 2.28/1.06 10785:1:0:[10547.0,5177.0]:: p(n9,n7,n2) ->
% 2.28/1.06 10839:1:0:[10537.0,6717.0]:: p(n3,n7,n9) ->
% 2.28/1.06 10838:1:0:[10537.0,6716.0]:: p(n3,n7,n8) ->
% 2.28/1.06 10837:1:0:[10537.0,6715.0]:: p(n3,n7,n7) ->
% 2.28/1.06 10836:1:0:[10537.0,6714.0]:: p(n3,n7,n6) ->
% 2.28/1.06 10835:1:0:[10537.0,6712.0]:: p(n3,n7,n4) ->
% 2.28/1.06 10834:1:0:[10537.0,6698.1]:: p(n3,n7,n1) ->
% 2.28/1.06 10786:1:0:[10541.0,5280.1]:: p(n2,n8,n6) ->
% 2.28/1.06 10787:1:0:[10545.0,5293.1]:: p(n2,n8,n1) ->
% 2.28/1.06 10788:1:0:[10541.0,5334.1]:: p(n3,n8,n6) ->
% 2.28/1.06 10789:1:0:[10545.0,5347.1]:: p(n3,n8,n1) ->
% 2.28/1.06 10833:1:0:[10536.0,6531.0]:: p(n3,n2,n9) ->
% 2.28/1.06 10832:1:0:[10536.0,6530.0]:: p(n3,n2,n8) ->
% 2.28/1.06 10790:1:0:[10541.0,5379.1]:: p(n4,n8,n6) ->
% 2.28/1.06 10831:1:0:[10536.0,6529.0]:: p(n3,n2,n7) ->
% 2.28/1.06 10830:1:0:[10536.0,6528.0]:: p(n3,n2,n6) ->
% 2.28/1.06 10829:1:0:[10536.0,6527.0]:: p(n3,n2,n5) ->
% 2.28/1.06 10828:1:0:[10536.0,6526.0]:: p(n3,n2,n4) ->
% 2.28/1.06 10827:1:0:[10536.0,6517.1]:: p(n3,n2,n1) ->
% 2.28/1.06 10791:1:0:[10545.0,5392.1]:: p(n4,n8,n1) ->
% 2.28/1.06 10792:1:0:[10541.0,5424.0]:: p(n6,n8,n6) ->
% 2.28/1.06 10793:1:0:[10545.0,5428.1]:: p(n5,n8,n1) ->
% 2.28/1.06 10794:1:0:[10541.0,5433.0]:: p(n7,n8,n6) ->
% 2.28/1.06 10795:1:0:[10541.0,5442.0]:: p(n8,n8,n6) ->
% 2.28/1.06 10796:1:0:[10541.0,5451.0]:: p(n9,n8,n6) ->
% 2.28/1.06 10797:1:0:[10545.0,5455.1]:: p(n6,n8,n1) ->
% 2.28/1.06 10798:1:0:[10545.0,5482.0]:: p(n8,n8,n1) ->
% 2.28/1.06 10826:1:0:[10535.0,6402.0]:: p(n2,n7,n9) ->
% 2.28/1.06 10799:1:0:[10545.0,5491.0]:: p(n9,n8,n1) ->
% 2.28/1.06 10825:1:0:[10535.0,6400.0]:: p(n2,n7,n7) ->
% 2.28/1.06 10824:1:0:[10535.0,6399.0]:: p(n2,n7,n6) ->
% 2.28/1.06 10823:1:0:[10535.0,6394.1]:: p(n2,n7,n4) ->
% 2.28/1.06 10822:1:0:[10535.0,6376.1]:: p(n2,n7,n1) ->
% 2.28/1.06 10821:1:0:[10534.0,6372.0]:: p(n2,n6,n9) ->
% 2.28/1.06 10820:1:0:[10534.0,6370.1]:: p(n2,n6,n7) ->
% 2.28/1.06 10819:1:0:[10534.0,6368.1]:: p(n2,n6,n6) ->
% 2.28/1.06 10818:1:0:[10534.0,6361.1]:: p(n2,n6,n4) ->
% 2.28/1.06 10817:1:0:[10534.0,6350.1]:: p(n2,n6,n2) ->
% 2.28/1.06 10816:1:0:[10534.0,6343.1]:: p(n2,n6,n1) ->
% 2.28/1.06 10815:1:0:[10533.0,5973.0]:: p(n1,n4,n9) ->
% 2.28/1.06 10814:1:0:[10533.0,5972.0]:: p(n1,n4,n8) ->
% 2.28/1.06 10813:1:0:[10533.0,5967.1]:: p(n1,n4,n5) ->
% 2.28/1.06 10812:1:0:[10533.0,5963.1]:: p(n1,n4,n4) ->
% 2.28/1.06 10811:1:0:[10533.0,5958.1]:: p(n1,n4,n3) ->
% 2.28/1.06 10810:1:0:[10532.0,5939.0]:: p(n1,n3,n9) ->
% 2.28/1.06 10809:1:0:[10532.0,5938.0]:: p(n1,n3,n8) ->
% 2.28/1.06 10800:1:0:[10531.0,5833.0]:: p(n1,n1,n2) ->
% 2.28/1.06 10801:1:0:[10531.0,5834.0]:: p(n1,n1,n3) ->
% 2.28/1.06 10802:1:0:[10531.0,5835.0]:: p(n1,n1,n4) ->
% 2.28/1.06 10803:1:0:[10531.0,5836.0]:: p(n1,n1,n5) ->
% 2.28/1.06 10808:1:0:[10532.0,5932.1]:: p(n1,n3,n5) ->
% 2.28/1.06 10807:1:0:[10532.0,5928.1]:: p(n1,n3,n4) ->
% 2.28/1.06 10804:1:0:[10531.0,5839.0]:: p(n1,n1,n8) ->
% 2.28/1.06 10806:1:0:[10532.0,5923.1]:: p(n1,n3,n3) ->
% 2.28/1.06 10805:1:0:[10532.0,5917.1]:: p(n1,n3,n2) ->
% 2.28/1.06
% 2.28/1.06 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,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(n8,n7,n2) 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(n8,n2,n3) p(n7,n8,n1) p(n1,n5,n8) p(n1,n5,n9) p(n1,n6,n1) p(n1,n6,n2) p(n1,n6,n3) p(n1,n6,n4) p(n1,n6,n5) p(n7,n4,n7) p(n6,n6,n3) p(n1,n6,n8) p(n1,n6,n9) p(n1,n7,n1) p(n1,n7,n2) p(n1,n7,n3) p(n1,n7,n4) p(n1,n7,n5) p(n6,n5,n5) p(n5,n8,n6) p(n1,n7,n8) p(n1,n7,n9) p(n1,n8,n1) p(n1,n8,n2) p(n1,n8,n3) p(n1,n8,n4) p(n1,n8,n5) p(n5,n1,n9) p(n4,n5,n4) p(n1,n8,n8) p(n1,n8,n9) p(n1,n9,n1) p(n1,n9,n2) p(n1,n9,n3) p(n1,n9,n4) p(n1,n9,n5) p(n4,n4,n2) p(n3,n7,n3) p(n1,n9,n8) p(n1,n9,n9) p(n3,n2,n2) p(n2,n7,n5) p(n2,n6,n8) p(n1,n4,n6) p(n1,n3,n7) p(n1,n1,n1) p(n7,n7,n9) p(n7,n9,n9) p(n8,n8,n9) p(n8,n9,n9) p(n9,n7,n9) p(n9,n8,n9) p(n9,n9,n9) p(n7,n7,n8) p(n7,n9,n8) p(n8,n8,n8) p(n8,n9,n8) p(n9,n7,n8) p(n9,n8,n8) p(n9,n9,n8) p(n8,n8,n7) p(n8,n9,n7) p(n9,n7,n7) p(n9,n8,n7) p(n9,n9,n7) p(n7,n9,n5) p(n8,n8,n5) p(n8,n9,n5) p(n9,n8,n5) p(n9,n9,n5) p(n7,n7,n4) p(n7,n9,n4) p(n8,n8,n4) p(n8,n9,n4) p(n9,n7,n4) p(n9,n8,n4) p(n9,n9,n4) p(n7,n9,n3) p(n9,n8,n3) p(n9,n9,n3) p(n7,n5,n9) p(n7,n6,n9) p(n8,n4,n9) p(n8,n5,n9) p(n8,n6,n9) p(n9,n4,n9) p(n9,n5,n9) p(n9,n6,n9) p(n7,n5,n8) p(n8,n4,n8) p(n8,n5,n8) p(n9,n4,n8) p(n9,n5,n8) p(n7,n6,n5) p(n8,n4,n5) p(n8,n6,n5) p(n9,n4,n5) p(n9,n6,n5) p(n7,n6,n4) p(n8,n4,n4) p(n8,n6,n4) p(n9,n4,n4) p(n9,n6,n4) p(n7,n5,n3) p(n9,n4,n3) p(n9,n5,n3) p(n7,n5,n2) p(n7,n6,n2) p(n9,n5,n2) p(n9,n6,n2) p(n8,n4,n1) p(n8,n5,n1) p(n8,n6,n1) p(n9,n4,n1) p(n9,n5,n1) p(n9,n6,n1) p(n1,n4,n7) p(n7,n2,n9) p(n7,n3,n9) p(n8,n3,n9) p(n9,n2,n9) p(n9,n3,n9) p(n7,n1,n8) p(n7,n2,n8) p(n7,n3,n8) p(n8,n1,n8) p(n8,n3,n8) p(n9,n1,n8) p(n9,n2,n8) p(n9,n3,n8) p(n1,n5,n7) p(n8,n1,n7) p(n9,n1,n7) p(n9,n2,n7) p(n7,n1,n6) p(n7,n2,n6) p(n7,n3,n6) p(n8,n1,n6) p(n8,n3,n6) p(n9,n1,n6) p(n9,n2,n6) p(n9,n3,n6) p(n1,n6,n7) p(n7,n1,n5) p(n7,n2,n5) p(n7,n3,n5) p(n8,n1,n5) p(n8,n3,n5) p(n9,n1,n5) p(n9,n2,n5) p(n9,n3,n5) p(n7,n1,n4) p(n7,n2,n4) p(n7,n3,n4) p(n8,n1,n4) p(n8,n3,n4) p(n9,n1,n4) p(n9,n2,n4) p(n9,n3,n4) p(n1,n7,n7) p(n7,n1,n2) p(n7,n3,n2) p(n9,n1,n2) p(n9,n3,n2) p(n8,n3,n1) p(n9,n2,n1) p(n9,n3,n1) p(n1,n8,n7) p(n4,n7,n9) p(n4,n8,n9) p(n4,n9,n9) p(n6,n7,n9) p(n6,n8,n9) p(n6,n9,n9) p(n4,n7,n8) p(n4,n8,n8) p(n4,n9,n8) p(n5,n7,n8) p(n5,n9,n8) p(n6,n7,n8) p(n6,n8,n8) p(n6,n9,n8) p(n1,n9,n7) p(n4,n7,n7) p(n4,n8,n7) p(n4,n9,n7) p(n5,n7,n7) p(n5,n9,n7) p(n6,n7,n7) p(n6,n8,n7) p(n6,n9,n7) p(n1,n5,n6) p(n4,n8,n5) p(n4,n9,n5) p(n5,n9,n5) p(n5,n7,n4) p(n5,n9,n4) p(n6,n7,n4) p(n6,n8,n4) p(n6,n9,n4) p(n1,n6,n6) p(n4,n8,n3) p(n4,n9,n3) p(n5,n9,n3) p(n5,n9,n2) p(n6,n8,n2) p(n6,n9,n2) p(n1,n7,n6) p(n4,n6,n9) p(n6,n4,n9) p(n5,n4,n8) p(n5,n5,n8) p(n6,n4,n8) p(n1,n8,n6) p(n4,n6,n7) p(n5,n5,n7) p(n5,n6,n7) p(n4,n6,n6) p(n1,n9,n6) p(n4,n6,n1) p(n5,n4,n1) p(n5,n5,n1) p(n5,n6,n1) p(n6,n4,n1) p(n4,n1,n8) p(n4,n2,n8) p(n4,n3,n8) p(n5,n2,n8) p(n5,n3,n8) p(n6,n1,n8) p(n6,n2,n8) p(n6,n3,n8) p(n4,n1,n7) p(n4,n2,n7) p(n5,n2,n7) p(n6,n1,n7) p(n6,n2,n7) p(n4,n1,n5) p(n4,n2,n5) p(n4,n3,n5) p(n5,n2,n5) p(n5,n3,n5) p(n5,n2,n4) p(n5,n3,n4) p(n6,n1,n4) p(n6,n2,n4) p(n6,n3,n4) p(n4,n1,n3) p(n4,n3,n3) p(n5,n3,n3) p(n5,n3,n2) p(n6,n1,n2) p(n6,n3,n2) p(n4,n2,n1) p(n4,n3,n1) p(n5,n2,n1) p(n5,n3,n1) p(n6,n2,n1) p(n6,n3,n1) p(n2,n8,n9) p(n2,n9,n9) p(n3,n8,n9) p(n3,n9,n9) p(n3,n8,n8) p(n3,n9,n8) p(n2,n8,n7) p(n2,n9,n7) p(n3,n8,n7) p(n3,n9,n7) p(n2,n9,n6) p(n3,n9,n6) p(n2,n8,n4) p(n2,n9,n4) p(n3,n8,n4) p(n3,n9,n4) p(n2,n8,n2) p(n2,n9,n2) p(n2,n9,n1) p(n3,n9,n1) p(n2,n4,n9) p(n2,n5,n9) p(n3,n4,n9) p(n3,n5,n9) p(n3,n6,n9) p(n2,n5,n7) p(n3,n5,n7) p(n3,n6,n7) p(n3,n4,n5) p(n3,n6,n5) p(n2,n4,n4) p(n3,n4,n4) p(n3,n6,n4) p(n2,n5,n2) p(n2,n4,n1) p(n2,n5,n1) p(n3,n4,n1) p(n3,n5,n1) p(n3,n6,n1) p(n2,n2,n9) p(n2,n3,n9) p(n3,n3,n9) p(n3,n1,n8) p(n3,n3,n8) p(n2,n1,n6) p(n2,n2,n6) p(n2,n3,n6) p(n3,n1,n6) p(n3,n3,n6) p(n3,n1,n5) p(n3,n3,n5) p(n2,n1,n4) p(n2,n2,n4) p(n2,n3,n4) p(n3,n1,n4) p(n3,n3,n4) p(n2,n1,n3) p(n2,n3,n3) p(n9,n9,n6) p(n9,n7,n6) p(n9,n6,n6) p(n2,n1,n1) p(n2,n2,n1) p(n2,n1,n2) p(n2,n2,n2) p(n2,n2,n3) p(n2,n1,n5) p(n2,n2,n5) p(n2,n1,n7) p(n2,n2,n7) p(n2,n1,n8) p(n2,n2,n8) p(n2,n1,n9) p(n2,n3,n1) p(n2,n3,n2) p(n2,n3,n5) p(n2,n3,n7) p(n2,n3,n8) p(n2,n4,n2) p(n2,n4,n3) p(n2,n4,n5) p(n2,n4,n6) p(n2,n4,n7) p(n2,n4,n8) p(n2,n5,n3) p(n2,n5,n4) p(n2,n5,n5) p(n2,n5,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(n2,n6,n7) p(n2,n6,n9) p(n2,n7,n1) p(n2,n7,n2) p(n2,n7,n3) p(n2,n7,n4) p(n2,n7,n6) p(n2,n7,n7) p(n9,n5,n6) p(n2,n7,n9) p(n2,n8,n1) p(n2,n8,n3) p(n2,n8,n6) p(n2,n9,n3) p(n8,n9,n6) p(n8,n6,n6) p(n8,n5,n6) p(n7,n9,n6) p(n7,n7,n6) p(n7,n6,n6) p(n7,n5,n6) p(n6,n9,n1) p(n6,n7,n1) p(n6,n3,n6) p(n6,n2,n6) p(n2,n7,n8) p(n6,n1,n6) p(n2,n8,n8) p(n5,n9,n1) p(n2,n9,n8) p(n2,n8,n5) p(n5,n7,n1) p(n2,n9,n5) p(n3,n1,n1) p(n3,n2,n1) p(n3,n1,n2) p(n3,n1,n3) p(n3,n2,n3) p(n3,n2,n4) p(n3,n2,n5) p(n3,n2,n6) p(n3,n1,n7) p(n3,n2,n7) p(n3,n2,n8) p(n3,n1,n9) p(n3,n2,n9) p(n3,n3,n1) p(n3,n3,n3) p(n3,n3,n7) p(n3,n4,n3) p(n3,n4,n6) p(n3,n4,n7) p(n3,n4,n8) p(n4,n9,n1) p(n3,n5,n3) p(n3,n5,n4) p(n3,n5,n5) p(n3,n5,n6) p(n3,n5,n8) p(n3,n6,n3) p(n3,n6,n6) p(n3,n6,n8) p(n3,n7,n1) p(n4,n7,n1) p(n3,n7,n4) p(n3,n7,n5) p(n3,n7,n6) p(n3,n7,n7) p(n3,n7,n8) p(n3,n7,n9) p(n3,n8,n1) p(n4,n3,n6) p(n3,n8,n5) p(n3,n8,n6) p(n4,n2,n6) p(n4,n1,n6) p(n3,n9,n5) p(n3,n3,n2) p(n3,n4,n2) p(n3,n5,n2) p(n3,n6,n2) p(n3,n7,n2) p(n3,n8,n2) p(n3,n9,n2) p(n3,n8,n3) p(n3,n9,n3) p(n4,n1,n1) p(n4,n1,n2) p(n4,n2,n2) p(n4,n2,n3) p(n4,n1,n4) p(n4,n2,n4) p(n4,n1,n9) p(n4,n2,n9) p(n4,n3,n2) p(n4,n3,n4) p(n4,n3,n7) 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,n7) p(n4,n4,n8) p(n4,n4,n9) p(n4,n5,n1) p(n4,n5,n3) p(n4,n5,n5) p(n4,n5,n6) p(n4,n5,n7) p(n4,n5,n8) p(n4,n5,n9) p(n4,n6,n3) p(n4,n6,n5) p(n4,n6,n8) p(n4,n7,n3) p(n4,n7,n5) p(n4,n7,n6) p(n4,n8,n1) p(n4,n8,n6) p(n4,n9,n6) p(n4,n5,n2) p(n4,n6,n2) p(n4,n7,n2) p(n4,n8,n2) p(n4,n9,n2) p(n4,n6,n4) p(n4,n7,n4) p(n4,n8,n4) p(n4,n9,n4) p(n5,n1,n1) p(n5,n1,n2) p(n5,n2,n2) p(n5,n1,n3) p(n5,n2,n3) p(n5,n1,n4) p(n5,n1,n5) p(n5,n1,n6) p(n5,n2,n6) p(n5,n1,n7) p(n5,n1,n8) p(n5,n2,n9) p(n5,n3,n6) p(n5,n3,n7) p(n5,n3,n9) p(n5,n4,n2) p(n5,n4,n3) p(n5,n4,n4) p(n5,n4,n5) p(n5,n4,n6) p(n5,n4,n7) p(n5,n4,n9) p(n5,n5,n2) p(n5,n5,n3) p(n5,n5,n4) p(n5,n5,n5) p(n5,n5,n6) p(n5,n5,n9) p(n5,n6,n2) p(n5,n6,n3) p(n5,n6,n4) p(n5,n6,n5) p(n5,n6,n6) p(n5,n6,n8) p(n5,n6,n9) p(n5,n7,n2) p(n5,n7,n3) p(n5,n7,n5) p(n5,n7,n6) p(n5,n7,n9) p(n5,n8,n1) p(n5,n8,n2) p(n5,n8,n3) p(n5,n8,n4) p(n5,n8,n5) p(n5,n8,n7) p(n5,n8,n8) p(n5,n8,n9) p(n5,n9,n9) p(n5,n9,n6) p(n6,n1,n1) p(n6,n2,n2) p(n6,n1,n3) p(n6,n2,n3) p(n6,n1,n5) p(n6,n2,n5) p(n6,n1,n9) p(n6,n2,n9) p(n6,n3,n3) p(n6,n3,n5) p(n6,n3,n7) p(n6,n3,n9) p(n6,n4,n2) p(n6,n4,n3) p(n6,n4,n4) p(n6,n4,n5) p(n6,n4,n6) p(n6,n4,n7) p(n6,n5,n1) p(n6,n5,n2) p(n6,n5,n3) p(n6,n5,n4) p(n6,n5,n6) p(n6,n5,n7) p(n6,n5,n8) p(n6,n5,n9) p(n6,n6,n1) p(n6,n6,n2) 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,n6) p(n6,n8,n1) p(n6,n8,n6) p(n6,n9,n6) p(n6,n6,n5) p(n6,n7,n5) p(n6,n8,n5) p(n6,n9,n5) p(n6,n7,n3) p(n6,n8,n3) p(n6,n9,n3) p(n7,n1,n1) p(n7,n2,n1) p(n7,n2,n2) p(n7,n1,n3) p(n7,n2,n3) p(n7,n1,n7) p(n7,n2,n7) p(n7,n1,n9) p(n7,n3,n1) p(n7,n3,n3) p(n7,n3,n7) p(n7,n4,n1) p(n7,n4,n2) p(n7,n4,n3) p(n7,n4,n4) p(n7,n4,n5) p(n7,n4,n6) p(n7,n4,n8) p(n7,n4,n9) p(n7,n5,n1) p(n7,n5,n4) p(n7,n5,n5) p(n7,n6,n1) p(n7,n6,n3) p(n7,n6,n8) p(n7,n7,n1) p(n7,n7,n2) p(n7,n7,n3) p(n7,n7,n5) p(n7,n8,n2) p(n7,n8,n3) p(n7,n8,n4) p(n7,n8,n5) p(n7,n8,n6) p(n7,n8,n8) p(n7,n8,n9) p(n7,n9,n2) p(n9,n9,n2) p(n9,n8,n2) p(n7,n5,n7) p(n7,n6,n7) p(n7,n7,n7) p(n7,n8,n7) p(n7,n9,n7) p(n9,n9,n1) p(n9,n7,n1) p(n8,n9,n1) p(n7,n9,n1) p(n8,n1,n1) p(n8,n2,n1) p(n8,n1,n2) p(n8,n2,n2) p(n8,n1,n3) p(n8,n2,n4) p(n8,n2,n5) p(n8,n2,n6) p(n8,n2,n7) p(n8,n2,n8) p(n8,n1,n9) p(n8,n2,n9) p(n8,n3,n2) p(n8,n3,n7) p(n8,n4,n2) p(n8,n4,n6) p(n8,n4,n7) p(n8,n5,n2) p(n8,n5,n4) p(n8,n5,n5) p(n8,n5,n7) p(n8,n6,n2) p(n8,n6,n7) p(n8,n6,n8) p(n8,n7,n1) p(n8,n7,n4) p(n8,n7,n5) p(n8,n7,n6) p(n8,n7,n7) p(n8,n7,n8) p(n8,n7,n9) p(n8,n8,n1) p(n8,n8,n6) p(n8,n3,n3) p(n8,n4,n3) p(n8,n5,n3) p(n8,n6,n3) p(n8,n7,n3) p(n8,n8,n3) p(n8,n9,n3) p(n8,n8,n2) p(n8,n9,n2) p(n9,n1,n1) p(n9,n2,n2) p(n9,n1,n3) p(n9,n2,n3) p(n9,n1,n9) p(n9,n3,n3) p(n9,n3,n7) p(n9,n4,n2) p(n9,n4,n6) p(n9,n4,n7) p(n9,n5,n4) p(n9,n5,n5) p(n9,n5,n7) p(n9,n6,n3) p(n9,n6,n7) p(n9,n6,n8) p(n9,n7,n2) p(n9,n7,n3) p(n9,n7,n5) p(n9,n8,n1) p(n9,n8,n6)
% 2.28/1.06
% 2.28/1.06 === Starting SPASS-SCL-FOL A Little Less Naive, considering 729 atoms initially, heuristics mode: normal ===
% 2.28/1.06
% 2.28/1.06 === Backtracking. Learning clause 11999:1:0:[1077.2,11880.1]:: p(n4,n2,n6) ->
% 2.28/1.06 === Backtracking. Learning clause 12000:2:0:[7209.1,11088.1,11095.1,7427.1,5754.1,11921.3,1031.2,11154.2,1040.2]:: p(n4,n1,n5) -> p(n7,n5,n3)
% 2.28/1.06 === Conflict found: 11396:3:0:[10563.1,10339.0,10820.0,11391.1,10873.1,11392.5,10659.1,11393.6,10944.1,11394.7,10946.1,11395.8]:: -> p(n3,n6,n7),p(n4,n6,n7),p(n5,n6,n7) {}
% 2.28/1.06 === Backtracking. Learning clause 12001:3:0:[11396.1,6666.2,1573.1]:: p(n3,n6,n1),p(n5,n7,n7) -> p(n4,n6,n7)
% 2.28/1.06 === Conflict found: 11899:2:0:[10844.1,10494.0,10850.1,11893.1,10622.1,11894.3,10623.1,11895.4,10624.1,11896.5,10868.1,11897.7,10874.1,11898.8]:: -> p(n4,n6,n9),p(n6,n4,n9) {}
% 2.28/1.06 === Backtracking. Learning clause 12003:1:0:[11880.0,12002.1,11899.2,1836.1,7017.2]:: p(n6,n7,n9) ->
% 2.28/1.06 === Backtracking. Learning clause 12004:1:0:[6773.2,11829.2,11815.2,6452.1,6477.1]:: p(n2,n9,n9) ->
% 2.28/1.06 === Conflict found: 11815:2:0:[10555.1,10468.0,10556.1,11809.1,10557.1,11810.2,10822.0,11811.3,10787.0,11812.4,10834.0,11813.6,10789.0,11814.7]:: -> p(n2,n9,n1),p(n3,n9,n1) {}
% 2.28/1.06 === Backtracking. Learning clause 12005:1:0:[11815.1,5608.1,5662.1]:: p(n6,n9,n1) ->
% 2.28/1.06 === Conflict found: 11886:3:0:[10732.0,10492.0,10848.1,11881.1,10734.0,11882.3,10735.0,11883.6,10866.1,11884.7,10873.1,11885.8]:: -> p(n4,n6,n7),p(n5,n5,n7),p(n5,n6,n7) {}
% 2.28/1.06 === Backtracking. Learning clause 12006:2:0:[11886.2,1546.1,1573.1]:: p(n5,n7,n7) -> p(n4,n6,n7)
% 2.28/1.06 === Backtracking. Learning clause 12007:1:0:[4260.1,10965.1,11154.1,5754.2,11095.2,7209.2,11088.1]:: -> p(n5,n9,n2)
% 2.28/1.06 === Conflict found: 11886:3:0:[10732.0,10492.0,10848.1,11881.1,10734.0,11882.3,10735.0,11883.6,10866.1,11884.7,10873.1,11885.8]:: -> p(n4,n6,n7),p(n5,n5,n7),p(n5,n6,n7) {}
% 2.28/1.06 === Backtracking. Learning clause 12010:1:0:[11880.0,12008.0,1573.0,12009.2,11886.1,7015.2,1546.1]:: p(n5,n7,n7) ->
% 2.28/1.06 === Conflict found: 11079:4:0:[10694.0,10242.0,10921.0,11075.1,10922.0,11076.2,10844.1,11077.3,10850.1,11078.4]:: -> p(n4,n6,n9),p(n4,n7,n9),p(n4,n8,n9),p(n4,n9,n9) {}
% 2.28/1.06 === Backtracking. Learning clause 12011:5:0:[11079.4,7122.2,7077.2,5076.1,11921.2,7073.2,11911.1]:: p(n7,n7,n9) -> p(n4,n6,n9),p(n5,n9,n5),p(n4,n9,n3),p(n5,n9,n3)
% 2.28/1.06 === Conflict found: 11483:7:0:[10566.1,10366.0,10663.1,11482.6]:: -> p(n2,n9,n7),p(n3,n9,n7),p(n4,n9,n7),p(n5,n9,n7),p(n6,n9,n7),p(n8,n9,n7),p(n9,n9,n7) {}
% 2.28/1.06 === Backtracking. Learning clause 12012:7:0:[11483.7,2725.2,8422.1]:: p(n9,n2,n7),p(n8,n9,n8) -> p(n2,n9,n7),p(n3,n9,n7),p(n4,n9,n7),p(n5,n9,n7),p(n6,n9,n7)
% 2.28/1.06 === Conflict found: 11117:5:0:[10689.1,10252.0,10863.0,11114.4,10869.0,11115.5,10797.0,11116.7]:: -> p(n6,n2,n1),p(n6,n3,n1),p(n6,n4,n1),p(n6,n7,n1),p(n6,n9,n1) {}
% 2.28/1.06 === Backtracking. Learning clause 12018:5:0:[11880.0,12013.4,12005.0,12014.6,11999.0,12015.7,12010.0,12016.8,1040.0,12017.9,11117.1,3439.2,9298.2,11585.1,7674.1,11421.3,2707.2,1052.1,11946.3,3148.2,979.2,3139.2,11581.4,989.1,7055.1,1103.1,7568.1,1014.1,9246.1]:: p(n4,n3,n8),p(n4,n7,n9),p(n4,n9,n5),p(n6,n4,n9),p(n5,n3,n3) ->
% 2.28/1.06 === Backtracking. Learning clause 12025:23:0:[10965.0,12019.0,4708.0,12020.4,9239.0,12021.15,7368.1,12022.21,10036.1,12023.24,4852.1,12024.25,936.2,11574.4,11569.5,4550.2,706.2,11758.5,6577.1,907.2,11806.2,3280.1,6313.2,11648.2,11789.3,6023.1,11047.2,10976.2,5345.1,11137.6,7774.2,9031.2,9260.2,5985.1,3272.1,7675.2,3445.2,11483.5,3059.1,409.1,9269.2,10195.1,2905.2,11581.5,11071.2,3139.1,11946.1,2644.1,11421.4,7674.2,11405.3,7347.1,8466.2,3529.1,11200.1,463.1,10027.2,11533.3]:: p(n5,n2,n5),p(n5,n7,n4),p(n8,n6,n1) -> p(n2,n1,n4),p(n3,n6,n7),p(n6,n2,n6),p(n3,n9,n8),p(n6,n1,n8),p(n6,n4,n8),p(n2,n9,n7),p(n3,n9,n7),p(n5,n9,n7),p(n4,n1,n3),p(n4,n1,n6),p(n4,n6,n7),p(n4,n8,n7),p(n4,n9,n7),p(n4,n7,n7),p(n4,n7,n1),p(n9,n3,n1),p(n2,n4,n1),p(n2,n4,n3),p(n2,n4,n9)
% 2.28/1.06 === Conflict found: 11574:4:0:[10789.0,10394.0,10596.1,11570.1,10602.1,11571.2,10917.1,11572.4,10788.0,11573.5]:: -> p(n3,n8,n4),p(n3,n8,n7),p(n3,n8,n8),p(n3,n8,n9) {}
% 2.28/1.06 === Backtracking. Learning clause 12034:19:0:[10965.0,12026.1,12007.0,12027.5,1626.1,12028.10,9246.0,12029.17,9239.0,12030.18,3120.0,12031.19,12006.0,12032.21,7186.0,12033.26,11574.2,907.2,706.2,11758.5,11806.2,6577.1,936.2,11047.2,11569.5,4550.2,6313.2,11789.3,5345.1,11137.6,3280.1,11648.2,3445.2,6023.1,10976.2,7774.2,9269.2,11483.5,9031.2,9260.2,3059.1,463.1,7675.2,409.1,10195.1,2905.2,11071.2,11581.5,3139.1,11946.1,2707.1,2644.1,11421.4,7674.2,1729.1,11405.3,7347.1,11533.3,3272.1,5985.1,11100.3,4708.1,7216.2,7484.2,7426.2]:: p(n5,n2,n5),p(n8,n6,n1),p(n5,n3,n3),p(n6,n1,n6) -> p(n2,n1,n4),p(n3,n9,n8),p(n3,n6,n7),p(n6,n4,n8),p(n2,n9,n7),p(n3,n9,n7),p(n5,n9,n7),p(n4,n6,n7),p(n4,n8,n7),p(n4,n9,n7),p(n4,n7,n7),p(n4,n7,n1),p(n2,n4,n1),p(n2,n4,n3),p(n2,n4,n9)
% 2.28/1.06 === Conflict found: 11100:4:0:[10853.0,10246.0,10927.1,11096.3,10743.1,11097.4,10928.1,11098.5,10859.0,11099.7]:: -> p(n5,n2,n4),p(n5,n3,n4),p(n5,n7,n4),p(n5,n9,n4) {}
% 2.28/1.06 === Backtracking. Learning clause 12037:8:0:[12007.0,12035.0,12006.0,12036.4,11100.4,7426.2,7347.2,7216.2,11405.2,7674.1,11421.3,2707.2,11946.3,3148.2,3139.2,11071.1]:: p(n5,n3,n3) -> p(n5,n2,n4),p(n4,n7,n1),p(n4,n2,n7),p(n4,n6,n7),p(n4,n7,n7),p(n4,n8,n7),p(n4,n9,n7)
% 2.28/1.06 === Conflict found: 11648:5:0:[10704.1,10415.1,10639.0,11645.2,10638.0,11646.4,10923.1,11647.8]:: -> p(n6,n2,n1),p(n6,n2,n4),p(n6,n2,n6),p(n6,n2,n7),p(n6,n2,n8) {}
% 2.28/1.06 === Backtracking. Learning clause 12039:8:0:[823.0,12038.8,11648.3,1626.2,3280.2,11758.1,706.1]:: p(n6,n1,n6),p(n3,n8,n4) -> p(n6,n2,n1),p(n6,n2,n7),p(n6,n2,n8),p(n2,n1,n4),p(n2,n2,n4),p(n2,n3,n4)
% 2.28/1.06 === Conflict found: 11648:5:0:[10704.1,10415.1,10639.0,11645.2,10638.0,11646.4,10923.1,11647.8]:: -> p(n6,n2,n1),p(n6,n2,n4),p(n6,n2,n6),p(n6,n2,n7),p(n6,n2,n8) {}
% 2.28/1.06 === Backtracking. Learning clause 12040:5:0:[11648.3,1626.2,3280.2]:: p(n6,n1,n6),p(n1,n2,n4) -> p(n6,n2,n1),p(n6,n2,n7),p(n6,n2,n8)
% 2.28/1.06 === Conflict found: 11648:5:0:[10704.1,10415.1,10639.0,11645.2,10638.0,11646.4,10923.1,11647.8]:: -> p(n6,n2,n1),p(n6,n2,n4),p(n6,n2,n6),p(n6,n2,n7),p(n6,n2,n8) {}
% 2.28/1.06 === Backtracking. Learning clause 12041:5:0:[11648.3,1626.2]:: p(n6,n1,n6) -> p(n6,n2,n1),p(n6,n2,n4),p(n6,n2,n7),p(n6,n2,n8)
% 2.28/1.06 === Conflict found: 11137:7:0:[10867.1,10259.4,10759.1,11136.5]:: -> p(n6,n1,n8),p(n6,n2,n8),p(n6,n3,n8),p(n6,n4,n8),p(n6,n7,n8),p(n6,n8,n8),p(n6,n9,n8) {}
% 2.28/1.06 === Backtracking. Learning clause 12042:13:0:[11137.1,7484.2,5345.2,11047.3,6577.2,11758.6]:: p(n6,n1,n6) -> p(n6,n2,n8),p(n6,n3,n8),p(n6,n4,n8),p(n6,n7,n8),p(n6,n9,n8),p(n3,n1,n8),p(n3,n9,n8),p(n1,n2,n4),p(n2,n1,n4),p(n2,n2,n4),p(n2,n3,n4),p(n3,n1,n4)
% 2.28/1.06 === Conflict found: 11031:4:0:[10829.1,10229.1,10742.0,11027.4,10771.1,11028.6,10917.1,11029.7,10918.1,11030.8]:: -> p(n3,n1,n5),p(n3,n3,n5),p(n3,n4,n5),p(n3,n6,n5) {}
% 2.28/1.06 === Backtracking. Learning clause 12044:15:0:[1105.1,12043.11,11031.1,6502.2,9005.2,6581.1,11047.2,5345.1,11137.6,7484.2,12042.13,463.1,4550.2,9269.2,10976.2,12040.2,9260.2,3272.1,7774.2,3445.2,11483.5,3059.1,409.1,11533.3,7675.2,2905.2,10195.1,1729.1]:: p(n6,n1,n6),p(n5,n2,n5),p(n4,n2,n7),p(n4,n1,n8),p(n9,n7,n7),p(n6,n7,n1) -> p(n6,n4,n8),p(n3,n9,n8),p(n2,n1,n4),p(n2,n9,n7),p(n3,n9,n7),p(n5,n9,n7),p(n2,n4,n1),p(n2,n4,n3),p(n2,n4,n9)
% 2.28/1.06 === Conflict found: 11100:4:0:[10853.0,10246.0,10927.1,11096.3,10743.1,11097.4,10928.1,11098.5,10859.0,11099.7]:: -> p(n5,n2,n4),p(n5,n3,n4),p(n5,n7,n4),p(n5,n9,n4) {}
% 2.28/1.06 === Backtracking. Learning clause 12049:16:0:[12007.0,12045.0,7186.0,12046.6,1087.1,12047.17,12010.0,12048.18,11100.3,7347.2,7426.2,7216.2,11405.2,12044.6,11421.4]:: p(n5,n3,n3),p(n6,n1,n6),p(n5,n2,n5),p(n4,n2,n7),p(n4,n1,n8) -> p(n4,n7,n1),p(n6,n4,n8),p(n3,n9,n8),p(n2,n1,n4),p(n2,n9,n7),p(n3,n9,n7),p(n5,n9,n7),p(n2,n4,n1),p(n2,n4,n3),p(n2,n4,n9),p(n6,n7,n7)
% 2.28/1.06 === Conflict found: 11100:4:0:[10853.0,10246.0,10927.1,11096.3,10743.1,11097.4,10928.1,11098.5,10859.0,11099.7]:: -> p(n5,n2,n4),p(n5,n3,n4),p(n5,n7,n4),p(n5,n9,n4) {}
% 2.28/1.06 === Backtracking. Learning clause 12057:17:0:[12007.0,12050.0,9246.0,12051.13,3120.0,12052.14,1040.0,12053.20,1103.0,12054.21,1157.0,12055.22,7217.1,12056.23,11100.4,7426.2,7216.2,7347.2,11405.2,7674.1,12049.16,11581.5,979.1,12037.4,7120.2,11863.4]:: p(n6,n1,n6),p(n5,n3,n3),p(n4,n9,n5) -> p(n6,n4,n8),p(n3,n9,n8),p(n2,n1,n4),p(n2,n9,n7),p(n3,n9,n7),p(n5,n9,n7),p(n2,n4,n1),p(n2,n4,n3),p(n2,n4,n9),p(n5,n2,n4),p(n4,n7,n1),p(n4,n6,n7),p(n4,n7,n7),p(n4,n8,n7)
% 2.28/1.06 === Conflict found: 11071:6:0:[10713.1,10240.2,10732.0,11069.3,10848.1,11070.4]:: -> p(n4,n1,n7),p(n4,n2,n7),p(n4,n6,n7),p(n4,n7,n7),p(n4,n8,n7),p(n4,n9,n7) {}
% 2.28/1.06 === Backtracking. Learning clause 12058:6:0:[11071.6,7120.2]:: p(n4,n9,n5) -> p(n4,n1,n7),p(n4,n2,n7),p(n4,n6,n7),p(n4,n7,n7),p(n4,n8,n7)
% 2.28/1.06 === Conflict found: 11050:6:0:[10693.0,10233.0,10833.1,11048.1,10839.1,11049.6]:: -> p(n3,n3,n9),p(n3,n4,n9),p(n3,n5,n9),p(n3,n6,n9),p(n3,n8,n9),p(n3,n9,n9) {}
% 2.28/1.06 === Backtracking. Learning clause 12059:7:0:[11050.1,6588.2,6668.2,11023.3,6630.1,6659.2]:: p(n3,n3,n8),p(n3,n5,n7) -> p(n3,n4,n9),p(n3,n8,n9),p(n3,n9,n9),p(n3,n4,n1),p(n3,n9,n1)
% 2.28/1.06
% 2.28/1.06 Linear Model Building succeeded.
% 2.28/1.06 SZS status Satisfiable
% 2.28/1.06
% 2.28/1.06 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.28/1.06
% 2.28/1.06 SPASS-SCL-FOL Statistics:
% 2.28/1.06 Number of learned clauses: 24
% 2.28/1.06 Number of propagations: 5333
% 2.28/1.06 Number of decisions: 81
% 2.28/1.06 Number of resolutions: 219
% 2.28/1.06 Number of condensations: 0
% 2.28/1.06 Number of sub resolutions: 1488
% 2.28/1.06 Number of input literals (deduplicated): 729
% 2.28/1.06 Number of grows: 0
% 2.28/1.06 Number of considered ground atoms: 729
% 2.28/1.06
% 2.28/1.06 Needed: 0:00:00.49
% 2.28/1.06
%------------------------------------------------------------------------------