SPASS-SCL---0.1.SAT-Ass.s

%------------------------------------------------------------------------------
% File     : SPASS-SCL---0.1
% Problem  : PUZ068+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 : n009.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.75s 1.09s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14  % Problem  : PUZ068+2 : TPTP v9.2.1. Bugfixed v5.4.0.
% 0.11/0.14  % Command  : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.36  % Computer : n009.cluster.edu
% 0.18/0.36  % Model    : x86_64 x86_64
% 0.18/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.36  % Memory   : 8042.1875MB
% 0.18/0.36  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.36  % CPULimit : 300
% 0.18/0.36  % WCLimit  : 300
% 0.18/0.36  % DateTime : Thu May  7 12:57:56 EDT 2026
% 0.18/0.36  % CPUTime  : 
% 0.18/0.36  SPASS-SCL-FOL version:
% 0.18/0.45  SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 2.75/1.06  Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.75/1.06  Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.75/1.06  Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.75/1.06  Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.75/1.06  Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.75/1.06  Execution resolution_2 ended with status: satisfiable
% 2.75/1.06  Used heuristic: resolution_2
% 2.75/1.06  
% 2.75/1.06   Input Clauses:
% 2.75/1.08  
% 2.75/1.08   Predicates: p 
% 2.75/1.08   Fol Constants: n1 n2 n3 n4 n5 n6 n7 n8 n9 
% 2.75/1.08   Fol Functions: 
% 2.75/1.08   Problem Properties:
% 2.75/1.08   This is a first-order ground problem without equality.
% 2.75/1.08  
% 2.75/1.08   After reduction:  Problem Properties:
% 2.75/1.08   This is a first-order ground problem without equality.
% 2.75/1.08  
% 2.75/1.08  
% 2.75/1.08   Reduced Input Clauses:
% 2.75/1.08  10548:1:0:[10531.0,22.1]:: p(n1,n1,n4) -> 
% 2.75/1.08  10549:1:0:[10532.0,34.1]:: p(n1,n1,n7) -> 
% 2.75/1.08  10550:1:0:[10533.0,46.1]:: p(n1,n1,n1) -> 
% 2.75/1.08  10551:1:0:[10531.0,85.1]:: p(n1,n2,n4) -> 
% 2.75/1.08  10552:1:0:[10532.0,97.1]:: p(n1,n2,n7) -> 
% 2.75/1.08  10553:1:0:[10533.0,109.1]:: p(n1,n2,n1) -> 
% 2.75/1.08  11971:7:0:[10883.1,10530.1,10897.1,11970.8]::  -> p(n7,n7,n9),p(n7,n9,n9),p(n8,n7,n9),p(n8,n8,n9),p(n8,n9,n9),p(n9,n7,n9),p(n9,n8,n9)
% 2.75/1.08  11969:5:0:[10882.1,10529.1,10786.1,11966.2,10787.1,11967.5,10789.1,11968.8]::  -> p(n7,n7,n8),p(n8,n7,n8),p(n8,n8,n8),p(n9,n7,n8),p(n9,n8,n8)
% 2.75/1.08  11965:3:0:[10660.1,10528.0,10662.1,11960.1,10663.1,11961.2,10765.1,11962.3,10766.1,11963.6,10896.1,11964.8]::  -> p(n8,n8,n7),p(n8,n9,n7),p(n9,n8,n7)
% 2.75/1.08  11959:7:0:[10881.1,10527.1,10895.1,11958.8]::  -> p(n7,n7,n6),p(n7,n9,n6),p(n8,n7,n6),p(n8,n8,n6),p(n8,n9,n6),p(n9,n7,n6),p(n9,n8,n6)
% 2.75/1.08  11957:5:0:[10775.1,10526.1,10776.1,11954.4,10777.1,11955.7,10894.1,11956.8]::  -> p(n7,n7,n5),p(n7,n9,n5),p(n8,n7,n5),p(n8,n9,n5),p(n9,n7,n5)
% 2.75/1.08  10554:1:0:[10531.0,139.1]:: p(n1,n3,n4) -> 
% 2.75/1.08  11953:7:0:[10879.0,10523.1,10892.0,11952.8]::  -> p(n7,n7,n2),p(n7,n9,n2),p(n8,n7,n2),p(n8,n8,n2),p(n8,n9,n2),p(n9,n7,n2),p(n9,n8,n2)
% 2.75/1.08  10555:1:0:[10532.0,151.1]:: p(n1,n3,n7) -> 
% 2.75/1.08  11951:2:0:[10759.1,10522.0,10878.0,11945.1,10673.1,11946.3,10674.1,11947.4,10675.1,11948.5,10760.1,11949.6,10891.0,11950.8]::  -> p(n7,n9,n1),p(n9,n8,n1)
% 2.75/1.08  11944:8:0:[10877.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.75/1.08  10556:1:0:[10533.0,163.1]:: p(n1,n3,n1) -> 
% 2.75/1.08  11943:8:0:[10876.1,10520.0]::  -> p(n7,n5,n8),p(n7,n6,n8),p(n8,n4,n8),p(n8,n5,n8),p(n8,n6,n8),p(n9,n4,n8),p(n9,n5,n8),p(n9,n6,n8)
% 2.75/1.08  11942:8:0:[10875.0,10518.0]::  -> p(n7,n5,n6),p(n7,n6,n6),p(n8,n4,n6),p(n8,n5,n6),p(n8,n6,n6),p(n9,n4,n6),p(n9,n5,n6),p(n9,n6,n6)
% 2.75/1.08  11941:8:0:[10874.0,10517.0]::  -> p(n7,n5,n5),p(n7,n6,n5),p(n8,n4,n5),p(n8,n5,n5),p(n8,n6,n5),p(n9,n4,n5),p(n9,n5,n5),p(n9,n6,n5)
% 2.75/1.08  11940:4:0:[10722.1,10516.0,10723.1,11936.3,10679.0,11937.6,10680.0,11938.7,10681.0,11939.8]::  -> p(n7,n5,n4),p(n7,n6,n4),p(n8,n5,n4),p(n8,n6,n4)
% 2.75/1.08  11935:6:0:[10728.1,10514.0,10730.1,11933.3,10731.1,11934.6]::  -> p(n7,n5,n2),p(n7,n6,n2),p(n8,n5,n2),p(n8,n6,n2),p(n9,n5,n2),p(n9,n6,n2)
% 2.75/1.08  11932:3:0:[10873.0,10513.0,10747.1,11927.1,10670.1,11928.3,10671.1,11929.4,10672.1,11930.5,10748.1,11931.7]::  -> p(n7,n6,n1),p(n9,n4,n1),p(n9,n6,n1)
% 2.75/1.08  11926:8:0:[10890.1,10512.3]::  -> p(n7,n1,n9),p(n7,n2,n9),p(n7,n3,n9),p(n8,n2,n9),p(n8,n3,n9),p(n9,n1,n9),p(n9,n2,n9),p(n9,n3,n9)
% 2.75/1.08  11925:8:0:[10889.1,10511.3]::  -> p(n7,n1,n8),p(n7,n2,n8),p(n7,n3,n8),p(n8,n2,n8),p(n8,n3,n8),p(n9,n1,n8),p(n9,n2,n8),p(n9,n3,n8)
% 2.75/1.08  10557:1:0:[10531.0,193.0]:: p(n1,n5,n4) -> 
% 2.75/1.08  10558:1:0:[10532.0,196.1]:: p(n1,n4,n7) -> 
% 2.75/1.08  10559:1:0:[10531.0,202.0]:: p(n1,n6,n4) -> 
% 2.75/1.08  11924:5:0:[10652.0,10510.0,10654.0,11921.1,10656.0,11922.2,10888.1,11923.3]::  -> p(n8,n2,n7),p(n8,n3,n7),p(n9,n1,n7),p(n9,n2,n7),p(n9,n3,n7)
% 2.75/1.08  10560:1:0:[10533.0,208.1]:: p(n1,n4,n1) -> 
% 2.75/1.08  10561:1:0:[10531.0,211.0]:: p(n1,n7,n4) -> 
% 2.75/1.08  11920:6:0:[10691.1,10509.0,10692.1,11918.3,10693.1,11919.6]::  -> p(n7,n2,n6),p(n7,n3,n6),p(n8,n2,n6),p(n8,n3,n6),p(n9,n2,n6),p(n9,n3,n6)
% 2.75/1.08  11917:5:0:[10704.1,10508.1,10887.1,11914.3,10705.1,11915.4,10706.1,11916.7]::  -> p(n7,n1,n5),p(n7,n3,n5),p(n8,n3,n5),p(n9,n1,n5),p(n9,n3,n5)
% 2.75/1.08  10562:1:0:[10531.0,220.0]:: p(n1,n8,n4) -> 
% 2.75/1.08  11913:3:0:[10653.0,10506.0,10655.0,11908.1,10657.0,11909.2,10885.1,11910.3,10709.1,11911.4,10710.1,11912.7]::  -> p(n8,n3,n3),p(n9,n1,n3),p(n9,n3,n3)
% 2.75/1.08  11907:8:0:[10884.1,10505.3]::  -> p(n7,n1,n2),p(n7,n2,n2),p(n7,n3,n2),p(n8,n2,n2),p(n8,n3,n2),p(n9,n1,n2),p(n9,n2,n2),p(n9,n3,n2)
% 2.75/1.08  10563:1:0:[10531.0,229.0]:: p(n1,n9,n4) -> 
% 2.75/1.08  11906:7:0:[10851.1,10503.0,10872.1,11905.7]::  -> p(n4,n8,n9),p(n4,n9,n9),p(n5,n7,n9),p(n5,n8,n9),p(n5,n9,n9),p(n6,n7,n9),p(n6,n9,n9)
% 2.75/1.08  11904:4:0:[10850.1,10502.0,10783.1,11900.2,10784.1,11901.5,10871.1,11902.7,10785.1,11903.8]::  -> p(n4,n8,n8),p(n5,n7,n8),p(n5,n8,n8),p(n6,n7,n8)
% 2.75/1.08  10564:1:0:[10532.0,241.0]:: p(n1,n6,n7) -> 
% 2.75/1.08  10565:1:0:[10533.0,244.1]:: p(n1,n5,n1) -> 
% 2.75/1.08  11899:5:0:[10610.1,10500.0,10612.1,11896.1,10613.1,11897.2,10869.1,11898.7]::  -> p(n5,n7,n6),p(n5,n8,n6),p(n5,n9,n6),p(n6,n7,n6),p(n6,n9,n6)
% 2.75/1.08  10566:1:0:[10532.0,250.0]:: p(n1,n7,n7) -> 
% 2.75/1.08  11895:2:0:[10848.0,10498.0,10790.0,11889.2,10636.1,11890.3,10637.1,11891.4,10638.1,11892.5,10868.0,11893.7,10791.0,11894.8]::  -> p(n4,n8,n4),p(n6,n7,n4)
% 2.75/1.08  11888:3:0:[10847.0,10497.0,10772.0,11883.1,10641.1,11884.3,10642.1,11885.4,10643.1,11886.5,10774.0,11887.7]::  -> p(n4,n9,n3),p(n6,n7,n3),p(n6,n9,n3)
% 2.75/1.08  10567:1:0:[10532.0,259.0]:: p(n1,n8,n7) -> 
% 2.75/1.08  11882:7:0:[10846.0,10496.0,10867.0,11881.7]::  -> p(n4,n8,n2),p(n4,n9,n2),p(n5,n7,n2),p(n5,n8,n2),p(n5,n9,n2),p(n6,n7,n2),p(n6,n9,n2)
% 2.75/1.08  11880:3:0:[10621.1,10495.0,10623.1,11875.1,10624.1,11876.2,10757.1,11877.3,10758.1,11878.6,10866.0,11879.7]::  -> p(n5,n8,n1),p(n5,n9,n1),p(n6,n9,n1)
% 2.75/1.08  10568:1:0:[10532.0,268.0]:: p(n1,n9,n7) -> 
% 2.75/1.08  10569:1:0:[10533.0,271.1]:: p(n1,n6,n1) -> 
% 2.75/1.08  11874:7:0:[10845.1,10494.1,10865.1,11873.5]::  -> p(n4,n4,n9),p(n4,n6,n9),p(n5,n4,n9),p(n5,n5,n9),p(n6,n4,n9),p(n6,n5,n9),p(n6,n6,n9)
% 2.75/1.08  11872:7:0:[10844.1,10493.1,10864.1,11871.5]::  -> p(n4,n4,n8),p(n4,n6,n8),p(n5,n4,n8),p(n5,n5,n8),p(n6,n4,n8),p(n6,n5,n8),p(n6,n6,n8)
% 2.75/1.08  11870:5:0:[10606.1,10491.0,10608.1,11867.1,10609.1,11868.2,10862.1,11869.5]::  -> p(n5,n4,n6),p(n5,n5,n6),p(n6,n4,n6),p(n6,n5,n6),p(n6,n6,n6)
% 2.75/1.08  11866:4:0:[10843.1,10490.1,10861.1,11862.5,10647.0,11863.6,10648.0,11864.7,10649.0,11865.8]::  -> p(n4,n4,n5),p(n4,n6,n5),p(n5,n4,n5),p(n5,n5,n5)
% 2.75/1.08  11861:3:0:[10720.1,10489.0,10842.1,11856.1,10632.1,11857.3,10633.1,11858.4,10635.1,11859.5,10721.1,11860.6]::  -> p(n4,n6,n4),p(n6,n5,n4),p(n6,n6,n4)
% 2.75/1.08  11855:4:0:[10725.1,10487.0,10840.1,11851.1,10726.1,11852.3,10860.0,11853.5,10727.1,11854.6]::  -> p(n4,n6,n2),p(n5,n5,n2),p(n6,n5,n2),p(n6,n6,n2)
% 2.75/1.08  11850:7:0:[10839.1,10485.0,10858.1,11849.5]::  -> p(n4,n2,n9),p(n4,n3,n9),p(n5,n1,n9),p(n5,n2,n9),p(n6,n1,n9),p(n6,n2,n9),p(n6,n3,n9)
% 2.75/1.08  11848:7:0:[10838.1,10484.0,10857.1,11847.5]::  -> p(n4,n2,n8),p(n4,n3,n8),p(n5,n1,n8),p(n5,n2,n8),p(n6,n1,n8),p(n6,n2,n8),p(n6,n3,n8)
% 2.75/1.08  10570:1:0:[10533.0,298.0]:: p(n1,n8,n1) -> 
% 2.75/1.08  11846:2:0:[10837.0,10481.0,10702.1,11840.1,10703.1,11841.4,10854.1,11842.5,10644.0,11843.6,10645.0,11844.7,10646.0,11845.8]::  -> p(n4,n3,n5),p(n5,n1,n5)
% 2.75/1.08  11839:3:0:[10835.0,10479.0,10707.1,11834.1,10629.0,11835.3,10631.0,11836.4,10634.0,11837.5,10708.1,11838.7]::  -> p(n4,n3,n3),p(n6,n1,n3),p(n6,n3,n3)
% 2.75/1.08  10571:1:0:[10533.0,307.0]:: p(n1,n9,n1) -> 
% 2.75/1.08  11833:7:0:[10834.0,10478.0,10853.0,11832.5]::  -> p(n4,n2,n2),p(n4,n3,n2),p(n5,n1,n2),p(n5,n2,n2),p(n6,n1,n2),p(n6,n2,n2),p(n6,n3,n2)
% 2.75/1.08  11831:7:0:[10810.1,10476.0,10833.1,11830.8]::  -> p(n1,n8,n9),p(n1,n9,n9),p(n2,n7,n9),p(n2,n8,n9),p(n2,n9,n9),p(n3,n7,n9),p(n3,n8,n9)
% 2.75/1.08  11829:3:0:[10566.1,10474.0,10567.1,11824.1,10568.1,11825.2,10761.0,11826.3,10762.0,11827.6,10832.0,11828.8]::  -> p(n2,n8,n7),p(n2,n9,n7),p(n3,n8,n7)
% 2.75/1.08  11823:7:0:[10808.1,10473.0,10831.0,11822.8]::  -> p(n1,n8,n6),p(n1,n9,n6),p(n2,n7,n6),p(n2,n8,n6),p(n2,n9,n6),p(n3,n7,n6),p(n3,n8,n6)
% 2.75/1.08  11821:2:0:[10807.1,10472.0,10767.0,11815.1,10579.1,11816.3,10580.1,11817.4,10581.1,11818.5,10770.0,11819.7,10830.0,11820.8]::  -> p(n1,n9,n5),p(n3,n7,n5)
% 2.75/1.08  10572:1:0:[10534.0,329.1]:: p(n2,n1,n5) -> 
% 2.75/1.08  11814:4:0:[10561.1,10471.0,10562.1,11810.1,10563.1,11811.2,10782.0,11812.5,10788.0,11813.8]::  -> p(n2,n7,n4),p(n2,n8,n4),p(n3,n7,n4),p(n3,n8,n4)
% 2.75/1.08  10573:1:0:[10535.0,344.1]:: p(n2,n1,n2) -> 
% 2.75/1.08  11809:4:0:[10805.1,10469.0,10585.1,11805.3,10586.1,11806.4,10587.1,11807.5,10829.0,11808.8]::  -> p(n1,n8,n2),p(n1,n9,n2),p(n3,n7,n2),p(n3,n8,n2)
% 2.75/1.08  11804:6:0:[10798.1,10467.0,10804.1,11802.1,10821.1,11803.3]::  -> p(n1,n6,n9),p(n2,n5,n9),p(n2,n6,n9),p(n3,n4,n9),p(n3,n5,n9),p(n3,n6,n9)
% 2.75/1.08  11801:3:0:[10797.1,10466.0,10803.1,11796.1,10820.1,11797.3,10599.0,11798.6,10600.0,11799.7,10601.0,11800.8]::  -> p(n1,n6,n8),p(n2,n5,n8),p(n2,n6,n8)
% 2.75/1.08  11795:6:0:[10796.1,10464.0,10802.0,11793.1,10819.1,11794.3]::  -> p(n1,n6,n6),p(n2,n5,n6),p(n2,n6,n6),p(n3,n4,n6),p(n3,n5,n6),p(n3,n6,n6)
% 2.75/1.08  11792:4:0:[10795.1,10463.0,10801.0,11788.1,10576.1,11789.3,10577.1,11790.4,10578.1,11791.5]::  -> p(n1,n6,n5),p(n3,n4,n5),p(n3,n5,n5),p(n3,n6,n5)
% 2.75/1.08  11787:1:0:[10794.0,10461.0,10800.0,11780.1,10749.0,11781.2,10818.1,11782.3,10750.0,11783.5,10591.1,11784.6,10592.1,11785.7,10593.1,11786.8]::  -> p(n2,n5,n3)
% 2.75/1.08  11779:3:0:[10560.0,10459.0,10565.0,11774.1,10569.0,11775.2,10817.0,11776.3,10743.0,11777.4,10744.0,11778.7]::  -> p(n2,n6,n1),p(n3,n4,n1),p(n3,n6,n1)
% 2.75/1.08  11773:7:0:[10816.1,10458.4,10827.1,11772.7]::  -> p(n1,n1,n9),p(n1,n2,n9),p(n1,n3,n9),p(n2,n1,n9),p(n2,n3,n9),p(n3,n1,n9),p(n3,n3,n9)
% 2.75/1.08  11771:5:0:[10815.1,10457.4,10589.0,11768.6,10597.0,11769.7,10598.0,11770.8]::  -> p(n1,n1,n8),p(n1,n2,n8),p(n1,n3,n8),p(n2,n1,n8),p(n2,n3,n8)
% 2.75/1.08  11767:4:0:[10549.0,10456.0,10552.0,11763.1,10555.0,11764.2,10814.1,11765.4,10826.1,11766.7]::  -> p(n2,n1,n7),p(n2,n3,n7),p(n3,n1,n7),p(n3,n3,n7)
% 2.75/1.08  11762:4:0:[10684.0,10455.0,10685.0,11758.3,10813.1,11759.4,10687.0,11760.6,10825.1,11761.7]::  -> p(n1,n2,n6),p(n1,n3,n6),p(n2,n3,n6),p(n3,n3,n6)
% 2.75/1.08  10574:1:0:[10534.0,401.0]:: p(n2,n3,n5) -> 
% 2.75/1.08  10575:1:0:[10535.0,407.1]:: p(n2,n2,n2) -> 
% 2.75/1.08  10576:1:0:[10534.0,410.0]:: p(n2,n4,n5) -> 
% 2.75/1.08  11757:2:0:[10548.0,10453.0,10551.0,11751.1,10554.0,11752.2,10812.0,11753.4,10711.0,11754.5,10824.1,11755.7,10712.0,11756.8]::  -> p(n2,n1,n4),p(n3,n1,n4)
% 2.75/1.08  10577:1:0:[10534.0,419.0]:: p(n2,n5,n5) -> 
% 2.75/1.08  11750:5:0:[10573.0,10451.3,10575.0,11747.4,10582.0,11748.5,10823.0,11749.7]::  -> p(n1,n1,n2),p(n1,n2,n2),p(n1,n3,n2),p(n3,n1,n2),p(n3,n3,n2)
% 2.75/1.08  10578:1:0:[10534.0,428.0]:: p(n2,n6,n5) -> 
% 2.75/1.08  11746:2:0:[10550.0,10450.0,10553.0,11740.1,10556.0,11741.2,10686.0,11742.3,10811.0,11743.4,10688.0,11744.6,10822.0,11745.7]::  -> p(n2,n3,n1),p(n3,n3,n1)
% 2.75/1.08  10579:1:0:[10534.0,437.0]:: p(n2,n7,n5) -> 
% 2.75/1.08  11739:6:0:[10779.1,10448.2,10683.0,11737.3,10777.1,11738.4]::  -> p(n9,n8,n1),p(n9,n8,n2),p(n9,n8,n6),p(n9,n8,n7),p(n9,n8,n8),p(n9,n8,n9)
% 2.75/1.08  10580:1:0:[10534.0,446.0]:: p(n2,n8,n5) -> 
% 2.75/1.08  11736:5:0:[10760.1,10447.0,10948.1,11733.2,10682.0,11734.3,10766.1,11735.6]::  -> p(n9,n7,n2),p(n9,n7,n5),p(n9,n7,n6),p(n9,n7,n8),p(n9,n7,n9)
% 2.75/1.08  10581:1:0:[10534.0,455.0]:: p(n2,n9,n5) -> 
% 2.75/1.08  10582:1:0:[10535.0,461.1]:: p(n2,n3,n2) -> 
% 2.75/1.08  11732:6:0:[10754.1,10446.2,10681.0,11730.3,10944.1,11731.6]::  -> p(n9,n6,n1),p(n9,n6,n2),p(n9,n6,n5),p(n9,n6,n6),p(n9,n6,n8),p(n9,n6,n9)
% 2.75/1.08  11729:6:0:[10748.1,10445.0,10680.0,11727.3,10742.1,11728.6]::  -> p(n9,n5,n2),p(n9,n5,n3),p(n9,n5,n5),p(n9,n5,n6),p(n9,n5,n8),p(n9,n5,n9)
% 2.75/1.08  11726:6:0:[10731.1,10444.1,10679.0,11724.3,10736.1,11725.6]::  -> p(n9,n4,n1),p(n9,n4,n3),p(n9,n4,n5),p(n9,n4,n6),p(n9,n4,n8),p(n9,n4,n9)
% 2.75/1.08  11723:7:0:[10942.1,10443.0,10678.0,11722.3]::  -> p(n9,n3,n2),p(n9,n3,n3),p(n9,n3,n5),p(n9,n3,n6),p(n9,n3,n7),p(n9,n3,n8),p(n9,n3,n9)
% 2.75/1.08  11721:5:0:[10941.1,10442.0,10710.1,11718.2,10677.0,11719.3,10706.1,11720.4]::  -> p(n9,n2,n2),p(n9,n2,n6),p(n9,n2,n7),p(n9,n2,n8),p(n9,n2,n9)
% 2.75/1.08  11717:6:0:[10697.1,10441.0,10676.0,11715.3,10693.1,11716.5]::  -> p(n9,n1,n2),p(n9,n1,n3),p(n9,n1,n5),p(n9,n1,n7),p(n9,n1,n8),p(n9,n1,n9)
% 2.75/1.08  11714:5:0:[10675.1,10440.0,10947.1,11711.2,10793.0,11712.3,10787.1,11713.7]::  -> p(n8,n9,n2),p(n8,n9,n5),p(n8,n9,n6),p(n8,n9,n7),p(n8,n9,n9)
% 2.75/1.08  11710:5:0:[10674.1,10439.0,10778.1,11707.2,10950.0,11708.3,10776.1,11709.4]::  -> p(n8,n8,n2),p(n8,n8,n6),p(n8,n8,n7),p(n8,n8,n8),p(n8,n8,n9)
% 2.75/1.08  11706:5:0:[10673.1,10438.0,10946.1,11703.2,10949.0,11704.3,10765.1,11705.6]::  -> p(n8,n7,n2),p(n8,n7,n5),p(n8,n7,n6),p(n8,n7,n8),p(n8,n7,n9)
% 2.75/1.08  11702:6:0:[10672.1,10437.0,10753.1,11700.2,10943.1,11701.6]::  -> p(n8,n6,n2),p(n8,n6,n4),p(n8,n6,n5),p(n8,n6,n6),p(n8,n6,n8),p(n8,n6,n9)
% 2.75/1.08  11699:7:0:[10671.1,10436.0,10741.1,11698.6]::  -> p(n8,n5,n2),p(n8,n5,n3),p(n8,n5,n4),p(n8,n5,n5),p(n8,n5,n6),p(n8,n5,n8),p(n8,n5,n9)
% 2.75/1.08  10583:1:0:[10535.0,515.0]:: p(n2,n5,n2) -> 
% 2.75/1.08  11697:5:0:[10670.1,10435.0,10730.1,11694.1,10723.1,11695.3,10735.1,11696.6]::  -> p(n8,n4,n3),p(n8,n4,n5),p(n8,n4,n6),p(n8,n4,n8),p(n8,n4,n9)
% 2.75/1.08  10584:1:0:[10535.0,524.0]:: p(n2,n6,n2) -> 
% 2.75/1.08  11693:7:0:[10669.1,10434.0,10716.1,11692.3]::  -> p(n8,n3,n2),p(n8,n3,n3),p(n8,n3,n5),p(n8,n3,n6),p(n8,n3,n7),p(n8,n3,n8),p(n8,n3,n9)
% 2.75/1.08  10585:1:0:[10535.0,533.0]:: p(n2,n7,n2) -> 
% 2.75/1.08  11691:6:0:[10668.1,10433.0,10709.1,11689.2,10705.1,11690.4]::  -> p(n8,n2,n2),p(n8,n2,n4),p(n8,n2,n6),p(n8,n2,n7),p(n8,n2,n8),p(n8,n2,n9)
% 2.75/1.08  10586:1:0:[10535.0,542.0]:: p(n2,n8,n2) -> 
% 2.75/1.08  11688:5:0:[10667.1,10431.2,10792.0,11685.3,10663.1,11686.6,10786.1,11687.7]::  -> p(n7,n9,n1),p(n7,n9,n2),p(n7,n9,n5),p(n7,n9,n6),p(n7,n9,n9)
% 2.75/1.08  10587:1:0:[10535.0,551.0]:: p(n2,n9,n2) -> 
% 2.75/1.08  11684:5:0:[10759.1,10429.0,10666.0,11681.2,10945.0,11682.3,10660.1,11683.6]::  -> p(n7,n7,n2),p(n7,n7,n5),p(n7,n7,n6),p(n7,n7,n8),p(n7,n7,n9)
% 2.75/1.08  11680:7:0:[10665.0,10428.2,10659.1,11679.6]::  -> p(n7,n6,n1),p(n7,n6,n2),p(n7,n6,n4),p(n7,n6,n5),p(n7,n6,n6),p(n7,n6,n8),p(n7,n6,n9)
% 2.75/1.08  11678:6:0:[10747.1,10427.0,10664.0,11676.2,10658.1,11677.6]::  -> p(n7,n5,n2),p(n7,n5,n4),p(n7,n5,n5),p(n7,n5,n6),p(n7,n5,n8),p(n7,n5,n9)
% 2.75/1.08  11675:5:0:[10940.0,10425.0,10657.0,11672.2,10715.1,11673.3,10656.0,11674.6]::  -> p(n7,n3,n2),p(n7,n3,n5),p(n7,n3,n6),p(n7,n3,n8),p(n7,n3,n9)
% 2.75/1.08  11671:5:0:[10939.0,10424.0,10655.0,11668.2,10704.1,11669.4,10654.0,11670.6]::  -> p(n7,n2,n2),p(n7,n2,n4),p(n7,n2,n6),p(n7,n2,n8),p(n7,n2,n9)
% 2.75/1.08  11667:5:0:[10696.0,10423.0,10653.0,11664.2,10691.1,11665.5,10652.0,11666.6]::  -> p(n7,n1,n2),p(n7,n1,n4),p(n7,n1,n5),p(n7,n1,n8),p(n7,n1,n9)
% 2.75/1.08  11663:5:0:[10791.0,10422.3,10651.1,11660.4,10935.1,11661.6,10785.1,11662.7]::  -> p(n6,n9,n1),p(n6,n9,n2),p(n6,n9,n3),p(n6,n9,n6),p(n6,n9,n9)
% 2.75/1.08  11659:6:0:[10758.1,10420.0,10650.0,11657.4,10764.1,11658.6]::  -> p(n6,n7,n2),p(n6,n7,n3),p(n6,n7,n4),p(n6,n7,n6),p(n6,n7,n8),p(n6,n7,n9)
% 2.75/1.08  11656:5:0:[10746.1,10418.0,10932.1,11653.2,10648.0,11654.4,10740.1,11655.6]::  -> p(n6,n5,n2),p(n6,n5,n4),p(n6,n5,n6),p(n6,n5,n8),p(n6,n5,n9)
% 2.75/1.08  11652:3:0:[10929.1,10417.0,10727.1,11647.1,10931.1,11648.2,10721.1,11649.3,10647.0,11650.4,10734.0,11651.6]::  -> p(n6,n4,n6),p(n6,n4,n8),p(n6,n4,n9)
% 2.75/1.08  11646:6:0:[10714.1,10416.3,10646.0,11644.4,10923.1,11645.5]::  -> p(n6,n3,n1),p(n6,n3,n2),p(n6,n3,n3),p(n6,n3,n7),p(n6,n3,n8),p(n6,n3,n9)
% 2.75/1.08  11643:5:0:[10708.1,10415.2,10926.1,11640.3,10645.0,11641.4,10922.1,11642.5]::  -> p(n6,n2,n1),p(n6,n2,n2),p(n6,n2,n7),p(n6,n2,n8),p(n6,n2,n9)
% 2.75/1.08  11639:5:0:[10695.0,10414.0,10925.1,11636.3,10644.0,11637.4,10690.1,11638.5]::  -> p(n6,n1,n2),p(n6,n1,n3),p(n6,n1,n7),p(n6,n1,n8),p(n6,n1,n9)
% 2.75/1.08  11635:4:0:[10643.1,10413.2,10638.1,11631.3,10938.0,11632.4,10934.1,11633.6,10784.1,11634.7]::  -> p(n5,n9,n1),p(n5,n9,n2),p(n5,n9,n6),p(n5,n9,n9)
% 2.75/1.08  11630:5:0:[10642.1,10412.2,10637.1,11627.3,10773.0,11628.4,10933.1,11629.6]::  -> p(n5,n8,n1),p(n5,n8,n2),p(n5,n8,n6),p(n5,n8,n8),p(n5,n8,n9)
% 2.75/1.08  11626:4:0:[10757.1,10411.0,10641.1,11622.2,10636.1,11623.3,10937.0,11624.4,10763.1,11625.6]::  -> p(n5,n7,n2),p(n5,n7,n6),p(n5,n7,n8),p(n5,n7,n9)
% 2.75/1.08  11621:5:0:[10745.1,10409.0,10640.0,11618.2,10633.1,11619.3,10739.1,11620.6]::  -> p(n5,n5,n2),p(n5,n5,n5),p(n5,n5,n6),p(n5,n5,n8),p(n5,n5,n9)
% 2.75/1.08  11617:4:0:[10928.1,10408.0,10726.1,11613.1,10639.0,11614.2,10632.1,11615.3,10733.0,11616.6]::  -> p(n5,n4,n5),p(n5,n4,n6),p(n5,n4,n8),p(n5,n4,n9)
% 2.75/1.08  11612:5:0:[10631.0,10406.2,10630.0,11609.3,10703.1,11610.4,10921.1,11611.5]::  -> p(n5,n2,n1),p(n5,n2,n2),p(n5,n2,n7),p(n5,n2,n8),p(n5,n2,n9)
% 2.75/1.08  11608:5:0:[10694.0,10405.0,10629.0,11605.2,10628.0,11606.3,10689.1,11607.5]::  -> p(n5,n1,n2),p(n5,n1,n5),p(n5,n1,n7),p(n5,n1,n8),p(n5,n1,n9)
% 2.75/1.08  11604:3:0:[10624.1,10404.0,10790.0,11599.3,10936.0,11600.4,10613.1,11601.5,10627.1,11602.6,10783.1,11603.7]::  -> p(n4,n9,n2),p(n4,n9,n3),p(n4,n9,n9)
% 2.75/1.08  10588:1:0:[10536.0,651.1]:: p(n3,n1,n3) -> 
% 2.75/1.08  11598:4:0:[10623.1,10403.0,10772.0,11594.2,10771.0,11595.4,10612.1,11596.5,10626.1,11597.6]::  -> p(n4,n8,n2),p(n4,n8,n4),p(n4,n8,n8),p(n4,n8,n9)
% 2.75/1.08  11593:5:0:[10620.1,10401.0,10751.0,11590.2,10609.1,11591.5,10625.0,11592.6]::  -> p(n4,n6,n2),p(n4,n6,n4),p(n4,n6,n5),p(n4,n6,n8),p(n4,n6,n9)
% 2.75/1.08  11589:3:0:[10618.0,10399.0,10725.1,11584.1,10927.0,11585.2,10720.1,11586.3,10606.1,11587.5,10619.0,11588.6]::  -> p(n4,n4,n5),p(n4,n4,n8),p(n4,n4,n9)
% 2.75/1.08  11583:5:0:[10616.0,10398.0,10713.0,11580.3,10605.1,11581.5,10617.0,11582.6]::  -> p(n4,n3,n2),p(n4,n3,n3),p(n4,n3,n5),p(n4,n3,n8),p(n4,n3,n9)
% 2.75/1.08  11579:3:0:[10614.0,10397.0,10707.1,11574.2,10924.0,11575.3,10702.1,11576.4,10604.1,11577.5,10615.0,11578.6]::  -> p(n4,n2,n2),p(n4,n2,n8),p(n4,n2,n9)
% 2.75/1.08  11573:5:0:[10917.1,10394.0,10595.1,11570.2,10770.0,11571.4,10603.0,11572.7]::  -> p(n3,n8,n2),p(n3,n8,n4),p(n3,n8,n6),p(n3,n8,n7),p(n3,n8,n9)
% 2.75/1.08  11569:5:0:[10756.1,10393.0,10594.1,11566.2,10762.0,11567.6,10602.0,11568.7]::  -> p(n3,n7,n2),p(n3,n7,n4),p(n3,n7,n5),p(n3,n7,n6),p(n3,n7,n9)
% 2.75/1.08  10589:1:0:[10537.0,719.1]:: p(n3,n1,n8) -> 
% 2.75/1.08  10590:1:0:[10536.0,723.0]:: p(n3,n3,n3) -> 
% 2.75/1.08  10591:1:0:[10536.0,732.0]:: p(n3,n4,n3) -> 
% 2.75/1.08  10592:1:0:[10536.0,741.0]:: p(n3,n5,n3) -> 
% 2.75/1.08  10593:1:0:[10536.0,750.0]:: p(n3,n6,n3) -> 
% 2.75/1.08  10594:1:0:[10536.0,759.0]:: p(n3,n7,n3) -> 
% 2.75/1.08  10595:1:0:[10536.0,768.0]:: p(n3,n8,n3) -> 
% 2.75/1.08  10596:1:0:[10536.0,777.0]:: p(n3,n9,n3) -> 
% 2.75/1.08  10597:1:0:[10537.0,782.1]:: p(n3,n2,n8) -> 
% 2.75/1.08  11565:4:0:[10914.1,10392.1,10593.1,11561.2,10909.1,11562.3,10911.1,11563.6,10601.0,11564.7]::  -> p(n3,n6,n1),p(n3,n6,n5),p(n3,n6,n6),p(n3,n6,n9)
% 2.75/1.08  11560:3:0:[10744.0,10391.0,10913.1,11555.1,10592.1,11556.2,10908.1,11557.3,10738.1,11558.6,10600.0,11559.7]::  -> p(n3,n5,n5),p(n3,n5,n6),p(n3,n5,n9)
% 2.75/1.08  11554:4:0:[10724.1,10390.1,10591.1,11550.2,10719.1,11551.3,10732.0,11552.6,10599.0,11553.7]::  -> p(n3,n4,n1),p(n3,n4,n5),p(n3,n4,n6),p(n3,n4,n9)
% 2.75/1.08  11549:5:0:[10590.1,10389.2,10712.0,11546.3,10904.1,11547.4,10598.0,11548.7]::  -> p(n3,n3,n1),p(n3,n3,n2),p(n3,n3,n6),p(n3,n3,n7),p(n3,n3,n9)
% 2.75/1.08  11545:4:0:[10688.0,10387.0,10588.0,11541.2,10903.1,11542.4,10687.0,11543.5,10589.0,11544.7]::  -> p(n3,n1,n2),p(n3,n1,n4),p(n3,n1,n7),p(n3,n1,n9)
% 2.75/1.08  11540:4:0:[10916.1,10386.0,10587.1,11536.1,10782.0,11537.3,10581.1,11538.4,10781.0,11539.7]::  -> p(n2,n9,n3),p(n2,n9,n6),p(n2,n9,n7),p(n2,n9,n9)
% 2.75/1.08  10598:1:0:[10537.0,836.1]:: p(n3,n3,n8) -> 
% 2.75/1.08  11535:4:0:[10915.1,10385.0,10586.1,11531.1,10769.0,11532.2,10580.1,11533.4,10920.0,11534.7]::  -> p(n2,n8,n4),p(n2,n8,n6),p(n2,n8,n7),p(n2,n8,n9)
% 2.75/1.08  11530:4:0:[10755.1,10384.0,10585.1,11526.1,10579.1,11527.4,10761.0,11528.6,10919.0,11529.7]::  -> p(n2,n7,n3),p(n2,n7,n4),p(n2,n7,n6),p(n2,n7,n9)
% 2.75/1.08  11525:4:0:[10584.1,10383.1,10750.0,11521.2,10907.1,11522.3,10578.1,11523.4,10910.1,11524.6]::  -> p(n2,n6,n1),p(n2,n6,n6),p(n2,n6,n8),p(n2,n6,n9)
% 2.75/1.08  11520:4:0:[10743.0,10382.0,10583.1,11516.1,10906.1,11517.3,10577.1,11518.4,10737.1,11519.6]::  -> p(n2,n5,n3),p(n2,n5,n6),p(n2,n5,n8),p(n2,n5,n9)
% 2.75/1.08  11515:5:0:[10582.0,10380.1,10905.0,11512.2,10711.0,11513.3,10574.1,11514.4]::  -> p(n2,n3,n1),p(n2,n3,n6),p(n2,n3,n7),p(n2,n3,n8),p(n2,n3,n9)
% 2.75/1.08  10599:1:0:[10537.0,881.1]:: p(n3,n4,n8) -> 
% 2.75/1.08  11511:4:0:[10686.0,10378.0,10573.0,11507.1,10902.0,11508.2,10572.0,11509.4,10685.0,11510.5]::  -> p(n2,n1,n4),p(n2,n1,n7),p(n2,n1,n8),p(n2,n1,n9)
% 2.75/1.08  11506:3:0:[10570.1,10376.0,10768.0,11501.2,10562.1,11502.3,10767.0,11503.4,10567.1,11504.6,10918.0,11505.7]::  -> p(n1,n8,n2),p(n1,n8,n6),p(n1,n8,n9)
% 2.75/1.08  11500:4:0:[10569.0,10374.0,10912.0,11496.1,10749.0,11497.2,10559.1,11498.3,10564.1,11499.6]::  -> p(n1,n6,n5),p(n1,n6,n6),p(n1,n6,n8),p(n1,n6,n9)
% 2.75/1.08  11495:4:0:[10556.0,10371.0,10901.0,11491.2,10554.0,11492.3,10900.0,11493.4,10555.0,11494.6]::  -> p(n1,n3,n2),p(n1,n3,n6),p(n1,n3,n8),p(n1,n3,n9)
% 2.75/1.08  10600:1:0:[10537.0,917.1]:: p(n3,n5,n8) -> 
% 2.75/1.08  11490:4:0:[10553.0,10370.0,10699.0,11486.2,10551.0,11487.3,10698.0,11488.4,10552.0,11489.6]::  -> p(n1,n2,n2),p(n1,n2,n6),p(n1,n2,n8),p(n1,n2,n9)
% 2.75/1.08  11485:3:0:[10550.0,10369.0,10899.0,11480.2,10548.0,11481.3,10898.0,11482.4,10684.0,11483.5,10549.0,11484.6]::  -> p(n1,n1,n2),p(n1,n1,n8),p(n1,n1,n9)
% 2.75/1.08  11479:7:0:[10833.1,10368.2,10897.1,11478.8]::  -> p(n1,n9,n9),p(n2,n9,n9),p(n4,n9,n9),p(n5,n9,n9),p(n6,n9,n9),p(n7,n9,n9),p(n8,n9,n9)
% 2.75/1.08  10601:1:0:[10537.0,944.1]:: p(n3,n6,n8) -> 
% 2.75/1.08  11477:2:0:[10568.1,10366.0,10832.0,11471.2,10627.1,11472.3,10934.1,11473.4,10935.1,11474.5,10663.1,11475.6,10896.1,11476.8]::  -> p(n2,n9,n7),p(n8,n9,n7)
% 2.75/1.08  11470:6:0:[10831.0,10365.2,10613.1,11468.3,10895.1,11469.8]::  -> p(n1,n9,n6),p(n2,n9,n6),p(n5,n9,n6),p(n6,n9,n6),p(n7,n9,n6),p(n8,n9,n6)
% 2.75/1.08  10602:1:0:[10537.0,962.1]:: p(n3,n7,n8) -> 
% 2.75/1.08  11467:3:0:[10581.1,10364.1,10830.0,11462.2,10936.0,11463.3,10938.0,11464.4,10651.1,11465.5,10894.1,11466.8]::  -> p(n1,n9,n5),p(n7,n9,n5),p(n8,n9,n5)
% 2.75/1.08  10603:1:0:[10537.0,971.1]:: p(n3,n8,n8) -> 
% 2.75/1.08  10604:1:0:[10538.0,978.0]:: p(n4,n2,n6) -> 
% 2.75/1.08  10605:1:0:[10538.0,987.0]:: p(n4,n3,n6) -> 
% 2.75/1.08  10606:1:0:[10538.0,996.0]:: p(n4,n4,n6) -> 
% 2.75/1.08  10607:1:0:[10539.0,1000.1]:: p(n4,n1,n1) -> 
% 2.75/1.08  10608:1:0:[10538.0,1005.0]:: p(n4,n5,n6) -> 
% 2.75/1.08  11461:6:0:[10587.1,10361.1,10829.0,11459.2,10892.0,11460.8]::  -> p(n1,n9,n2),p(n4,n9,n2),p(n5,n9,n2),p(n6,n9,n2),p(n7,n9,n2),p(n8,n9,n2)
% 2.75/1.08  10609:1:0:[10538.0,1014.0]:: p(n4,n6,n6) -> 
% 2.75/1.08  11458:3:0:[10571.1,10360.0,10916.1,11453.1,10828.0,11454.2,10624.1,11455.3,10675.1,11456.7,10891.0,11457.8]::  -> p(n5,n9,n1),p(n6,n9,n1),p(n7,n9,n1)
% 2.75/1.08  10610:1:0:[10538.0,1023.0]:: p(n4,n7,n6) -> 
% 2.75/1.08  10611:1:0:[10540.0,1024.1]:: p(n4,n1,n7) -> 
% 2.75/1.08  11452:7:0:[10872.1,10359.5,10883.1,11451.6]::  -> p(n1,n8,n9),p(n2,n8,n9),p(n3,n8,n9),p(n4,n8,n9),p(n5,n8,n9),p(n8,n8,n9),p(n9,n8,n9)
% 2.75/1.08  10612:1:0:[10538.0,1032.0]:: p(n4,n8,n6) -> 
% 2.75/1.08  11450:4:0:[10918.0,10358.0,10920.0,11446.1,10603.0,11447.2,10871.1,11448.5,10882.1,11449.6]::  -> p(n4,n8,n8),p(n5,n8,n8),p(n8,n8,n8),p(n9,n8,n8)
% 2.75/1.08  11445:4:0:[10567.1,10357.0,10626.1,11441.3,10933.1,11442.4,10870.1,11443.5,10662.1,11444.6]::  -> p(n2,n8,n7),p(n3,n8,n7),p(n8,n8,n7),p(n9,n8,n7)
% 2.75/1.08  10613:1:0:[10538.0,1041.0]:: p(n4,n9,n6) -> 
% 2.75/1.08  11440:6:0:[10612.1,10356.3,10869.1,11438.5,10881.1,11439.6]::  -> p(n1,n8,n6),p(n2,n8,n6),p(n3,n8,n6),p(n5,n8,n6),p(n8,n8,n6),p(n9,n8,n6)
% 2.75/1.08  11437:3:0:[10562.1,10354.0,10637.1,11432.4,10868.0,11433.5,10880.1,11434.6,10950.0,11435.7,10683.0,11436.8]::  -> p(n2,n8,n4),p(n3,n8,n4),p(n4,n8,n4)
% 2.75/1.08  11431:6:0:[10586.1,10352.1,10867.0,11429.5,10879.0,11430.6]::  -> p(n1,n8,n2),p(n3,n8,n2),p(n4,n8,n2),p(n5,n8,n2),p(n8,n8,n2),p(n9,n8,n2)
% 2.75/1.08  10614:1:0:[10539.0,1063.1]:: p(n4,n2,n1) -> 
% 2.75/1.08  11428:2:0:[10570.1,10351.0,10915.1,11422.1,10917.1,11423.2,10623.1,11424.3,10866.0,11425.5,10878.0,11426.6,10674.1,11427.7]::  -> p(n5,n8,n1),p(n9,n8,n1)
% 2.75/1.08  11421:7:0:[10810.1,10350.0,10851.1,11420.3]::  -> p(n2,n7,n9),p(n3,n7,n9),p(n5,n7,n9),p(n6,n7,n9),p(n7,n7,n9),p(n8,n7,n9),p(n9,n7,n9)
% 2.75/1.08  11419:5:0:[10809.1,10349.0,10919.0,11416.1,10602.0,11417.2,10850.1,11418.3]::  -> p(n5,n7,n8),p(n6,n7,n8),p(n7,n7,n8),p(n8,n7,n8),p(n9,n7,n8)
% 2.75/1.08  11415:7:0:[10808.1,10347.0,10610.1,11414.3]::  -> p(n2,n7,n6),p(n3,n7,n6),p(n5,n7,n6),p(n6,n7,n6),p(n7,n7,n6),p(n8,n7,n6),p(n9,n7,n6)
% 2.75/1.08  11413:4:0:[10807.1,10346.0,10579.1,11409.1,10849.0,11410.3,10937.0,11411.4,10650.0,11412.5]::  -> p(n3,n7,n5),p(n7,n7,n5),p(n8,n7,n5),p(n9,n7,n5)
% 2.75/1.08  10615:1:0:[10540.0,1087.1]:: p(n4,n2,n7) -> 
% 2.75/1.08  11408:3:0:[10561.1,10345.0,10848.0,11403.3,10636.1,11404.4,10945.0,11405.6,10949.0,11406.7,10682.0,11407.8]::  -> p(n2,n7,n4),p(n3,n7,n4),p(n6,n7,n4)
% 2.75/1.08  11402:2:0:[10806.1,10344.0,10594.1,11396.2,10847.0,11397.3,10641.1,11398.4,10666.0,11399.6,10946.1,11400.7,10948.1,11401.8]::  -> p(n2,n7,n3),p(n6,n7,n3)
% 2.75/1.08  11395:6:0:[10805.1,10343.0,10585.1,11393.1,10846.0,11394.3]::  -> p(n3,n7,n2),p(n5,n7,n2),p(n6,n7,n2),p(n7,n7,n2),p(n8,n7,n2),p(n9,n7,n2)
% 2.75/1.08  11392:8:0:[10865.1,10341.4]::  -> p(n1,n6,n9),p(n2,n6,n9),p(n3,n6,n9),p(n4,n6,n9),p(n6,n6,n9),p(n7,n6,n9),p(n8,n6,n9),p(n9,n6,n9)
% 2.75/1.08  11391:7:0:[10601.0,10340.2,10864.1,11390.4]::  -> p(n1,n6,n8),p(n2,n6,n8),p(n4,n6,n8),p(n6,n6,n8),p(n7,n6,n8),p(n8,n6,n8),p(n9,n6,n8)
% 2.75/1.08  11389:1:0:[10564.1,10339.0,10910.1,11382.1,10911.1,11383.2,10625.0,11384.3,10863.1,11385.4,10659.1,11386.6,10943.1,11387.7,10944.1,11388.8]::  -> p(n6,n6,n7)
% 2.75/1.08  11381:7:0:[10609.1,10338.3,10862.1,11380.4]::  -> p(n1,n6,n6),p(n2,n6,n6),p(n3,n6,n6),p(n6,n6,n6),p(n7,n6,n6),p(n8,n6,n6),p(n9,n6,n6)
% 2.75/1.08  10616:1:0:[10539.0,1117.1]:: p(n4,n3,n1) -> 
% 2.75/1.08  11379:6:0:[10578.1,10337.1,10861.1,11377.4,10649.0,11378.5]::  -> p(n1,n6,n5),p(n3,n6,n5),p(n4,n6,n5),p(n7,n6,n5),p(n8,n6,n5),p(n9,n6,n5)
% 2.75/1.08  11376:4:0:[10559.1,10336.0,10907.1,11372.1,10909.1,11373.2,10635.1,11374.4,10681.0,11375.8]::  -> p(n4,n6,n4),p(n6,n6,n4),p(n7,n6,n4),p(n8,n6,n4)
% 2.75/1.08  11371:5:0:[10912.0,10334.0,10584.1,11368.1,10914.1,11369.2,10860.0,11370.4]::  -> p(n4,n6,n2),p(n6,n6,n2),p(n7,n6,n2),p(n8,n6,n2),p(n9,n6,n2)
% 2.75/1.08  11367:4:0:[10569.0,10333.0,10620.1,11363.3,10859.0,11364.4,10930.1,11365.5,10672.1,11366.7]::  -> p(n2,n6,n1),p(n3,n6,n1),p(n7,n6,n1),p(n9,n6,n1)
% 2.75/1.08  11362:7:0:[10804.1,10332.0,10845.1,11361.3]::  -> p(n2,n5,n9),p(n3,n5,n9),p(n5,n5,n9),p(n6,n5,n9),p(n7,n5,n9),p(n8,n5,n9),p(n9,n5,n9)
% 2.75/1.08  10617:1:0:[10540.0,1141.1]:: p(n4,n3,n7) -> 
% 2.75/1.08  11360:6:0:[10803.1,10331.0,10600.0,11358.2,10844.1,11359.3]::  -> p(n2,n5,n8),p(n5,n5,n8),p(n6,n5,n8),p(n7,n5,n8),p(n8,n5,n8),p(n9,n5,n8)
% 2.75/1.08  11357:7:0:[10802.0,10329.0,10608.1,11356.3]::  -> p(n2,n5,n6),p(n3,n5,n6),p(n5,n5,n6),p(n6,n5,n6),p(n7,n5,n6),p(n8,n5,n6),p(n9,n5,n6)
% 2.75/1.08  11355:5:0:[10801.0,10328.0,10577.1,11352.1,10843.1,11353.3,10648.0,11354.5]::  -> p(n3,n5,n5),p(n5,n5,n5),p(n7,n5,n5),p(n8,n5,n5),p(n9,n5,n5)
% 2.75/1.08  11351:3:0:[10557.1,10327.0,10906.1,11346.1,10908.1,11347.2,10842.1,11348.3,10633.1,11349.4,10680.0,11350.8]::  -> p(n6,n5,n4),p(n7,n5,n4),p(n8,n5,n4)
% 2.75/1.08  11345:3:0:[10800.0,10326.0,10592.1,11340.2,10841.1,11341.3,10640.0,11342.4,10932.1,11343.5,10664.0,11344.6]::  -> p(n2,n5,n3),p(n8,n5,n3),p(n9,n5,n3)
% 2.75/1.08  11339:5:0:[10799.0,10325.0,10583.1,11336.1,10913.1,11337.2,10840.1,11338.3]::  -> p(n5,n5,n2),p(n6,n5,n2),p(n7,n5,n2),p(n8,n5,n2),p(n9,n5,n2)
% 2.75/1.08  10618:1:0:[10539.0,1162.1]:: p(n4,n4,n1) -> 
% 2.75/1.08  11335:6:0:[10798.1,10323.0,10821.1,11333.1,10877.1,11334.6]::  -> p(n3,n4,n9),p(n4,n4,n9),p(n5,n4,n9),p(n6,n4,n9),p(n8,n4,n9),p(n9,n4,n9)
% 2.75/1.08  11332:5:0:[10797.1,10322.0,10820.1,11329.1,10599.0,11330.2,10876.1,11331.6]::  -> p(n4,n4,n8),p(n5,n4,n8),p(n6,n4,n8),p(n8,n4,n8),p(n9,n4,n8)
% 2.75/1.08  11328:5:0:[10796.1,10320.0,10819.1,11325.1,10606.1,11326.3,10875.0,11327.6]::  -> p(n3,n4,n6),p(n5,n4,n6),p(n6,n4,n6),p(n8,n4,n6),p(n9,n4,n6)
% 2.75/1.08  11324:5:0:[10795.1,10319.0,10576.1,11321.1,10647.0,11322.5,10874.0,11323.6]::  -> p(n3,n4,n5),p(n4,n4,n5),p(n5,n4,n5),p(n8,n4,n5),p(n9,n4,n5)
% 2.75/1.08  11320:2:0:[10794.0,10317.0,10818.1,11314.1,10591.1,11315.2,10927.0,11316.3,10639.0,11317.4,10931.1,11318.5,10661.0,11319.6]::  -> p(n8,n4,n3),p(n9,n4,n3)
% 2.75/1.08  10619:1:0:[10540.0,1186.1]:: p(n4,n4,n7) -> 
% 2.75/1.08  11313:2:0:[10560.0,10315.0,10817.0,11307.1,10618.0,11308.3,10928.1,11309.4,10929.1,11310.5,10873.0,11311.6,10670.1,11312.7]::  -> p(n3,n4,n1),p(n9,n4,n1)
% 2.75/1.08  11306:8:0:[10858.1,10314.4]::  -> p(n1,n3,n9),p(n2,n3,n9),p(n3,n3,n9),p(n4,n3,n9),p(n6,n3,n9),p(n7,n3,n9),p(n8,n3,n9),p(n9,n3,n9)
% 2.75/1.08  11305:7:0:[10598.0,10313.2,10857.1,11304.4]::  -> p(n1,n3,n8),p(n2,n3,n8),p(n4,n3,n8),p(n6,n3,n8),p(n7,n3,n8),p(n8,n3,n8),p(n9,n3,n8)
% 2.75/1.08  11303:5:0:[10555.0,10312.0,10617.0,11300.3,10856.1,11301.4,10656.0,11302.6]::  -> p(n2,n3,n7),p(n3,n3,n7),p(n6,n3,n7),p(n8,n3,n7),p(n9,n3,n7)
% 2.75/1.08  11299:6:0:[10605.1,10311.3,10855.1,11297.4,10923.1,11298.5]::  -> p(n1,n3,n6),p(n2,n3,n6),p(n3,n3,n6),p(n7,n3,n6),p(n8,n3,n6),p(n9,n3,n6)
% 2.75/1.08  11296:4:0:[10900.0,10310.0,10574.1,11292.1,10904.1,11293.2,10854.1,11294.4,10646.0,11295.5]::  -> p(n4,n3,n5),p(n7,n3,n5),p(n8,n3,n5),p(n9,n3,n5)
% 2.75/1.08  10620:1:0:[10539.0,1207.0]:: p(n4,n6,n1) -> 
% 2.75/1.08  11291:4:0:[10901.0,10308.0,10905.0,11287.1,10590.1,11288.2,10634.0,11289.4,10657.0,11290.6]::  -> p(n4,n3,n3),p(n6,n3,n3),p(n8,n3,n3),p(n9,n3,n3)
% 2.75/1.08  10621:1:0:[10539.0,1216.0]:: p(n4,n7,n1) -> 
% 2.75/1.08  11286:7:0:[10582.0,10307.1,10853.0,11285.4]::  -> p(n1,n3,n2),p(n3,n3,n2),p(n4,n3,n2),p(n6,n3,n2),p(n7,n3,n2),p(n8,n3,n2),p(n9,n3,n2)
% 2.75/1.08  10622:1:0:[10540.0,1222.1]:: p(n4,n5,n7) -> 
% 2.75/1.08  10623:1:0:[10539.0,1225.0]:: p(n4,n8,n1) -> 
% 2.75/1.08  11284:3:0:[10556.0,10306.0,10616.0,11279.3,10852.0,11280.4,10940.0,11281.6,10669.1,11282.7,10942.1,11283.8]::  -> p(n2,n3,n1),p(n3,n3,n1),p(n6,n3,n1)
% 2.75/1.08  11278:7:0:[10816.1,10305.1,10827.1,11277.2]::  -> p(n1,n2,n9),p(n4,n2,n9),p(n5,n2,n9),p(n6,n2,n9),p(n7,n2,n9),p(n8,n2,n9),p(n9,n2,n9)
% 2.75/1.08  10624:1:0:[10539.0,1234.0]:: p(n4,n9,n1) -> 
% 2.75/1.08  11276:7:0:[10815.1,10304.1,10597.0,11275.2]::  -> p(n1,n2,n8),p(n4,n2,n8),p(n5,n2,n8),p(n6,n2,n8),p(n7,n2,n8),p(n8,n2,n8),p(n9,n2,n8)
% 2.75/1.08  11274:4:0:[10552.0,10303.0,10814.1,11270.1,10826.1,11271.2,10615.0,11272.3,10654.0,11273.6]::  -> p(n5,n2,n7),p(n6,n2,n7),p(n8,n2,n7),p(n9,n2,n7)
% 2.75/1.08  11269:4:0:[10813.1,10302.1,10825.1,11265.2,10604.1,11266.3,10921.1,11267.4,10922.1,11268.5]::  -> p(n1,n2,n6),p(n7,n2,n6),p(n8,n2,n6),p(n9,n2,n6)
% 2.75/1.08  11264:2:0:[10551.0,10300.0,10812.0,11258.1,10824.1,11259.2,10924.0,11260.3,10630.0,11261.4,10926.1,11262.5,10677.0,11263.8]::  -> p(n7,n2,n4),p(n8,n2,n4)
% 2.75/1.08  10625:1:0:[10540.0,1249.1]:: p(n4,n6,n7) -> 
% 2.75/1.08  11257:7:0:[10575.0,10298.1,10823.0,11256.2]::  -> p(n1,n2,n2),p(n4,n2,n2),p(n5,n2,n2),p(n6,n2,n2),p(n7,n2,n2),p(n8,n2,n2),p(n9,n2,n2)
% 2.75/1.08  11255:2:0:[10553.0,10297.0,10811.0,11249.1,10822.0,11250.2,10614.0,11251.3,10939.0,11252.6,10668.1,11253.7,10941.1,11254.8]::  -> p(n5,n2,n1),p(n6,n2,n1)
% 2.75/1.08  11248:7:0:[10839.1,10296.3,10890.1,11247.7]::  -> p(n1,n1,n9),p(n2,n1,n9),p(n3,n1,n9),p(n5,n1,n9),p(n6,n1,n9),p(n7,n1,n9),p(n9,n1,n9)
% 2.75/1.08  11246:6:0:[10589.0,10295.2,10838.1,11244.3,10889.1,11245.7]::  -> p(n1,n1,n8),p(n2,n1,n8),p(n5,n1,n8),p(n6,n1,n8),p(n7,n1,n8),p(n9,n1,n8)
% 2.75/1.08  11243:5:0:[10549.0,10294.0,10611.0,11240.3,10652.0,11241.6,10888.1,11242.7]::  -> p(n2,n1,n7),p(n3,n1,n7),p(n5,n1,n7),p(n6,n1,n7),p(n9,n1,n7)
% 2.75/1.08  11239:3:0:[10898.0,10292.0,10572.0,11234.1,10903.1,11235.2,10837.0,11236.3,10644.0,11237.5,10887.1,11238.7]::  -> p(n5,n1,n5),p(n7,n1,n5),p(n9,n1,n5)
% 2.75/1.08  11233:3:0:[10548.0,10291.0,10836.0,11228.3,10628.0,11229.4,10925.1,11230.5,10886.1,11231.7,10676.0,11232.8]::  -> p(n2,n1,n4),p(n3,n1,n4),p(n7,n1,n4)
% 2.75/1.08  11227:2:0:[10899.0,10290.0,10902.0,11221.1,10588.0,11222.2,10835.0,11223.3,10629.0,11224.4,10653.0,11225.6,10885.1,11226.7]::  -> p(n6,n1,n3),p(n9,n1,n3)
% 2.75/1.08  10626:1:0:[10540.0,1276.0]:: p(n4,n8,n7) -> 
% 2.75/1.08  11220:6:0:[10573.0,10289.1,10834.0,11218.3,10884.1,11219.7]::  -> p(n1,n1,n2),p(n3,n1,n2),p(n5,n1,n2),p(n6,n1,n2),p(n7,n1,n2),p(n9,n1,n2)
% 2.75/1.08  11217:8:0:[10897.1,10287.8]::  -> p(n9,n1,n9),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)
% 2.75/1.08  10627:1:0:[10540.0,1285.0]:: p(n4,n9,n7) -> 
% 2.75/1.08  11216:8:0:[10789.1,10286.8]::  -> p(n9,n1,n8),p(n9,n2,n8),p(n9,n3,n8),p(n9,n4,n8),p(n9,n5,n8),p(n9,n6,n8),p(n9,n7,n8),p(n9,n8,n8)
% 2.75/1.08  11215:4:0:[10736.1,10285.3,10742.1,11211.4,10944.1,11212.5,10766.1,11213.6,10896.1,11214.8]::  -> p(n9,n1,n7),p(n9,n2,n7),p(n9,n3,n7),p(n9,n8,n7)
% 2.75/1.08  11210:7:0:[10693.1,10284.0,10895.1,11209.8]::  -> p(n9,n2,n6),p(n9,n3,n6),p(n9,n4,n6),p(n9,n5,n6),p(n9,n6,n6),p(n9,n7,n6),p(n9,n8,n6)
% 2.75/1.08  10628:1:0:[10541.0,1309.1]:: p(n5,n1,n4) -> 
% 2.75/1.08  11208:6:0:[10706.1,10283.1,10777.1,11206.7,10894.1,11207.8]::  -> p(n9,n1,n5),p(n9,n3,n5),p(n9,n4,n5),p(n9,n5,n5),p(n9,n6,n5),p(n9,n7,n5)
% 2.75/1.08  11205:4:0:[10710.1,10281.1,10754.1,11201.5,10948.1,11202.6,10779.1,11203.7,10893.0,11204.8]::  -> p(n9,n1,n3),p(n9,n3,n3),p(n9,n4,n3),p(n9,n5,n3)
% 2.75/1.08  10629:1:0:[10542.0,1335.1]:: p(n5,n1,n3) -> 
% 2.75/1.08  11200:7:0:[10731.1,10280.3,10892.0,11199.8]::  -> p(n9,n1,n2),p(n9,n2,n2),p(n9,n3,n2),p(n9,n5,n2),p(n9,n6,n2),p(n9,n7,n2),p(n9,n8,n2)
% 2.75/1.08  11198:3:0:[10697.1,10279.0,10941.1,11193.1,10942.1,11194.2,10748.1,11195.4,10760.1,11196.6,10891.0,11197.8]::  -> p(n9,n4,n1),p(n9,n6,n1),p(n9,n8,n1)
% 2.75/1.08  11192:8:0:[10890.1,10278.0]::  -> p(n8,n2,n9),p(n8,n3,n9),p(n8,n4,n9),p(n8,n5,n9),p(n8,n6,n9),p(n8,n7,n9),p(n8,n8,n9),p(n8,n9,n9)
% 2.75/1.08  11191:7:0:[10889.1,10277.0,10787.1,11190.8]::  -> p(n8,n2,n8),p(n8,n3,n8),p(n8,n4,n8),p(n8,n5,n8),p(n8,n6,n8),p(n8,n7,n8),p(n8,n8,n8)
% 2.75/1.08  11189:4:0:[10888.1,10276.0,10735.1,11185.3,10741.1,11186.4,10943.1,11187.5,10765.1,11188.6]::  -> p(n8,n2,n7),p(n8,n3,n7),p(n8,n8,n7),p(n8,n9,n7)
% 2.75/1.08  11184:8:0:[10692.1,10275.0]::  -> p(n8,n2,n6),p(n8,n3,n6),p(n8,n4,n6),p(n8,n5,n6),p(n8,n6,n6),p(n8,n7,n6),p(n8,n8,n6),p(n8,n9,n6)
% 2.75/1.08  11183:6:0:[10887.1,10274.0,10705.1,11181.1,10776.1,11182.7]::  -> p(n8,n3,n5),p(n8,n4,n5),p(n8,n5,n5),p(n8,n6,n5),p(n8,n7,n5),p(n8,n9,n5)
% 2.75/1.08  10630:1:0:[10541.0,1372.1]:: p(n5,n2,n4) -> 
% 2.75/1.08  11180:3:0:[10886.1,10273.0,10716.1,11175.2,10723.1,11176.3,10949.0,11177.6,10950.0,11178.7,10793.0,11179.8]::  -> p(n8,n2,n4),p(n8,n5,n4),p(n8,n6,n4)
% 2.75/1.08  11174:3:0:[10885.1,10272.0,10709.1,11169.1,10753.1,11170.5,10946.1,11171.6,10778.1,11172.7,10947.1,11173.8]::  -> p(n8,n3,n3),p(n8,n4,n3),p(n8,n5,n3)
% 2.75/1.08  10631:1:0:[10542.0,1398.1]:: p(n5,n2,n3) -> 
% 2.75/1.08  11168:7:0:[10884.1,10271.0,10730.1,11167.3]::  -> p(n8,n2,n2),p(n8,n3,n2),p(n8,n5,n2),p(n8,n6,n2),p(n8,n7,n2),p(n8,n8,n2),p(n8,n9,n2)
% 2.75/1.08  11166:7:0:[10877.1,10269.3,10883.1,11165.7]::  -> p(n7,n1,n9),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.75/1.08  11164:6:0:[10876.1,10268.3,10882.1,11162.7,10786.1,11163.8]::  -> p(n7,n1,n8),p(n7,n2,n8),p(n7,n3,n8),p(n7,n5,n8),p(n7,n6,n8),p(n7,n7,n8)
% 2.75/1.08  11161:6:0:[10691.1,10266.0,10875.0,11159.3,10881.1,11160.7]::  -> 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.75/1.08  11158:6:0:[10704.1,10265.1,10874.0,11156.3,10775.1,11157.7]::  -> p(n7,n1,n5),p(n7,n3,n5),p(n7,n5,n5),p(n7,n6,n5),p(n7,n7,n5),p(n7,n9,n5)
% 2.75/1.08  11155:4:0:[10715.1,10264.2,10722.1,11151.3,10945.0,11152.6,10880.1,11153.7,10792.0,11154.8]::  -> p(n7,n1,n4),p(n7,n2,n4),p(n7,n5,n4),p(n7,n6,n4)
% 2.75/1.08  11150:7:0:[10728.1,10262.3,10879.0,11149.7]::  -> p(n7,n1,n2),p(n7,n2,n2),p(n7,n3,n2),p(n7,n5,n2),p(n7,n6,n2),p(n7,n7,n2),p(n7,n9,n2)
% 2.75/1.08  10632:1:0:[10541.0,1435.0]:: p(n5,n4,n4) -> 
% 2.75/1.08  10633:1:0:[10541.0,1444.0]:: p(n5,n5,n4) -> 
% 2.75/1.08  10634:1:0:[10542.0,1452.1]:: p(n5,n3,n3) -> 
% 2.75/1.08  10635:1:0:[10541.0,1453.0]:: p(n5,n6,n4) -> 
% 2.75/1.08  11148:2:0:[10696.0,10261.0,10939.0,11142.1,10940.0,11143.2,10873.0,11144.3,10747.1,11145.4,10759.1,11146.6,10878.0,11147.7]::  -> p(n7,n6,n1),p(n7,n9,n1)
% 2.75/1.08  10636:1:0:[10541.0,1462.0]:: p(n5,n7,n4) -> 
% 2.75/1.08  11141:8:0:[10872.1,10260.7]::  -> p(n6,n1,n9),p(n6,n2,n9),p(n6,n3,n9),p(n6,n4,n9),p(n6,n5,n9),p(n6,n6,n9),p(n6,n7,n9),p(n6,n9,n9)
% 2.75/1.08  10637:1:0:[10541.0,1471.0]:: p(n5,n8,n4) -> 
% 2.75/1.08  11140:7:0:[10871.1,10259.7,10785.1,11139.8]::  -> p(n6,n1,n8),p(n6,n2,n8),p(n6,n3,n8),p(n6,n4,n8),p(n6,n5,n8),p(n6,n6,n8),p(n6,n7,n8)
% 2.75/1.08  10638:1:0:[10541.0,1480.0]:: p(n5,n9,n4) -> 
% 2.75/1.08  11138:4:0:[10734.0,10258.3,10740.1,11134.4,10764.1,11135.6,10870.1,11136.7,10935.1,11137.8]::  -> p(n6,n1,n7),p(n6,n2,n7),p(n6,n3,n7),p(n6,n6,n7)
% 2.75/1.08  10639:1:0:[10542.0,1497.1]:: p(n5,n4,n3) -> 
% 2.75/1.08  11133:5:0:[10690.1,10257.0,10922.1,11130.1,10923.1,11131.2,10869.1,11132.7]::  -> p(n6,n4,n6),p(n6,n5,n6),p(n6,n6,n6),p(n6,n7,n6),p(n6,n9,n6)
% 2.75/1.08  11129:3:0:[10925.1,10255.0,10926.1,11124.1,10714.1,11125.2,10721.1,11126.3,10868.0,11127.7,10791.0,11128.8]::  -> p(n6,n5,n4),p(n6,n6,n4),p(n6,n7,n4)
% 2.75/1.08  11123:4:0:[10708.1,10254.1,10931.1,11119.3,10932.1,11120.4,10752.1,11121.5,10774.0,11122.7]::  -> p(n6,n1,n3),p(n6,n3,n3),p(n6,n7,n3),p(n6,n9,n3)
% 2.75/1.08  11118:7:0:[10727.1,10253.3,10867.0,11117.7]::  -> p(n6,n1,n2),p(n6,n2,n2),p(n6,n3,n2),p(n6,n5,n2),p(n6,n6,n2),p(n6,n7,n2),p(n6,n9,n2)
% 2.75/1.08  11116:3:0:[10695.0,10252.0,10929.1,11111.3,10746.1,11112.4,10930.1,11113.5,10758.1,11114.6,10866.0,11115.7]::  -> p(n6,n2,n1),p(n6,n3,n1),p(n6,n9,n1)
% 2.75/1.08  11110:7:0:[10858.1,10251.2,10865.1,11109.5]::  -> p(n5,n1,n9),p(n5,n2,n9),p(n5,n4,n9),p(n5,n5,n9),p(n5,n7,n9),p(n5,n8,n9),p(n5,n9,n9)
% 2.75/1.08  11108:6:0:[10857.1,10250.2,10864.1,11106.5,10784.1,11107.8]::  -> p(n5,n1,n8),p(n5,n2,n8),p(n5,n4,n8),p(n5,n5,n8),p(n5,n7,n8),p(n5,n8,n8)
% 2.75/1.08  10640:1:0:[10542.0,1533.1]:: p(n5,n5,n3) -> 
% 2.75/1.08  11105:2:0:[10856.1,10249.2,10733.0,11099.3,10739.1,11100.4,10863.1,11101.5,10763.1,11102.6,10933.1,11103.7,10934.1,11104.8]::  -> p(n5,n1,n7),p(n5,n2,n7)
% 2.75/1.08  11098:5:0:[10689.1,10248.0,10921.1,11095.1,10855.1,11096.2,10862.1,11097.5]::  -> p(n5,n4,n6),p(n5,n5,n6),p(n5,n7,n6),p(n5,n8,n6),p(n5,n9,n6)
% 2.75/1.08  11094:3:0:[10703.1,10247.1,10854.1,11089.2,10861.1,11090.5,10937.0,11091.6,10773.0,11092.7,10938.0,11093.8]::  -> p(n5,n1,n5),p(n5,n4,n5),p(n5,n5,n5)
% 2.75/1.08  11088:6:0:[10853.0,10244.2,10726.1,11086.3,10860.0,11087.5]::  -> p(n5,n1,n2),p(n5,n2,n2),p(n5,n5,n2),p(n5,n7,n2),p(n5,n8,n2),p(n5,n9,n2)
% 2.75/1.08  11085:3:0:[10694.0,10243.0,10852.0,11080.2,10928.1,11081.3,10745.1,11082.4,10859.0,11083.5,10757.1,11084.6]::  -> p(n5,n2,n1),p(n5,n8,n1),p(n5,n9,n1)
% 2.75/1.08  11079:6:0:[10839.1,10242.0,10845.1,11077.4,10851.1,11078.6]::  -> p(n4,n2,n9),p(n4,n3,n9),p(n4,n4,n9),p(n4,n6,n9),p(n4,n8,n9),p(n4,n9,n9)
% 2.75/1.08  11076:5:0:[10838.1,10241.0,10844.1,11073.4,10850.1,11074.6,10783.1,11075.8]::  -> p(n4,n2,n8),p(n4,n3,n8),p(n4,n4,n8),p(n4,n6,n8),p(n4,n8,n8)
% 2.75/1.08  10641:1:0:[10542.0,1569.0]:: p(n5,n7,n3) -> 
% 2.75/1.08  11072:3:0:[10837.0,10238.0,10702.1,11067.1,10843.1,11068.4,10849.0,11069.6,10771.0,11070.7,10936.0,11071.8]::  -> p(n4,n3,n5),p(n4,n4,n5),p(n4,n6,n5)
% 2.75/1.08  10642:1:0:[10542.0,1578.0]:: p(n5,n8,n3) -> 
% 2.75/1.08  11066:2:0:[10836.0,10237.0,10924.0,11060.1,10713.0,11061.2,10720.1,11062.3,10842.1,11063.4,10848.0,11064.6,10790.0,11065.8]::  -> p(n4,n6,n4),p(n4,n8,n4)
% 2.75/1.08  10643:1:0:[10542.0,1587.0]:: p(n5,n9,n3) -> 
% 2.75/1.08  11059:2:0:[10835.0,10236.0,10707.1,11053.1,10927.0,11054.3,10841.1,11055.4,10751.0,11056.5,10847.0,11057.6,10772.0,11058.7]::  -> p(n4,n3,n3),p(n4,n9,n3)
% 2.75/1.08  11052:5:0:[10834.0,10235.0,10725.1,11049.3,10840.1,11050.4,10846.0,11051.6]::  -> p(n4,n2,n2),p(n4,n3,n2),p(n4,n6,n2),p(n4,n8,n2),p(n4,n9,n2)
% 2.75/1.08  11048:7:0:[10827.1,10233.1,10833.1,11047.8]::  -> p(n3,n1,n9),p(n3,n3,n9),p(n3,n4,n9),p(n3,n5,n9),p(n3,n6,n9),p(n3,n7,n9),p(n3,n8,n9)
% 2.75/1.08  11046:3:0:[10826.1,10231.1,10732.0,11041.3,10738.1,11042.4,10911.1,11043.5,10762.0,11044.6,10832.0,11045.8]::  -> p(n3,n1,n7),p(n3,n3,n7),p(n3,n8,n7)
% 2.75/1.08  11040:6:0:[10687.0,10230.0,10825.1,11038.1,10831.0,11039.8]::  -> p(n3,n3,n6),p(n3,n4,n6),p(n3,n5,n6),p(n3,n6,n6),p(n3,n7,n6),p(n3,n8,n6)
% 2.75/1.08  11037:4:0:[10903.1,10229.0,10701.1,11033.1,10904.1,11034.2,10770.0,11035.7,10830.0,11036.8]::  -> p(n3,n4,n5),p(n3,n5,n5),p(n3,n6,n5),p(n3,n7,n5)
% 2.75/1.08  11032:3:0:[10824.1,10228.1,10712.0,11027.2,10719.1,11028.3,10908.1,11029.4,10909.1,11030.5,10788.0,11031.8]::  -> p(n3,n1,n4),p(n3,n7,n4),p(n3,n8,n4)
% 2.75/1.08  10644:1:0:[10543.0,1679.1]:: p(n6,n1,n5) -> 
% 2.75/1.08  11026:4:0:[10823.0,10226.1,10724.1,11022.3,10913.1,11023.4,10914.1,11024.5,10829.0,11025.8]::  -> p(n3,n1,n2),p(n3,n3,n2),p(n3,n7,n2),p(n3,n8,n2)
% 2.75/1.08  10645:1:0:[10543.0,1742.1]:: p(n6,n2,n5) -> 
% 2.75/1.08  11021:3:0:[10688.0,10225.0,10822.0,11016.1,10744.0,11017.4,10756.1,11018.6,10917.1,11019.7,10828.0,11020.8]::  -> p(n3,n3,n1),p(n3,n4,n1),p(n3,n6,n1)
% 2.75/1.08  10646:1:0:[10543.0,1796.1]:: p(n6,n3,n5) -> 
% 2.75/1.08  11015:7:0:[10816.1,10224.1,10821.1,11014.3]::  -> p(n2,n1,n9),p(n2,n3,n9),p(n2,n5,n9),p(n2,n6,n9),p(n2,n7,n9),p(n2,n8,n9),p(n2,n9,n9)
% 2.75/1.08  10647:1:0:[10543.0,1841.1]:: p(n6,n4,n5) -> 
% 2.75/1.08  11013:4:0:[10815.1,10223.1,10820.1,11009.3,10919.0,11010.6,10920.0,11011.7,10781.0,11012.8]::  -> p(n2,n1,n8),p(n2,n3,n8),p(n2,n5,n8),p(n2,n6,n8)
% 2.75/1.08  10648:1:0:[10543.0,1877.1]:: p(n6,n5,n5) -> 
% 2.75/1.08  11008:4:0:[10814.1,10222.1,10729.0,11004.3,10737.1,11005.4,10910.1,11006.5,10761.0,11007.6]::  -> p(n2,n1,n7),p(n2,n3,n7),p(n2,n8,n7),p(n2,n9,n7)
% 2.75/1.08  10649:1:0:[10543.0,1904.1]:: p(n6,n6,n5) -> 
% 2.75/1.08  11003:6:0:[10685.0,10221.0,10813.1,11001.1,10819.1,11002.3]::  -> p(n2,n3,n6),p(n2,n5,n6),p(n2,n6,n6),p(n2,n7,n6),p(n2,n8,n6),p(n2,n9,n6)
% 2.75/1.08  10650:1:0:[10543.0,1922.1]:: p(n6,n7,n5) -> 
% 2.75/1.08  11000:3:0:[10812.0,10219.1,10711.0,10995.2,10718.1,10996.3,10906.1,10997.4,10907.1,10998.5,10782.0,10999.8]::  -> p(n2,n1,n4),p(n2,n7,n4),p(n2,n8,n4)
% 2.75/1.08  10651:1:0:[10543.0,1940.0]:: p(n6,n9,n5) -> 
% 2.75/1.08  10652:1:0:[10544.0,1969.1]:: p(n7,n1,n7) -> 
% 2.75/1.08  10994:3:0:[10902.0,10218.0,10700.0,10989.1,10905.0,10990.2,10818.1,10991.3,10750.0,10992.5,10769.0,10993.7]::  -> p(n2,n5,n3),p(n2,n7,n3),p(n2,n9,n3)
% 2.75/1.08  10988:2:0:[10686.0,10216.0,10811.0,10982.1,10817.0,10983.3,10743.0,10984.4,10755.1,10985.6,10915.1,10986.7,10916.1,10987.8]::  -> p(n2,n3,n1),p(n2,n6,n1)
% 2.75/1.08  10981:6:0:[10798.1,10215.3,10804.1,10979.4,10810.1,10980.6]::  -> p(n1,n1,n9),p(n1,n2,n9),p(n1,n3,n9),p(n1,n6,n9),p(n1,n8,n9),p(n1,n9,n9)
% 2.75/1.08  10653:1:0:[10545.0,2001.1]:: p(n7,n1,n3) -> 
% 2.75/1.08  10978:4:0:[10797.1,10214.3,10803.1,10974.4,10809.1,10975.6,10918.0,10976.7,10780.0,10977.8]::  -> p(n1,n1,n8),p(n1,n2,n8),p(n1,n3,n8),p(n1,n6,n8)
% 2.75/1.08  10973:5:0:[10684.0,10212.0,10796.1,10970.3,10802.0,10971.4,10808.1,10972.6]::  -> p(n1,n2,n6),p(n1,n3,n6),p(n1,n6,n6),p(n1,n8,n6),p(n1,n9,n6)
% 2.75/1.08  10969:2:0:[10898.0,10211.0,10698.0,10963.1,10900.0,10964.2,10795.1,10965.3,10801.0,10966.4,10807.1,10967.6,10767.0,10968.7]::  -> p(n1,n6,n5),p(n1,n9,n5)
% 2.75/1.08  10654:1:0:[10544.0,2032.1]:: p(n7,n2,n7) -> 
% 2.75/1.08  10962:1:0:[10899.0,10209.0,10699.0,10955.1,10901.0,10956.2,10794.0,10957.3,10800.0,10958.4,10749.0,10959.5,10806.1,10960.6,10768.0,10961.7]::  -> p(n1,n9,n3)
% 2.75/1.08  10954:5:0:[10717.0,10208.3,10799.0,10951.4,10912.0,10952.5,10805.1,10953.6]::  -> p(n1,n1,n2),p(n1,n2,n2),p(n1,n3,n2),p(n1,n8,n2),p(n1,n9,n2)
% 2.75/1.08  10655:1:0:[10545.0,2064.1]:: p(n7,n2,n3) -> 
% 2.75/1.08  10656:1:0:[10544.0,2086.1]:: p(n7,n3,n7) -> 
% 2.75/1.08  10657:1:0:[10545.0,2118.1]:: p(n7,n3,n3) -> 
% 2.75/1.08  10950:1:0:[10547.0,10183.1]:: p(n8,n8,n4) -> 
% 2.75/1.08  10658:1:0:[10544.0,2140.0]:: p(n7,n5,n7) -> 
% 2.75/1.08  10659:1:0:[10544.0,2149.0]:: p(n7,n6,n7) -> 
% 2.75/1.08  10660:1:0:[10544.0,2158.0]:: p(n7,n7,n7) -> 
% 2.75/1.08  10661:1:0:[10545.0,2163.1]:: p(n7,n4,n3) -> 
% 2.75/1.08  10662:1:0:[10544.0,2167.0]:: p(n7,n8,n7) -> 
% 2.75/1.08  10663:1:0:[10544.0,2176.0]:: p(n7,n9,n7) -> 
% 2.75/1.08  10664:1:0:[10545.0,2199.1]:: p(n7,n5,n3) -> 
% 2.75/1.08  10949:1:0:[10547.0,10165.1]:: p(n8,n7,n4) -> 
% 2.75/1.08  10665:1:0:[10545.0,2226.1]:: p(n7,n6,n3) -> 
% 2.75/1.08  10666:1:0:[10545.0,2244.1]:: p(n7,n7,n3) -> 
% 2.75/1.08  10667:1:0:[10545.0,2262.0]:: p(n7,n9,n3) -> 
% 2.75/1.08  10668:1:0:[10546.0,2269.0]:: p(n8,n2,n1) -> 
% 2.75/1.08  10669:1:0:[10546.0,2278.0]:: p(n8,n3,n1) -> 
% 2.75/1.08  10670:1:0:[10546.0,2287.0]:: p(n8,n4,n1) -> 
% 2.75/1.08  10671:1:0:[10546.0,2296.0]:: p(n8,n5,n1) -> 
% 2.75/1.08  10672:1:0:[10546.0,2305.0]:: p(n8,n6,n1) -> 
% 2.75/1.08  10673:1:0:[10546.0,2314.0]:: p(n8,n7,n1) -> 
% 2.75/1.08  10674:1:0:[10546.0,2323.0]:: p(n8,n8,n1) -> 
% 2.75/1.08  10675:1:0:[10546.0,2332.0]:: p(n8,n9,n1) -> 
% 2.75/1.08  10948:1:0:[10545.0,10101.0]:: p(n9,n7,n3) -> 
% 2.75/1.08  10947:1:0:[10545.0,10092.0]:: p(n8,n9,n3) -> 
% 2.75/1.08  10946:1:0:[10545.0,10083.0]:: p(n8,n7,n3) -> 
% 2.75/1.08  10945:1:0:[10547.0,10075.1]:: p(n7,n7,n4) -> 
% 2.75/1.08  10676:1:0:[10547.0,2659.1]:: p(n9,n1,n4) -> 
% 2.75/1.08  10677:1:0:[10547.0,2722.1]:: p(n9,n2,n4) -> 
% 2.75/1.08  10678:1:0:[10547.0,2776.1]:: p(n9,n3,n4) -> 
% 2.75/1.08  10679:1:0:[10547.0,2821.1]:: p(n9,n4,n4) -> 
% 2.75/1.08  10680:1:0:[10547.0,2857.1]:: p(n9,n5,n4) -> 
% 2.75/1.08  10681:1:0:[10547.0,2884.1]:: p(n9,n6,n4) -> 
% 2.75/1.08  10682:1:0:[10547.0,2902.1]:: p(n9,n7,n4) -> 
% 2.75/1.08  10683:1:0:[10547.0,2911.1]:: p(n9,n8,n4) -> 
% 2.75/1.08  10684:1:0:[10538.0,2940.1]:: p(n1,n1,n6) -> 
% 2.75/1.08  10685:1:0:[10538.0,3003.1]:: p(n2,n1,n6) -> 
% 2.75/1.08  10686:1:0:[10546.0,3034.1]:: p(n2,n1,n1) -> 
% 2.75/1.08  10944:1:0:[10544.0,9916.0]:: p(n9,n6,n7) -> 
% 2.75/1.08  10943:1:0:[10544.0,9898.0]:: p(n8,n6,n7) -> 
% 2.75/1.08  10687:1:0:[10538.0,3057.1]:: p(n3,n1,n6) -> 
% 2.75/1.08  10688:1:0:[10546.0,3088.1]:: p(n3,n1,n1) -> 
% 2.75/1.08  10942:1:0:[10546.0,9838.0]:: p(n9,n3,n1) -> 
% 2.75/1.08  10941:1:0:[10546.0,9829.0]:: p(n9,n2,n1) -> 
% 2.75/1.08  10689:1:0:[10538.0,3111.0]:: p(n5,n1,n6) -> 
% 2.75/1.08  10690:1:0:[10538.0,3120.0]:: p(n6,n1,n6) -> 
% 2.75/1.08  10691:1:0:[10538.0,3129.0]:: p(n7,n1,n6) -> 
% 2.75/1.08  10692:1:0:[10538.0,3138.0]:: p(n8,n1,n6) -> 
% 2.75/1.08  10940:1:0:[10546.0,9793.1]:: p(n7,n3,n1) -> 
% 2.75/1.08  10693:1:0:[10538.0,3147.0]:: p(n9,n1,n6) -> 
% 2.75/1.08  10694:1:0:[10546.0,3169.1]:: p(n5,n1,n1) -> 
% 2.75/1.08  10939:1:0:[10546.0,9757.1]:: p(n7,n2,n1) -> 
% 2.75/1.08  10695:1:0:[10546.0,3196.1]:: p(n6,n1,n1) -> 
% 2.75/1.08  10696:1:0:[10546.0,3214.1]:: p(n7,n1,n1) -> 
% 2.75/1.08  10938:1:0:[10543.0,9716.1]:: p(n5,n9,n5) -> 
% 2.75/1.08  10697:1:0:[10546.0,3232.0]:: p(n9,n1,n1) -> 
% 2.75/1.08  10698:1:0:[10534.0,3245.1]:: p(n1,n2,n5) -> 
% 2.75/1.08  10699:1:0:[10536.0,3252.1]:: p(n1,n2,n3) -> 
% 2.75/1.08  10937:1:0:[10543.0,9671.1]:: p(n5,n7,n5) -> 
% 2.75/1.08  10936:1:0:[10543.0,9662.1]:: p(n4,n9,n5) -> 
% 2.75/1.08  10935:1:0:[10540.0,9592.0]:: p(n6,n9,n7) -> 
% 2.75/1.08  10934:1:0:[10540.0,9574.0]:: p(n5,n9,n7) -> 
% 2.75/1.08  10933:1:0:[10540.0,9565.0]:: p(n5,n8,n7) -> 
% 2.75/1.08  10932:1:0:[10542.0,9552.0]:: p(n6,n5,n3) -> 
% 2.75/1.08  10931:1:0:[10542.0,9543.0]:: p(n6,n4,n3) -> 
% 2.75/1.08  10700:1:0:[10536.0,3315.1]:: p(n2,n2,n3) -> 
% 2.75/1.08  10701:1:0:[10534.0,3317.0]:: p(n3,n2,n5) -> 
% 2.75/1.08  10702:1:0:[10534.0,3326.0]:: p(n4,n2,n5) -> 
% 2.75/1.08  10703:1:0:[10534.0,3335.0]:: p(n5,n2,n5) -> 
% 2.75/1.08  10704:1:0:[10534.0,3353.0]:: p(n7,n2,n5) -> 
% 2.75/1.08  10930:1:0:[10539.0,9460.0]:: p(n6,n6,n1) -> 
% 2.75/1.08  10929:1:0:[10539.0,9451.0]:: p(n6,n4,n1) -> 
% 2.75/1.08  10705:1:0:[10534.0,3362.0]:: p(n8,n2,n5) -> 
% 2.75/1.08  10928:1:0:[10539.0,9433.0]:: p(n5,n4,n1) -> 
% 2.75/1.08  10706:1:0:[10534.0,3371.0]:: p(n9,n2,n5) -> 
% 2.75/1.08  10707:1:0:[10536.0,3378.0]:: p(n4,n2,n3) -> 
% 2.75/1.08  10927:1:0:[10542.0,9408.1]:: p(n4,n4,n3) -> 
% 2.75/1.08  10926:1:0:[10541.0,9391.0]:: p(n6,n2,n4) -> 
% 2.75/1.08  10925:1:0:[10541.0,9382.0]:: p(n6,n1,n4) -> 
% 2.75/1.08  10708:1:0:[10536.0,3396.0]:: p(n6,n2,n3) -> 
% 2.75/1.08  10709:1:0:[10536.0,3414.0]:: p(n8,n2,n3) -> 
% 2.75/1.08  10710:1:0:[10536.0,3423.0]:: p(n9,n2,n3) -> 
% 2.75/1.08  10924:1:0:[10541.0,9283.1]:: p(n4,n2,n4) -> 
% 2.75/1.08  10923:1:0:[10538.0,9267.0]:: p(n6,n3,n6) -> 
% 2.75/1.08  10922:1:0:[10538.0,9258.0]:: p(n6,n2,n6) -> 
% 2.75/1.08  10921:1:0:[10538.0,9240.0]:: p(n5,n2,n6) -> 
% 2.75/1.08  10920:1:0:[10537.0,9215.1]:: p(n2,n8,n8) -> 
% 2.75/1.08  10919:1:0:[10537.0,9197.1]:: p(n2,n7,n8) -> 
% 2.75/1.08  10918:1:0:[10537.0,9143.1]:: p(n1,n8,n8) -> 
% 2.75/1.08  10917:1:0:[10533.0,9091.0]:: p(n3,n8,n1) -> 
% 2.75/1.08  10916:1:0:[10533.0,9082.0]:: p(n2,n9,n1) -> 
% 2.75/1.08  10915:1:0:[10533.0,9073.0]:: p(n2,n8,n1) -> 
% 2.75/1.08  10914:1:0:[10535.0,9029.0]:: p(n3,n6,n2) -> 
% 2.75/1.08  10913:1:0:[10535.0,9020.0]:: p(n3,n5,n2) -> 
% 2.75/1.08  10912:1:0:[10535.0,8984.1]:: p(n1,n6,n2) -> 
% 2.75/1.08  10911:1:0:[10532.0,8980.0]:: p(n3,n6,n7) -> 
% 2.75/1.08  10910:1:0:[10532.0,8962.0]:: p(n2,n6,n7) -> 
% 2.75/1.08  10909:1:0:[10531.0,8941.0]:: p(n3,n6,n4) -> 
% 2.75/1.08  10908:1:0:[10531.0,8932.0]:: p(n3,n5,n4) -> 
% 2.75/1.08  10907:1:0:[10531.0,8923.0]:: p(n2,n6,n4) -> 
% 2.75/1.08  10906:1:0:[10531.0,8914.0]:: p(n2,n5,n4) -> 
% 2.75/1.08  10905:1:0:[10536.0,8904.1]:: p(n2,n3,n3) -> 
% 2.75/1.08  10904:1:0:[10534.0,8888.0]:: p(n3,n3,n5) -> 
% 2.75/1.08  10903:1:0:[10534.0,8879.0]:: p(n3,n1,n5) -> 
% 2.75/1.08  10902:1:0:[10536.0,8859.1]:: p(n2,n1,n3) -> 
% 2.75/1.08  10901:1:0:[10536.0,8850.1]:: p(n1,n3,n3) -> 
% 2.75/1.08  10711:1:0:[10541.0,3658.1]:: p(n2,n3,n4) -> 
% 2.75/1.08  10900:1:0:[10534.0,8834.1]:: p(n1,n3,n5) -> 
% 2.75/1.08  10899:1:0:[10536.0,8769.1]:: p(n1,n1,n3) -> 
% 2.75/1.08  10898:1:0:[10534.0,8753.1]:: p(n1,n1,n5) -> 
% 2.75/1.08  10712:1:0:[10541.0,3712.1]:: p(n3,n3,n4) -> 
% 2.75/1.08  10897:1:0:[10547.0,8738.0]:: p(n9,n9,n9) -> 
% 2.75/1.08  10896:1:0:[10547.0,8736.0]:: p(n9,n9,n7) -> 
% 2.75/1.08  10895:1:0:[10547.0,8735.0]:: p(n9,n9,n6) -> 
% 2.75/1.08  10894:1:0:[10547.0,8734.0]:: p(n9,n9,n5) -> 
% 2.75/1.08  10893:1:0:[10547.0,8728.1]:: p(n9,n9,n3) -> 
% 2.75/1.08  10892:1:0:[10547.0,8722.1]:: p(n9,n9,n2) -> 
% 2.75/1.08  10891:1:0:[10547.0,8715.1]:: p(n9,n9,n1) -> 
% 2.75/1.08  10713:1:0:[10541.0,3757.1]:: p(n4,n3,n4) -> 
% 2.75/1.08  10714:1:0:[10541.0,3802.0]:: p(n6,n3,n4) -> 
% 2.75/1.08  10715:1:0:[10541.0,3811.0]:: p(n7,n3,n4) -> 
% 2.75/1.08  10716:1:0:[10541.0,3820.0]:: p(n8,n3,n4) -> 
% 2.75/1.08  10717:1:0:[10535.0,3890.1]:: p(n1,n4,n2) -> 
% 2.75/1.08  10718:1:0:[10531.0,3892.0]:: p(n2,n4,n4) -> 
% 2.75/1.08  10719:1:0:[10531.0,3901.0]:: p(n3,n4,n4) -> 
% 2.75/1.08  10720:1:0:[10531.0,3910.0]:: p(n4,n4,n4) -> 
% 2.75/1.08  10721:1:0:[10531.0,3928.0]:: p(n6,n4,n4) -> 
% 2.75/1.08  10722:1:0:[10531.0,3937.0]:: p(n7,n4,n4) -> 
% 2.75/1.08  10723:1:0:[10531.0,3946.0]:: p(n8,n4,n4) -> 
% 2.75/1.08  10724:1:0:[10535.0,3962.0]:: p(n3,n4,n2) -> 
% 2.75/1.08  10725:1:0:[10535.0,3971.0]:: p(n4,n4,n2) -> 
% 2.75/1.08  10726:1:0:[10535.0,3980.0]:: p(n5,n4,n2) -> 
% 2.75/1.08  10727:1:0:[10535.0,3989.0]:: p(n6,n4,n2) -> 
% 2.75/1.08  10728:1:0:[10535.0,3998.0]:: p(n7,n4,n2) -> 
% 2.75/1.08  10729:1:0:[10544.0,4003.1]:: p(n2,n4,n7) -> 
% 2.75/1.08  10730:1:0:[10535.0,4007.0]:: p(n8,n4,n2) -> 
% 2.75/1.08  10731:1:0:[10535.0,4016.0]:: p(n9,n4,n2) -> 
% 2.75/1.08  10732:1:0:[10544.0,4057.1]:: p(n3,n4,n7) -> 
% 2.75/1.08  10733:1:0:[10544.0,4138.1]:: p(n5,n4,n7) -> 
% 2.75/1.08  10734:1:0:[10544.0,4165.1]:: p(n6,n4,n7) -> 
% 2.75/1.08  10735:1:0:[10544.0,4192.0]:: p(n8,n4,n7) -> 
% 2.75/1.08  10736:1:0:[10544.0,4201.0]:: p(n9,n4,n7) -> 
% 2.75/1.08  10737:1:0:[10532.0,4219.0]:: p(n2,n5,n7) -> 
% 2.75/1.08  10738:1:0:[10532.0,4228.0]:: p(n3,n5,n7) -> 
% 2.75/1.08  10739:1:0:[10532.0,4246.0]:: p(n5,n5,n7) -> 
% 2.75/1.08  10740:1:0:[10532.0,4255.0]:: p(n6,n5,n7) -> 
% 2.75/1.08  10741:1:0:[10532.0,4273.0]:: p(n8,n5,n7) -> 
% 2.75/1.08  10742:1:0:[10532.0,4282.0]:: p(n9,n5,n7) -> 
% 2.75/1.08  10743:1:0:[10539.0,4294.1]:: p(n2,n5,n1) -> 
% 2.75/1.08  10744:1:0:[10539.0,4348.1]:: p(n3,n5,n1) -> 
% 2.75/1.08  10890:1:0:[10546.0,8108.0]:: p(n8,n1,n9) -> 
% 2.75/1.08  10889:1:0:[10546.0,8107.0]:: p(n8,n1,n8) -> 
% 2.75/1.08  10888:1:0:[10546.0,8106.0]:: p(n8,n1,n7) -> 
% 2.75/1.08  10887:1:0:[10546.0,8104.0]:: p(n8,n1,n5) -> 
% 2.75/1.08  10886:1:0:[10546.0,8103.0]:: p(n8,n1,n4) -> 
% 2.75/1.08  10885:1:0:[10546.0,8102.0]:: p(n8,n1,n3) -> 
% 2.75/1.08  10884:1:0:[10546.0,8101.0]:: p(n8,n1,n2) -> 
% 2.75/1.08  10745:1:0:[10539.0,4402.0]:: p(n5,n5,n1) -> 
% 2.75/1.08  10883:1:0:[10545.0,8049.0]:: p(n7,n8,n9) -> 
% 2.75/1.08  10882:1:0:[10545.0,8048.0]:: p(n7,n8,n8) -> 
% 2.75/1.08  10881:1:0:[10545.0,8046.0]:: p(n7,n8,n6) -> 
% 2.75/1.08  10880:1:0:[10545.0,8044.0]:: p(n7,n8,n4) -> 
% 2.75/1.08  10746:1:0:[10539.0,4411.0]:: p(n6,n5,n1) -> 
% 2.75/1.08  10879:1:0:[10545.0,8037.1]:: p(n7,n8,n2) -> 
% 2.75/1.08  10878:1:0:[10545.0,8030.1]:: p(n7,n8,n1) -> 
% 2.75/1.08  10747:1:0:[10539.0,4420.0]:: p(n7,n5,n1) -> 
% 2.75/1.08  10748:1:0:[10539.0,4438.0]:: p(n9,n5,n1) -> 
% 2.75/1.08  10877:1:0:[10544.0,7919.0]:: p(n7,n4,n9) -> 
% 2.75/1.08  10876:1:0:[10544.0,7918.0]:: p(n7,n4,n8) -> 
% 2.75/1.08  10875:1:0:[10544.0,7915.1]:: p(n7,n4,n6) -> 
% 2.75/1.08  10874:1:0:[10544.0,7912.1]:: p(n7,n4,n5) -> 
% 2.75/1.08  10873:1:0:[10544.0,7890.1]:: p(n7,n4,n1) -> 
% 2.75/1.08  10749:1:0:[10542.0,4566.1]:: p(n1,n6,n3) -> 
% 2.75/1.08  10750:1:0:[10542.0,4629.1]:: p(n2,n6,n3) -> 
% 2.75/1.08  10872:1:0:[10543.0,7734.0]:: p(n6,n8,n9) -> 
% 2.75/1.08  10871:1:0:[10543.0,7733.0]:: p(n6,n8,n8) -> 
% 2.75/1.08  10870:1:0:[10543.0,7732.0]:: p(n6,n8,n7) -> 
% 2.75/1.08  10869:1:0:[10543.0,7731.0]:: p(n6,n8,n6) -> 
% 2.75/1.08  10868:1:0:[10543.0,7726.1]:: p(n6,n8,n4) -> 
% 2.75/1.08  10867:1:0:[10543.0,7715.1]:: p(n6,n8,n2) -> 
% 2.75/1.08  10866:1:0:[10543.0,7708.1]:: p(n6,n8,n1) -> 
% 2.75/1.08  10751:1:0:[10542.0,4728.1]:: p(n4,n6,n3) -> 
% 2.75/1.08  10752:1:0:[10542.0,4773.0]:: p(n6,n6,n3) -> 
% 2.75/1.08  10753:1:0:[10542.0,4791.0]:: p(n8,n6,n3) -> 
% 2.75/1.08  10754:1:0:[10542.0,4800.0]:: p(n9,n6,n3) -> 
% 2.75/1.09  10755:1:0:[10533.0,4861.0]:: p(n2,n7,n1) -> 
% 2.75/1.09  10756:1:0:[10533.0,4870.0]:: p(n3,n7,n1) -> 
% 2.75/1.09  10757:1:0:[10533.0,4888.0]:: p(n5,n7,n1) -> 
% 2.75/1.09  10758:1:0:[10533.0,4897.0]:: p(n6,n7,n1) -> 
% 2.75/1.09  10759:1:0:[10533.0,4906.0]:: p(n7,n7,n1) -> 
% 2.75/1.09  10760:1:0:[10533.0,4924.0]:: p(n9,n7,n1) -> 
% 2.75/1.09  10761:1:0:[10540.0,4948.1]:: p(n2,n7,n7) -> 
% 2.75/1.09  10762:1:0:[10540.0,5002.1]:: p(n3,n7,n7) -> 
% 2.75/1.09  10763:1:0:[10540.0,5056.0]:: p(n5,n7,n7) -> 
% 2.75/1.09  10764:1:0:[10540.0,5065.0]:: p(n6,n7,n7) -> 
% 2.75/1.09  10765:1:0:[10540.0,5083.0]:: p(n8,n7,n7) -> 
% 2.75/1.09  10766:1:0:[10540.0,5092.0]:: p(n9,n7,n7) -> 
% 2.75/1.09  10865:1:0:[10542.0,7329.0]:: p(n5,n6,n9) -> 
% 2.75/1.09  10864:1:0:[10542.0,7328.0]:: p(n5,n6,n8) -> 
% 2.75/1.09  10863:1:0:[10542.0,7327.0]:: p(n5,n6,n7) -> 
% 2.75/1.09  10862:1:0:[10542.0,7326.0]:: p(n5,n6,n6) -> 
% 2.75/1.09  10861:1:0:[10542.0,7325.0]:: p(n5,n6,n5) -> 
% 2.75/1.09  10860:1:0:[10542.0,7317.1]:: p(n5,n6,n2) -> 
% 2.75/1.09  10859:1:0:[10542.0,7310.1]:: p(n5,n6,n1) -> 
% 2.75/1.09  10858:1:0:[10541.0,7226.0]:: p(n5,n3,n9) -> 
% 2.75/1.09  10857:1:0:[10541.0,7225.0]:: p(n5,n3,n8) -> 
% 2.75/1.09  10856:1:0:[10541.0,7224.0]:: p(n5,n3,n7) -> 
% 2.75/1.09  10855:1:0:[10541.0,7223.0]:: p(n5,n3,n6) -> 
% 2.75/1.09  10854:1:0:[10541.0,7222.0]:: p(n5,n3,n5) -> 
% 2.75/1.09  10853:1:0:[10541.0,7210.1]:: p(n5,n3,n2) -> 
% 2.75/1.09  10852:1:0:[10541.0,7203.1]:: p(n5,n3,n1) -> 
% 2.75/1.09  10767:1:0:[10543.0,5225.1]:: p(n1,n8,n5) -> 
% 2.75/1.09  10768:1:0:[10545.0,5232.1]:: p(n1,n8,n3) -> 
% 2.75/1.09  10851:1:0:[10540.0,7055.0]:: p(n4,n7,n9) -> 
% 2.75/1.09  10850:1:0:[10540.0,7054.0]:: p(n4,n7,n8) -> 
% 2.75/1.09  10849:1:0:[10540.0,7048.1]:: p(n4,n7,n5) -> 
% 2.75/1.09  10848:1:0:[10540.0,7044.1]:: p(n4,n7,n4) -> 
% 2.75/1.09  10847:1:0:[10540.0,7039.1]:: p(n4,n7,n3) -> 
% 2.75/1.09  10846:1:0:[10540.0,7033.1]:: p(n4,n7,n2) -> 
% 2.75/1.09  10769:1:0:[10545.0,5295.1]:: p(n2,n8,n3) -> 
% 2.75/1.09  10845:1:0:[10539.0,6956.0]:: p(n4,n5,n9) -> 
% 2.75/1.09  10844:1:0:[10539.0,6955.0]:: p(n4,n5,n8) -> 
% 2.75/1.09  10843:1:0:[10539.0,6952.0]:: p(n4,n5,n5) -> 
% 2.75/1.09  10842:1:0:[10539.0,6951.0]:: p(n4,n5,n4) -> 
% 2.75/1.09  10841:1:0:[10539.0,6950.0]:: p(n4,n5,n3) -> 
% 2.75/1.09  10840:1:0:[10539.0,6949.0]:: p(n4,n5,n2) -> 
% 2.75/1.09  10770:1:0:[10543.0,5342.1]:: p(n3,n8,n5) -> 
% 2.75/1.09  10771:1:0:[10543.0,5387.1]:: p(n4,n8,n5) -> 
% 2.75/1.09  10839:1:0:[10538.0,6837.0]:: p(n4,n1,n9) -> 
% 2.75/1.09  10838:1:0:[10538.0,6836.0]:: p(n4,n1,n8) -> 
% 2.75/1.09  10837:1:0:[10538.0,6831.1]:: p(n4,n1,n5) -> 
% 2.75/1.09  10772:1:0:[10545.0,5394.1]:: p(n4,n8,n3) -> 
% 2.75/1.09  10836:1:0:[10538.0,6827.1]:: p(n4,n1,n4) -> 
% 2.75/1.09  10835:1:0:[10538.0,6822.1]:: p(n4,n1,n3) -> 
% 2.75/1.09  10834:1:0:[10538.0,6816.1]:: p(n4,n1,n2) -> 
% 2.75/1.09  10833:1:0:[10537.0,6804.0]:: p(n3,n9,n9) -> 
% 2.75/1.09  10832:1:0:[10537.0,6802.1]:: p(n3,n9,n7) -> 
% 2.75/1.09  10831:1:0:[10537.0,6800.1]:: p(n3,n9,n6) -> 
% 2.75/1.09  10830:1:0:[10537.0,6797.1]:: p(n3,n9,n5) -> 
% 2.75/1.09  10773:1:0:[10543.0,5423.1]:: p(n5,n8,n5) -> 
% 2.75/1.09  10829:1:0:[10537.0,6782.1]:: p(n3,n9,n2) -> 
% 2.75/1.09  10828:1:0:[10537.0,6775.1]:: p(n3,n9,n1) -> 
% 2.75/1.09  10774:1:0:[10545.0,5457.1]:: p(n6,n8,n3) -> 
% 2.75/1.09  10775:1:0:[10543.0,5459.0]:: p(n7,n8,n5) -> 
% 2.75/1.09  10776:1:0:[10543.0,5468.0]:: p(n8,n8,n5) -> 
% 2.75/1.09  10777:1:0:[10543.0,5477.0]:: p(n9,n8,n5) -> 
% 2.75/1.09  10778:1:0:[10545.0,5484.0]:: p(n8,n8,n3) -> 
% 2.75/1.09  10779:1:0:[10545.0,5493.0]:: p(n9,n8,n3) -> 
% 2.75/1.09  10780:1:0:[10537.0,5525.1]:: p(n1,n9,n8) -> 
% 2.75/1.09  10781:1:0:[10537.0,5588.1]:: p(n2,n9,n8) -> 
% 2.75/1.09  10827:1:0:[10536.0,6537.0]:: p(n3,n2,n9) -> 
% 2.75/1.09  10826:1:0:[10536.0,6535.0]:: p(n3,n2,n7) -> 
% 2.75/1.09  10825:1:0:[10536.0,6534.0]:: p(n3,n2,n6) -> 
% 2.75/1.09  10824:1:0:[10536.0,6532.0]:: p(n3,n2,n4) -> 
% 2.75/1.09  10782:1:0:[10547.0,5638.1]:: p(n2,n9,n4) -> 
% 2.75/1.09  10823:1:0:[10536.0,6525.1]:: p(n3,n2,n2) -> 
% 2.75/1.09  10822:1:0:[10536.0,6518.1]:: p(n3,n2,n1) -> 
% 2.75/1.09  10783:1:0:[10537.0,5651.0]:: p(n4,n9,n8) -> 
% 2.75/1.09  10784:1:0:[10537.0,5660.0]:: p(n5,n9,n8) -> 
% 2.75/1.09  10785:1:0:[10537.0,5669.0]:: p(n6,n9,n8) -> 
% 2.75/1.09  10786:1:0:[10537.0,5678.0]:: p(n7,n9,n8) -> 
% 2.75/1.09  10787:1:0:[10537.0,5687.0]:: p(n8,n9,n8) -> 
% 2.75/1.09  10788:1:0:[10547.0,5692.1]:: p(n3,n9,n4) -> 
% 2.75/1.09  10789:1:0:[10537.0,5696.0]:: p(n9,n9,n8) -> 
% 2.75/1.09  10790:1:0:[10547.0,5737.1]:: p(n4,n9,n4) -> 
% 2.75/1.09  10791:1:0:[10547.0,5800.1]:: p(n6,n9,n4) -> 
% 2.75/1.09  10792:1:0:[10547.0,5818.1]:: p(n7,n9,n4) -> 
% 2.75/1.09  10793:1:0:[10547.0,5827.1]:: p(n8,n9,n4) -> 
% 2.75/1.09  10821:1:0:[10535.0,6279.0]:: p(n2,n4,n9) -> 
% 2.75/1.09  10820:1:0:[10535.0,6278.0]:: p(n2,n4,n8) -> 
% 2.75/1.09  10819:1:0:[10535.0,6276.0]:: p(n2,n4,n6) -> 
% 2.75/1.09  10818:1:0:[10535.0,6273.0]:: p(n2,n4,n3) -> 
% 2.75/1.09  10817:1:0:[10535.0,6265.1]:: p(n2,n4,n1) -> 
% 2.75/1.09  10816:1:0:[10534.0,6222.0]:: p(n2,n2,n9) -> 
% 2.75/1.09  10815:1:0:[10534.0,6221.0]:: p(n2,n2,n8) -> 
% 2.75/1.09  10814:1:0:[10534.0,6220.0]:: p(n2,n2,n7) -> 
% 2.75/1.09  10813:1:0:[10534.0,6219.0]:: p(n2,n2,n6) -> 
% 2.75/1.09  10812:1:0:[10534.0,6214.1]:: p(n2,n2,n4) -> 
% 2.75/1.09  10811:1:0:[10534.0,6196.1]:: p(n2,n2,n1) -> 
% 2.75/1.09  10810:1:0:[10533.0,6056.0]:: p(n1,n7,n9) -> 
% 2.75/1.09  10809:1:0:[10533.0,6055.0]:: p(n1,n7,n8) -> 
% 2.75/1.09  10808:1:0:[10533.0,6053.0]:: p(n1,n7,n6) -> 
% 2.75/1.09  10807:1:0:[10533.0,6052.0]:: p(n1,n7,n5) -> 
% 2.75/1.09  10806:1:0:[10533.0,6050.0]:: p(n1,n7,n3) -> 
% 2.75/1.09  10805:1:0:[10533.0,6049.0]:: p(n1,n7,n2) -> 
% 2.75/1.09  10804:1:0:[10532.0,6011.0]:: p(n1,n5,n9) -> 
% 2.75/1.09  10803:1:0:[10532.0,6010.0]:: p(n1,n5,n8) -> 
% 2.75/1.09  10802:1:0:[10532.0,6007.1]:: p(n1,n5,n6) -> 
% 2.75/1.09  10801:1:0:[10532.0,6004.1]:: p(n1,n5,n5) -> 
% 2.75/1.09  10800:1:0:[10532.0,5995.1]:: p(n1,n5,n3) -> 
% 2.75/1.09  10799:1:0:[10532.0,5989.1]:: p(n1,n5,n2) -> 
% 2.75/1.09  10798:1:0:[10531.0,5966.0]:: p(n1,n4,n9) -> 
% 2.75/1.09  10797:1:0:[10531.0,5965.0]:: p(n1,n4,n8) -> 
% 2.75/1.09  10796:1:0:[10531.0,5963.0]:: p(n1,n4,n6) -> 
% 2.75/1.09  10795:1:0:[10531.0,5962.0]:: p(n1,n4,n5) -> 
% 2.75/1.09  10794:1:0:[10531.0,5956.1]:: p(n1,n4,n3) -> 
% 2.75/1.09  
% 2.75/1.09   Most General Atoms: p(n1,n1,n1) p(n1,n2,n1) p(n1,n1,n2) p(n1,n2,n2) p(n1,n1,n3) p(n1,n2,n3) p(n1,n1,n4) p(n1,n2,n4) p(n1,n1,n5) p(n1,n2,n5) p(n1,n1,n6) p(n1,n2,n6) p(n1,n1,n7) p(n1,n2,n7) p(n1,n1,n8) p(n1,n2,n8) p(n1,n1,n9) p(n1,n2,n9) p(n1,n3,n1) p(n1,n3,n2) p(n1,n3,n3) p(n1,n3,n4) p(n1,n3,n5) p(n1,n3,n6) p(n1,n3,n7) p(n1,n3,n8) p(n1,n3,n9) p(n1,n4,n1) p(n1,n4,n2) p(n1,n4,n3) p(n1,n4,n5) p(n1,n4,n6) p(n1,n4,n7) p(n1,n4,n8) p(n1,n4,n9) p(n1,n5,n1) p(n1,n5,n2) p(n1,n5,n3) p(n9,n9,n4) p(n1,n5,n5) p(n1,n5,n6) p(n1,n5,n8) p(n1,n5,n9) p(n1,n6,n1) p(n1,n6,n2) p(n1,n6,n3) p(n8,n1,n1) p(n1,n6,n5) p(n1,n6,n6) p(n7,n8,n3) p(n1,n6,n8) p(n1,n6,n9) p(n1,n7,n2) p(n1,n7,n3) p(n7,n4,n7) p(n1,n7,n5) p(n1,n7,n6) p(n6,n8,n5) p(n1,n7,n8) p(n1,n7,n9) p(n5,n6,n3) p(n1,n8,n2) p(n1,n8,n3) p(n5,n3,n4) p(n1,n8,n5) p(n1,n8,n6) p(n4,n7,n7) p(n1,n8,n8) p(n1,n8,n9) p(n4,n5,n1) p(n1,n9,n2) p(n1,n9,n3) p(n4,n1,n6) p(n1,n9,n5) p(n1,n9,n6) p(n3,n9,n8) p(n1,n9,n8) p(n1,n9,n9) p(n3,n2,n3) p(n2,n4,n2) p(n2,n2,n5) p(n1,n7,n1) p(n1,n5,n7) p(n1,n4,n4) p(n7,n7,n9) p(n7,n9,n9) p(n8,n7,n9) p(n8,n8,n9) p(n8,n9,n9) p(n9,n7,n9) p(n9,n8,n9) p(n7,n7,n8) p(n8,n7,n8) p(n8,n8,n8) p(n9,n7,n8) p(n9,n8,n8) p(n8,n8,n7) p(n8,n9,n7) p(n9,n8,n7) p(n7,n7,n6) p(n7,n9,n6) p(n8,n7,n6) p(n8,n8,n6) p(n8,n9,n6) p(n9,n7,n6) p(n9,n8,n6) p(n7,n7,n5) p(n7,n9,n5) p(n8,n7,n5) p(n8,n9,n5) p(n9,n7,n5) p(n7,n7,n2) p(n7,n9,n2) p(n8,n7,n2) p(n8,n8,n2) p(n8,n9,n2) p(n9,n7,n2) p(n9,n8,n2) p(n7,n9,n1) p(n9,n8,n1) 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(n7,n6,n8) p(n8,n4,n8) p(n8,n5,n8) p(n8,n6,n8) p(n9,n4,n8) p(n9,n5,n8) p(n9,n6,n8) p(n7,n5,n6) p(n7,n6,n6) p(n8,n4,n6) p(n8,n5,n6) p(n8,n6,n6) p(n9,n4,n6) p(n9,n5,n6) p(n9,n6,n6) p(n7,n5,n5) p(n7,n6,n5) p(n8,n4,n5) p(n8,n5,n5) p(n8,n6,n5) p(n9,n4,n5) p(n9,n5,n5) p(n9,n6,n5) p(n7,n5,n4) p(n7,n6,n4) p(n8,n5,n4) p(n8,n6,n4) p(n7,n5,n2) p(n7,n6,n2) p(n8,n5,n2) p(n8,n6,n2) p(n9,n5,n2) p(n9,n6,n2) p(n7,n6,n1) p(n9,n4,n1) p(n9,n6,n1) p(n7,n1,n9) p(n7,n2,n9) p(n7,n3,n9) p(n8,n2,n9) p(n8,n3,n9) p(n9,n1,n9) p(n9,n2,n9) p(n9,n3,n9) p(n7,n1,n8) p(n7,n2,n8) p(n7,n3,n8) p(n8,n2,n8) p(n8,n3,n8) p(n9,n1,n8) p(n9,n2,n8) p(n9,n3,n8) p(n1,n5,n4) p(n1,n6,n4) p(n8,n2,n7) p(n8,n3,n7) p(n9,n1,n7) p(n9,n2,n7) p(n9,n3,n7) p(n1,n7,n4) p(n7,n2,n6) p(n7,n3,n6) p(n8,n2,n6) p(n8,n3,n6) p(n9,n2,n6) p(n9,n3,n6) p(n7,n1,n5) p(n7,n3,n5) p(n8,n3,n5) p(n9,n1,n5) p(n9,n3,n5) p(n1,n8,n4) p(n8,n3,n3) p(n9,n1,n3) p(n9,n3,n3) p(n7,n1,n2) p(n7,n2,n2) p(n7,n3,n2) p(n8,n2,n2) p(n8,n3,n2) p(n9,n1,n2) p(n9,n2,n2) p(n9,n3,n2) p(n1,n9,n4) p(n4,n8,n9) p(n4,n9,n9) p(n5,n7,n9) p(n5,n8,n9) p(n5,n9,n9) p(n6,n7,n9) p(n6,n9,n9) p(n4,n8,n8) p(n5,n7,n8) p(n5,n8,n8) p(n6,n7,n8) p(n1,n6,n7) p(n5,n7,n6) p(n5,n8,n6) p(n5,n9,n6) p(n6,n7,n6) p(n6,n9,n6) p(n1,n7,n7) p(n4,n8,n4) p(n6,n7,n4) p(n4,n9,n3) p(n6,n7,n3) p(n6,n9,n3) p(n1,n8,n7) p(n4,n8,n2) p(n4,n9,n2) p(n5,n7,n2) p(n5,n8,n2) p(n5,n9,n2) p(n6,n7,n2) p(n6,n9,n2) p(n5,n8,n1) p(n5,n9,n1) p(n6,n9,n1) p(n1,n9,n7) p(n4,n4,n9) p(n4,n6,n9) p(n5,n4,n9) p(n5,n5,n9) p(n6,n4,n9) p(n6,n5,n9) p(n6,n6,n9) p(n4,n4,n8) p(n4,n6,n8) p(n5,n4,n8) p(n5,n5,n8) p(n6,n4,n8) p(n6,n5,n8) p(n6,n6,n8) p(n5,n4,n6) p(n5,n5,n6) p(n6,n4,n6) p(n6,n5,n6) p(n6,n6,n6) p(n4,n4,n5) p(n4,n6,n5) p(n5,n4,n5) p(n5,n5,n5) p(n4,n6,n4) p(n6,n5,n4) p(n6,n6,n4) p(n4,n6,n2) p(n5,n5,n2) p(n6,n5,n2) p(n6,n6,n2) p(n4,n2,n9) p(n4,n3,n9) p(n5,n1,n9) p(n5,n2,n9) p(n6,n1,n9) p(n6,n2,n9) p(n6,n3,n9) p(n4,n2,n8) p(n4,n3,n8) p(n5,n1,n8) p(n5,n2,n8) p(n6,n1,n8) p(n6,n2,n8) p(n6,n3,n8) p(n1,n8,n1) p(n4,n3,n5) p(n5,n1,n5) p(n4,n3,n3) p(n6,n1,n3) p(n6,n3,n3) p(n1,n9,n1) p(n4,n2,n2) p(n4,n3,n2) p(n5,n1,n2) p(n5,n2,n2) p(n6,n1,n2) p(n6,n2,n2) p(n6,n3,n2) p(n2,n7,n9) p(n2,n8,n9) p(n2,n9,n9) p(n3,n7,n9) p(n3,n8,n9) p(n2,n8,n7) p(n2,n9,n7) p(n3,n8,n7) p(n2,n7,n6) p(n2,n8,n6) p(n2,n9,n6) p(n3,n7,n6) p(n3,n8,n6) p(n3,n7,n5) p(n2,n1,n1) p(n2,n2,n1) p(n2,n1,n2) p(n2,n2,n2) p(n2,n1,n3) p(n2,n2,n3) p(n2,n1,n4) p(n2,n2,n4) p(n2,n1,n5) p(n2,n1,n6) p(n2,n2,n6) p(n2,n1,n7) p(n2,n2,n7) p(n2,n1,n8) p(n2,n2,n8) p(n2,n1,n9) p(n2,n2,n9) p(n2,n3,n1) p(n2,n3,n2) p(n2,n3,n3) p(n2,n3,n4) p(n2,n7,n4) p(n2,n8,n4) p(n3,n7,n4) p(n3,n8,n4) p(n2,n3,n6) p(n2,n3,n7) p(n2,n3,n8) p(n2,n3,n9) p(n2,n4,n1) p(n2,n4,n3) p(n2,n4,n4) p(n3,n7,n2) p(n3,n8,n2) p(n2,n4,n6) p(n2,n4,n7) p(n2,n4,n8) p(n2,n4,n9) p(n2,n5,n1) p(n2,n5,n9) p(n2,n6,n9) p(n3,n4,n9) p(n3,n5,n9) p(n3,n6,n9) p(n2,n5,n3) p(n2,n5,n4) p(n2,n5,n8) p(n2,n6,n8) p(n2,n5,n6) p(n2,n5,n7) p(n2,n6,n1) p(n2,n6,n6) p(n3,n4,n6) p(n3,n5,n6) p(n3,n6,n6) p(n2,n6,n3) p(n2,n6,n4) p(n3,n4,n5) p(n3,n5,n5) p(n3,n6,n5) p(n2,n6,n7) p(n2,n7,n1) p(n2,n7,n3) p(n3,n4,n1) p(n3,n6,n1) p(n2,n7,n7) p(n2,n7,n8) p(n2,n8,n1) p(n3,n1,n9) p(n3,n3,n9) p(n2,n8,n3) p(n2,n8,n8) p(n2,n9,n1) p(n3,n1,n7) p(n3,n3,n7) p(n2,n9,n3) p(n2,n9,n4) p(n3,n3,n6) p(n2,n9,n8) p(n2,n3,n5) p(n2,n4,n5) p(n3,n1,n4) p(n2,n5,n5) p(n3,n1,n2) p(n3,n3,n2) p(n2,n6,n5) p(n3,n3,n1) p(n2,n7,n5) p(n2,n8,n5) p(n2,n9,n5) p(n9,n5,n3) p(n9,n4,n3) p(n8,n5,n3) p(n2,n5,n2) p(n8,n4,n3) p(n2,n6,n2) p(n2,n7,n2) p(n8,n2,n4) p(n2,n8,n2) p(n2,n9,n2) p(n7,n2,n4) p(n7,n1,n4) p(n6,n3,n1) p(n6,n3,n7) p(n6,n2,n1) p(n6,n2,n7) p(n6,n1,n7) p(n5,n2,n1) p(n5,n2,n7) p(n5,n1,n7) p(n3,n1,n1) p(n3,n2,n1) p(n3,n2,n2) p(n3,n1,n3) p(n3,n2,n4) p(n3,n1,n5) p(n3,n2,n5) p(n3,n1,n6) p(n3,n2,n6) p(n3,n2,n7) p(n3,n1,n8) p(n3,n2,n8) p(n3,n2,n9) p(n3,n3,n4) p(n3,n3,n5) p(n3,n3,n8) p(n3,n4,n2) p(n3,n4,n4) p(n3,n4,n7) p(n3,n4,n8) p(n3,n5,n1) p(n3,n5,n2) p(n3,n5,n4) p(n3,n5,n7) p(n3,n5,n8) p(n3,n6,n2) p(n3,n6,n4) p(n3,n6,n7) p(n3,n6,n8) p(n3,n7,n1) p(n3,n7,n7) p(n3,n7,n8) p(n3,n8,n1) p(n3,n8,n5) p(n3,n8,n8) p(n3,n9,n1) p(n3,n9,n2) p(n3,n9,n4) p(n3,n9,n5) p(n3,n9,n6) p(n3,n9,n7) p(n3,n9,n9) p(n3,n3,n3) p(n3,n4,n3) p(n3,n5,n3) p(n3,n6,n3) p(n3,n7,n3) p(n3,n8,n3) p(n3,n9,n3) p(n4,n1,n1) p(n4,n2,n1) p(n4,n1,n2) p(n4,n1,n3) p(n4,n2,n3) p(n4,n1,n4) p(n4,n2,n4) p(n4,n1,n5) p(n4,n2,n5) p(n4,n2,n6) p(n4,n1,n7) p(n4,n2,n7) p(n4,n1,n8) p(n4,n1,n9) p(n4,n3,n1) p(n4,n3,n4) p(n4,n3,n6) p(n4,n3,n7) p(n4,n4,n1) p(n4,n4,n2) p(n4,n4,n3) p(n4,n4,n4) p(n4,n4,n6) p(n4,n4,n7) p(n4,n5,n2) p(n4,n5,n3) p(n4,n5,n4) 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,n6) p(n4,n6,n7) 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,n7,n9) p(n4,n8,n3) p(n4,n8,n5) p(n4,n8,n6) p(n4,n9,n4) p(n4,n9,n5) p(n4,n9,n6) p(n4,n9,n8) p(n6,n6,n7) p(n4,n6,n1) p(n4,n7,n1) p(n4,n8,n1) p(n4,n9,n1) p(n4,n8,n7) p(n4,n9,n7) p(n5,n1,n1) p(n5,n1,n3) p(n5,n2,n3) p(n5,n1,n4) p(n5,n2,n4) p(n5,n2,n5) p(n5,n1,n6) p(n5,n2,n6) p(n5,n3,n1) p(n5,n3,n2) p(n5,n3,n3) 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(n5,n4,n2) p(n5,n4,n3) p(n5,n4,n7) p(n5,n5,n1) p(n5,n5,n3) p(n5,n5,n7) p(n5,n6,n1) p(n5,n6,n2) p(n5,n6,n5) p(n5,n6,n6) p(n5,n6,n7) p(n5,n6,n8) p(n5,n6,n9) p(n5,n7,n1) p(n5,n7,n5) p(n5,n7,n7) p(n5,n8,n5) p(n5,n8,n7) p(n5,n9,n5) p(n5,n9,n7) p(n5,n9,n8) p(n5,n4,n4) p(n5,n5,n4) p(n5,n6,n4) p(n5,n7,n4) p(n5,n8,n4) p(n5,n9,n4) p(n5,n7,n3) p(n5,n8,n3) p(n5,n9,n3) p(n6,n1,n1) 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,n3,n4) p(n6,n3,n5) p(n6,n3,n6) p(n6,n4,n1) p(n6,n4,n2) p(n6,n4,n3) p(n6,n4,n4) p(n6,n4,n5) p(n6,n4,n7) p(n6,n5,n1) p(n6,n5,n3) p(n6,n5,n5) p(n6,n5,n7) p(n6,n6,n1) p(n6,n6,n3) p(n6,n6,n5) p(n6,n7,n1) p(n6,n7,n5) p(n6,n7,n7) p(n6,n8,n1) p(n6,n8,n2) p(n6,n8,n3) p(n6,n8,n4) p(n6,n8,n6) p(n6,n8,n7) p(n6,n8,n8) p(n6,n8,n9) p(n6,n9,n4) p(n6,n9,n7) p(n6,n9,n8) p(n6,n9,n5) p(n7,n1,n1) p(n7,n2,n1) p(n7,n1,n3) p(n7,n2,n3) p(n7,n2,n5) p(n7,n1,n6) p(n7,n1,n7) p(n7,n2,n7) p(n7,n3,n1) p(n7,n3,n3) p(n7,n3,n4) 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,n3) p(n7,n6,n3) p(n7,n7,n1) p(n7,n7,n3) p(n7,n7,n4) p(n7,n8,n1) p(n7,n8,n2) p(n7,n8,n4) p(n7,n8,n5) p(n7,n8,n6) p(n7,n8,n8) p(n7,n8,n9) p(n7,n9,n4) p(n7,n9,n8) p(n8,n8,n4) p(n7,n5,n7) p(n7,n6,n7) p(n7,n7,n7) p(n7,n8,n7) p(n7,n9,n7) p(n8,n7,n4) p(n7,n9,n3) p(n8,n2,n1) p(n8,n1,n2) p(n8,n1,n3) p(n8,n2,n3) p(n8,n1,n4) p(n8,n1,n5) p(n8,n2,n5) p(n8,n1,n6) p(n8,n1,n7) p(n8,n1,n8) p(n8,n1,n9) p(n8,n3,n1) p(n8,n3,n4) p(n8,n4,n1) p(n8,n4,n2) p(n8,n4,n4) p(n8,n4,n7) p(n8,n5,n1) p(n8,n5,n7) p(n8,n6,n1) p(n8,n6,n3) p(n8,n6,n7) p(n8,n7,n1) p(n8,n7,n3) p(n8,n7,n7) p(n8,n8,n1) p(n8,n8,n3) p(n8,n8,n5) p(n8,n9,n1) p(n8,n9,n3) p(n8,n9,n4) p(n8,n9,n8) p(n9,n7,n3) p(n9,n1,n1) p(n9,n2,n1) p(n9,n2,n3) p(n9,n1,n4) p(n9,n2,n4) p(n9,n2,n5) p(n9,n1,n6) p(n9,n3,n1) p(n9,n3,n4) p(n9,n4,n2) p(n9,n4,n4) p(n9,n4,n7) p(n9,n5,n1) p(n9,n5,n4) p(n9,n5,n7) p(n9,n6,n3) p(n9,n6,n4) p(n9,n6,n7) p(n9,n7,n1) p(n9,n7,n4) p(n9,n7,n7) p(n9,n8,n3) p(n9,n8,n4) p(n9,n8,n5) p(n9,n9,n1) p(n9,n9,n2) p(n9,n9,n3) p(n9,n9,n5) p(n9,n9,n6) p(n9,n9,n7) p(n9,n9,n8) p(n9,n9,n9) 
% 2.75/1.09  
% 2.75/1.09  === Starting SPASS-SCL-FOL A Little Less Naive, considering 729 atoms initially, heuristics mode: resolution_2 ===
% 2.75/1.09  
% 2.75/1.09  === Conflict found: 11174:3:0:[10885.1,10272.0,10709.1,11169.1,10753.1,11170.5,10946.1,11171.6,10778.1,11172.7,10947.1,11173.8]::  -> p(n8,n3,n3),p(n8,n4,n3),p(n8,n5,n3) {}
% 2.75/1.09  === Backtracking. Learning clause 11973:2:0:[10011.0,11972.2,11174.2,4206.1,3783.2]:: p(n9,n4,n3),p(n4,n3,n3) -> 
% 2.75/1.09  === Conflict found: 11148:2:0:[10696.0,10261.0,10939.0,11142.1,10940.0,11143.2,10873.0,11144.3,10747.1,11145.4,10759.1,11146.6,10878.0,11147.7]::  -> p(n7,n6,n1),p(n7,n9,n1) {}
% 2.75/1.09  === Backtracking. Learning clause 11975:4:0:[11389.0,11974.0,11148.2,8068.1,4645.2,11467.2,10988.2,6137.2,6234.1,10962.1,11303.1,1780.1]::  -> p(n8,n9,n5),p(n3,n3,n7),p(n8,n3,n7),p(n9,n3,n7)
% 2.75/1.09  === Backtracking. Learning clause 11976:2:0:[4559.1,10969.1]:: p(n4,n6,n5) -> p(n1,n9,n5)
% 2.75/1.09  === Conflict found: 11059:2:0:[10835.0,10236.0,10707.1,11053.1,10927.0,11054.3,10841.1,11055.4,10751.0,11056.5,10847.0,11057.6,10772.0,11058.7]::  -> p(n4,n3,n3),p(n4,n9,n3) {}
% 2.75/1.09  === Backtracking. Learning clause 11977:1:0:[11059.1,6893.1,5529.2,11072.1,11976.1,6137.2,10962.1]::  -> p(n4,n4,n5)
% 2.75/1.09  === Backtracking. Learning clause 11980:9:0:[11787.0,11978.5,10070.1,11979.8,8682.1,11428.2,11215.4,7387.1,11450.2,8530.1,11216.3,3473.2,11076.1,7081.2,10052.2,5174.2,3508.2,11895.1,7684.2,4625.2,10025.2,11801.3,6041.2,4535.2,10016.2,6320.2]:: p(n7,n7,n8),p(n5,n2,n7),p(n6,n7,n3),p(n1,n6,n5),p(n8,n5,n8) -> p(n9,n1,n7),p(n9,n1,n8),p(n4,n3,n8),p(n4,n4,n8)
% 2.75/1.09  === Backtracking. Learning clause 11983:4:0:[10962.0,11981.0,6726.1,11982.4,6398.2,11831.3,11408.1,6141.2,5364.1,5247.1,6718.1,5310.1]:: p(n3,n7,n5),p(n8,n8,n9) -> p(n2,n9,n9),p(n6,n7,n4)
% 2.75/1.09  === Backtracking. Learning clause 11986:10:0:[11059.0,11984.2,10962.0,11985.4,8597.1,11208.4,11360.6,7621.2,5045.2,2195.1,11129.1,8524.1,7656.1,11389.1,4604.2,1556.1,11215.3,8682.2,11428.2,7387.1,11450.2,7081.2,11895.1,7684.2,10052.2,3508.2,11980.5,6320.2,11105.2,8444.2,6896.2,8443.2,10070.2,11787.1,11888.2,11913.2,5547.2]:: p(n3,n7,n5),p(n1,n6,n5),p(n7,n7,n8) -> p(n9,n1,n5),p(n9,n4,n5),p(n4,n4,n8),p(n5,n1,n7),p(n4,n9,n3),p(n8,n3,n3),p(n9,n3,n3)
% 2.75/1.09  === Conflict found: 11243:5:0:[10549.0,10294.0,10611.0,11240.3,10652.0,11241.6,10888.1,11242.7]::  -> p(n2,n1,n7),p(n3,n1,n7),p(n5,n1,n7),p(n6,n1,n7),p(n9,n1,n7) {}
% 2.75/1.09  === Backtracking. Learning clause 11988:6:0:[10962.0,11987.1,11243.4,1663.1,6504.2,394.1,11477.1,11032.1,10204.1,5323.1,6718.1,11215.4,8443.2,3508.2,11105.2,11913.2,11895.1,7684.2,11888.2,5547.2,11389.1]:: p(n3,n7,n5) -> p(n9,n3,n7),p(n5,n1,n7),p(n8,n3,n3),p(n9,n3,n3),p(n4,n9,n3)
% 2.75/1.09  === Conflict found: 11140:7:0:[10871.1,10259.7,10785.1,11139.8]::  -> p(n6,n1,n8),p(n6,n2,n8),p(n6,n3,n8),p(n6,n4,n8),p(n6,n5,n8),p(n6,n6,n8),p(n6,n7,n8) {}
% 2.75/1.09  === Backtracking. Learning clause 11992:8:0:[11389.0,11989.2,3473.1,11990.6,5507.1,11991.10,11140.7,7688.2,9296.2,3446.2,4184.1,9305.2,7666.2,11216.4,10178.2]:: p(n6,n7,n3),p(n4,n2,n8),p(n8,n8,n8) -> p(n6,n5,n8),p(n9,n1,n8),p(n9,n3,n8),p(n9,n5,n8),p(n9,n6,n8)
% 2.75/1.09  === Conflict found: 11809:4:0:[10805.1,10469.0,10585.1,11805.3,10586.1,11806.4,10587.1,11807.5,10829.0,11808.8]::  -> p(n1,n8,n2),p(n1,n9,n2),p(n3,n7,n2),p(n3,n8,n2) {}
% 2.75/1.09  === Backtracking. Learning clause 11993:4:0:[11809.4,6745.1,6707.1]:: p(n3,n8,n7),p(n3,n7,n5) -> p(n1,n8,n2),p(n1,n9,n2)
% 2.75/1.09  === Conflict found: 11710:5:0:[10674.1,10439.0,10778.1,11707.2,10950.0,11708.3,10776.1,11709.4]::  -> p(n8,n8,n2),p(n8,n8,n6),p(n8,n8,n7),p(n8,n8,n8),p(n8,n8,n9) {}
% 2.75/1.09  === Backtracking. Learning clause 11994:8:0:[11710.1,5240.2,2590.1,2571.2,11993.3,11046.3,3751.1]:: p(n8,n9,n7),p(n8,n7,n6),p(n3,n7,n5),p(n9,n3,n7) -> p(n8,n8,n8),p(n8,n8,n9),p(n1,n9,n2),p(n3,n1,n7)
% 2.75/1.09  === Conflict found: 11133:5:0:[10690.1,10257.0,10922.1,11130.1,10923.1,11131.2,10869.1,11132.7]::  -> p(n6,n4,n6),p(n6,n5,n6),p(n6,n6,n6),p(n6,n7,n6),p(n6,n9,n6) {}
% 2.75/1.09  === Backtracking. Learning clause 11998:8:0:[10969.0,11995.0,11059.0,11996.1,10962.0,11997.2,11133.5,5613.2,7663.1,11540.2,7686.2,7592.1,7619.2,11140.4,3446.2,9296.2,9305.2,7688.2,7666.2,11076.1,4625.2,11801.3,6041.2,7621.2,11129.1,6320.2,11787.1,6896.2,7656.1,394.2,11243.1,1663.1,6504.2,11032.1,5323.1,7081.2,6718.1,11895.1,7684.2,11888.2,11389.1,5547.2,2608.1,11988.2,7156.2,11821.2]:: p(n5,n1,n5) -> p(n2,n9,n3),p(n2,n9,n9),p(n4,n4,n8),p(n8,n3,n3),p(n9,n3,n3),p(n4,n9,n3),p(n1,n9,n5)
% 2.75/1.09  === Conflict found: 11988:6:0:[10962.0,11987.1,11243.4,1663.1,6504.2,394.1,11477.1,11032.1,10204.1,5323.1,6718.1,11215.4,8443.2,3508.2,11105.2,11913.2,11895.1,7684.2,11888.2,5547.2,11389.1]:: p(n3,n7,n5) -> p(n9,n3,n7),p(n5,n1,n7),p(n8,n3,n3),p(n9,n3,n3),p(n4,n9,n3) {}
% 2.75/1.09  === Backtracking. Learning clause 11999:6:0:[11988.1,11821.2,7156.2]:: p(n5,n1,n5) -> p(n9,n3,n7),p(n8,n3,n3),p(n9,n3,n3),p(n4,n9,n3),p(n1,n9,n5)
% 2.75/1.09  === Conflict found: 11809:4:0:[10805.1,10469.0,10585.1,11805.3,10586.1,11806.4,10587.1,11807.5,10829.0,11808.8]::  -> p(n1,n8,n2),p(n1,n9,n2),p(n3,n7,n2),p(n3,n8,n2) {}
% 2.75/1.09  === Backtracking. Learning clause 12001:3:0:[10962.0,12000.0,11809.2,6129.1]::  -> p(n1,n8,n2),p(n3,n7,n2),p(n3,n8,n2)
% 2.75/1.09  === Conflict found: 11076:5:0:[10838.1,10241.0,10844.1,11073.4,10850.1,11074.6,10783.1,11075.8]::  -> p(n4,n2,n8),p(n4,n3,n8),p(n4,n4,n8),p(n4,n6,n8),p(n4,n8,n8) {}
% 2.75/1.09  === Backtracking. Learning clause 12004:3:0:[11977.0,12002.0,9332.0,12003.2,11076.3,6941.2,9296.1]:: p(n6,n1,n8) -> p(n4,n6,n8),p(n4,n8,n8)
% 2.75/1.09  === Conflict found: 11046:3:0:[10826.1,10231.1,10732.0,11041.3,10738.1,11042.4,10911.1,11043.5,10762.0,11044.6,10832.0,11045.8]::  -> p(n3,n1,n7),p(n3,n3,n7),p(n3,n8,n7) {}
% 2.75/1.09  === Backtracking. Learning clause 12006:4:0:[10962.0,12005.2,11046.3,11993.1,3751.1,6129.1]:: p(n3,n7,n5),p(n9,n3,n7) -> p(n3,n1,n7),p(n1,n8,n2)
% 2.75/1.09  === Backtracking. Learning clause 12007:3:0:[4625.1,11801.3,12004.2,6041.2,6320.2,11787.1]:: p(n6,n1,n8),p(n1,n6,n5) -> p(n4,n8,n8)
% 2.75/1.09  === Backtracking. Learning clause 12008:4:0:[6504.1,11032.1,12006.3,5323.1,6718.1,11821.2]:: p(n9,n3,n7),p(n4,n8,n4) -> p(n1,n8,n2),p(n1,n9,n5)
% 2.75/1.09  === Conflict found: 12004:3:0:[11977.0,12002.0,9332.0,12003.2,11076.3,6941.2,9296.1]:: p(n6,n1,n8) -> p(n4,n6,n8),p(n4,n8,n8) {}
% 2.75/1.09  === Backtracking. Learning clause 12009:4:0:[12004.3,7081.2,4625.2,11801.3,6041.2]:: p(n6,n1,n8),p(n4,n8,n4),p(n1,n6,n5) -> p(n2,n5,n8)
% 2.75/1.09  === Conflict found: 11208:6:0:[10706.1,10283.1,10777.1,11206.7,10894.1,11207.8]::  -> p(n9,n1,n5),p(n9,n3,n5),p(n9,n4,n5),p(n9,n5,n5),p(n9,n6,n5),p(n9,n7,n5) {}
% 2.75/1.09  === Backtracking. Learning clause 12011:11:0:[11977.0,12010.0,11208.3,4118.2,3182.2,8597.1,11992.7]:: p(n5,n1,n5),p(n6,n7,n3),p(n4,n2,n8),p(n8,n8,n8) -> p(n9,n3,n5),p(n9,n6,n5),p(n9,n7,n5),p(n6,n5,n8),p(n9,n1,n8),p(n9,n3,n8),p(n9,n6,n8)
% 2.75/1.09  === Backtracking. Learning clause 12012:5:0:[3188.1,11639.1]:: p(n7,n1,n2) -> p(n6,n1,n3),p(n6,n1,n7),p(n6,n1,n8),p(n6,n1,n9)
% 2.75/1.09  === Backtracking. Learning clause 12013:10:0:[2693.2,11371.5,11257.7,8148.1,8290.1]:: p(n8,n2,n6),p(n8,n6,n4) -> p(n4,n6,n2),p(n6,n6,n2),p(n7,n6,n2),p(n1,n2,n2),p(n4,n2,n2),p(n5,n2,n2),p(n6,n2,n2),p(n7,n2,n2)
% 2.75/1.09  
% 2.75/1.09  Linear Model Building succeeded.
% 2.75/1.09  SZS status Satisfiable
% 2.75/1.09  
% 2.75/1.09  Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.75/1.09  
% 2.75/1.09  SPASS-SCL-FOL Statistics:
% 2.75/1.09  Number of learned clauses: 22
% 2.75/1.09  Number of propagations: 4811
% 2.75/1.09  Number of decisions: 64
% 2.75/1.09  Number of resolutions: 182
% 2.75/1.09  Number of condensations: 0
% 2.75/1.09  Number of sub resolutions: 1444
% 2.75/1.09  Number of input literals (deduplicated): 729
% 2.75/1.09  Number of grows: 0
% 2.75/1.09  Number of considered ground atoms: 729
% 2.75/1.09  
% 2.75/1.09   Needed:       0:00:00.49
% 2.75/1.09  
%------------------------------------------------------------------------------