%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : KRS040+1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:26:18 PM UTC 2026
% Result : Satisfiable 13.58s 3.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS040+1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.33 % Computer : n011.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Thu May 7 12:18:48 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 13.58/3.26 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.58/3.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.58/3.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.58/3.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.58/3.26 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.58/3.26 Execution resolution_2 ended with status: satisfiable
% 13.58/3.26 Used heuristic: resolution_2
% 13.58/3.26
% 13.58/3.26 Input Clauses:
% 13.58/3.26
% 13.58/3.26 Predicates: = cTorF cowlNothing cowlThing xsd_integer xsd_string
% 13.58/3.26 Fol Constants: iminus3 iplus3 iminus1 iplus1 iplus4 iminus4 iplus7 iminus7 iplus6 iminus6 iminus5 iplus5 iplus2 iminus2 iplus8 iminus8 iplus9 iminus9 iF iT
% 13.58/3.26 Fol Functions:
% 13.58/3.26 Problem Properties:
% 13.58/3.26 This is a Bernays Schoenfinkel Ramsey problem.
% 13.58/3.26
% 13.58/3.26
% 13.58/3.26 Reduced Input Clauses:
% 13.58/3.26
% 13.58/3.26 Most General Atoms: =(x0,x1) cTorF(x1) xsd_integer(x1) xsd_string(x1) cowlThing(x0) cowlNothing(x0)
% 13.58/3.26
% 13.58/3.26 === Starting SPASS-SCL-FOL A Little Less Naive, considering 500 atoms initially, heuristics mode: resolution_2 ===
% 13.58/3.26
% 13.58/3.26 === CC is in false state. New clause to be learned: 106:4:0:TAUT:: =(iminus9,iplus5),=(iT,iminus6),=(iT,iminus9) -> =(iminus6,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 107:2:0:TAUT:: =(iminus4,iminus6) -> =(iminus6,iminus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 108:4:0:TAUT:: =(iminus7,iminus6),=(iminus6,iplus7),=(iminus3,iplus7) -> =(iminus3,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 109:1:0:TAUT:: -> =(iplus7,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 110:1:0:TAUT:: -> =(iminus2,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 111:1:0:TAUT:: -> =(iplus3,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 112:3:0:TAUT:: =(iplus8,iminus1),=(iplus4,iplus8) -> =(iplus4,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 114:4:0:[105.0,113.4]:: =(iminus4,iF),=(iminus2,iT),=(iminus6,iminus2),=(iminus4,iminus6) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 115:1:0:TAUT:: -> =(iminus6,iminus6)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 116:4:0:TAUT:: =(iminus7,iminus8),=(iT,iminus8),=(iminus9,iT) -> =(iminus7,iminus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 118:1:0:[105.0,117.1]:: =(iF,iT) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 119:4:0:TAUT:: =(iminus7,iT),=(iT,iplus3),=(iplus3,iplus4) -> =(iplus4,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 120:3:0:TAUT:: =(iminus1,iplus1),=(iminus1,iminus3) -> =(iminus3,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 121:6:0:TAUT:: =(iminus8,iplus3),=(iminus8,iT),=(iminus2,iT),=(iminus3,iminus2),=(iplus7,iminus3) -> =(iplus7,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 122:4:0:TAUT:: =(iplus8,iplus3),=(iplus3,iminus2),=(iminus2,iT) -> =(iT,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 123:5:0:TAUT:: =(iplus6,iplus7),=(iplus5,iplus6),=(iplus1,iplus5),=(iplus1,iminus2) -> =(iplus7,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 124:1:0:TAUT:: -> =(iplus6,iplus6)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 125:6:0:TAUT:: =(iminus2,iplus6),=(iplus3,iminus6),=(iminus6,iminus8),=(iminus8,iminus9),=(iminus2,iminus9) -> =(iplus3,iplus6)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 126:2:0:TAUT:: =(iminus1,iplus6) -> =(iplus6,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 127:4:0:TAUT:: =(iminus7,iminus6),=(iminus6,iminus9),=(iminus4,iminus9) -> =(iminus4,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 128:2:0:TAUT:: =(iplus3,iplus7) -> =(iplus7,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 129:2:0:TAUT:: =(iplus1,iplus4) -> =(iplus4,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 130:1:0:TAUT:: -> =(iplus1,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 131:4:0:TAUT:: =(iminus6,iminus5),=(iminus5,iplus6),=(iplus5,iplus6) -> =(iminus6,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 132:6:0:TAUT:: =(iminus5,iminus1),=(iminus2,iplus5),=(iminus2,iT),=(iminus8,iT),=(iminus8,iminus1) -> =(iplus5,iminus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 133:4:0:TAUT:: =(iminus7,iplus9),=(iplus9,iplus1),=(iplus1,iminus2) -> =(iminus2,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 134:1:0:TAUT:: -> =(iplus5,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 135:3:0:TAUT:: =(iminus7,iminus5),=(iminus5,iplus1) -> =(iplus1,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 136:6:0:TAUT:: =(iminus6,iminus7),=(iminus6,iT),=(iT,iplus3),=(iplus3,iminus1),=(iplus2,iminus1) -> =(iplus2,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 137:1:0:TAUT:: -> =(iplus8,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 138:4:0:TAUT:: =(iminus4,iF),=(iminus4,iplus7),=(iplus8,iplus7) -> =(iF,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 139:6:0:TAUT:: =(iplus7,iminus5),=(iT,iplus7),=(iplus8,iT),=(iplus3,iplus8),xsd_integer(iminus5) -> xsd_integer(iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 140:2:0:TAUT:: =(iplus8,iF) -> =(iF,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 141:4:0:TAUT:: =(iT,iplus2),=(iminus6,iminus2),=(iminus2,iT) -> =(iminus6,iplus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 143:2:0:[105.0,142.2]:: =(iminus7,iF),=(iT,iminus7) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 144:1:0:TAUT:: -> =(iminus8,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 145:6:0:TAUT:: =(iminus2,iminus4),=(iplus8,iplus9),=(iminus1,iplus9),=(iF,iminus1),=(iminus4,iF) -> =(iplus8,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 146:4:0:TAUT:: =(iminus2,iminus8),=(iF,iminus9),=(iminus2,iF) -> =(iminus9,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 148:5:0:[105.0,147.5]:: =(iminus4,iF),=(iT,iplus1),=(iminus3,iplus1),=(iplus7,iminus3),=(iminus4,iplus7) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 149:3:0:TAUT:: =(iplus4,iminus5),=(iplus4,iminus3) -> =(iminus3,iminus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 150:3:0:TAUT:: =(iplus9,iminus9),=(iT,iminus9) -> =(iT,iplus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 151:3:0:TAUT:: =(iminus5,iT),=(iminus5,iplus2) -> =(iplus2,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 152:1:0:TAUT:: -> =(iminus4,iminus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 153:4:0:TAUT:: =(iplus8,iF),=(iplus8,iminus4),=(iminus4,iminus1) -> =(iminus1,iF)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 154:4:0:TAUT:: =(iplus5,iminus3),=(iplus3,iplus5),=(iminus6,iplus3) -> =(iminus6,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 155:5:0:TAUT:: =(iplus8,iplus4),=(iplus4,iplus1),=(iminus2,iminus8),=(iplus1,iminus8) -> =(iminus2,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 156:2:0:TAUT:: =(iplus3,iminus1) -> =(iminus1,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 157:3:0:TAUT:: =(iminus8,iplus3),=(iplus2,iminus8) -> =(iplus2,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 159:2:0:[118.0,158.2]:: =(iT,iplus3),=(iplus3,iF) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 160:3:0:TAUT:: =(iminus8,iplus9),=(iminus4,iplus9) -> =(iminus4,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 161:3:0:TAUT:: =(iplus4,iplus2),=(iplus2,iplus3) -> =(iplus3,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 162:3:0:TAUT:: =(iplus2,iminus1),=(iT,iplus2) -> =(iminus1,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 163:3:0:TAUT:: =(iminus5,iminus1),=(iminus5,iminus7) -> =(iminus1,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 164:2:0:TAUT:: =(iplus8,iplus3) -> =(iplus3,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 165:4:0:TAUT:: =(iplus5,iplus1),=(iT,iplus7),=(iplus1,iT) -> =(iplus7,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 166:3:0:TAUT:: =(iminus9,iminus4),=(iminus1,iminus4) -> =(iminus1,iminus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 167:3:0:TAUT:: =(iplus3,iT),=(iT,iplus4) -> =(iplus4,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 168:3:0:TAUT:: =(iplus9,iplus2),=(iplus9,iF) -> =(iplus2,iF)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 169:3:0:TAUT:: =(iminus3,iminus2),=(iminus7,iminus2) -> =(iminus3,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 170:3:0:TAUT:: =(iminus4,iminus3),=(iplus3,iminus3) -> =(iplus3,iminus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 171:4:0:TAUT:: =(iminus2,iminus1),=(iF,iminus1),=(iplus1,iF) -> =(iminus2,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 172:3:0:TAUT:: =(iF,iminus8),=(iplus9,iF) -> =(iminus8,iplus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 173:4:0:TAUT:: =(iminus7,iminus5),=(iminus6,iminus5),=(iminus6,iminus8) -> =(iminus8,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 174:4:0:TAUT:: =(iplus6,iminus5),=(iplus5,iplus6),=(iplus3,iplus5) -> =(iplus3,iminus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 175:3:0:TAUT:: =(iplus8,iplus3),=(iplus8,iminus5) -> =(iminus5,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 176:1:0:TAUT:: -> =(iplus9,iplus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 177:5:0:TAUT:: =(iplus5,iT),=(iplus5,iminus9),=(iminus9,iminus4),=(iminus4,iplus8) -> =(iplus8,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 178:1:0:TAUT:: -> =(iplus4,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 179:3:0:TAUT:: =(iminus6,iminus9),=(iminus1,iminus6) -> =(iminus1,iminus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 180:3:0:TAUT:: =(iT,iplus7),=(iT,iminus9) -> =(iminus9,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 181:4:0:TAUT:: =(iplus4,iplus7),=(iminus9,iplus7),=(iminus4,iminus9) -> =(iminus4,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 182:4:0:TAUT:: =(iT,iminus1),=(iplus5,iT),=(iplus5,iminus9) -> =(iminus9,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 183:4:0:TAUT:: =(iplus1,iplus5),=(iplus4,iF),=(iplus1,iplus4) -> =(iF,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 184:4:0:TAUT:: =(iplus7,iplus2),=(iminus9,iminus5),=(iminus5,iplus2) -> =(iminus9,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 185:4:0:TAUT:: =(iplus8,iminus5),=(iminus5,iplus1),=(iplus9,iplus1) -> =(iplus9,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 186:2:0:TAUT:: =(iplus6,iplus2) -> =(iplus2,iplus6)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 187:3:0:TAUT:: =(iminus9,iplus5),=(iminus9,iplus8) -> =(iplus8,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 188:2:0:TAUT:: =(iminus8,iminus4) -> =(iminus4,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 189:5:0:TAUT:: =(iplus6,iplus1),=(iF,iplus6),=(iminus1,iF),=(iminus8,iminus1) -> =(iminus8,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 190:4:0:TAUT:: =(iplus1,iminus2),=(iplus1,iplus9),=(iplus4,iplus9) -> =(iplus4,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 191:6:0:TAUT:: =(iplus7,iplus8),=(iplus3,iplus8),=(iplus3,iminus3),=(iminus4,iminus3),=(iminus4,iF) -> =(iF,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 192:3:0:TAUT:: =(iminus5,iplus5),=(iminus6,iminus5) -> =(iminus6,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 193:5:0:TAUT:: =(iminus7,iF),=(iplus8,iF),=(iminus1,iplus8),=(iminus8,iminus1) -> =(iminus7,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 194:3:0:TAUT:: =(iplus5,iplus7),=(iminus3,iplus5) -> =(iminus3,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 195:6:0:TAUT:: =(iplus8,iminus3),=(iminus3,iplus6),=(iplus6,iminus5),=(iminus5,iminus9),=(iminus9,iT) -> =(iT,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 196:2:0:TAUT:: =(iplus1,iminus3) -> =(iminus3,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 197:5:0:TAUT:: =(iminus6,iminus5),=(iminus3,iplus5),=(iplus5,iplus8),=(iminus6,iplus8) -> =(iminus3,iminus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 198:6:0:TAUT:: =(iplus4,iplus8),=(iplus4,iminus9),=(iplus7,iminus9),=(iminus8,iplus7),=(iminus2,iminus8) -> =(iminus2,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 199:3:0:TAUT:: =(iminus6,iminus8),=(iplus9,iminus6) -> =(iminus8,iplus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 200:9:0:TAUT:: =(iminus7,iminus5),=(iminus5,iminus1),=(iminus3,iminus1),=(iminus3,iminus2),=(iminus8,iplus7),=(iplus7,iF),=(iminus4,iF),=(iminus2,iminus4) -> =(iminus8,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 201:2:0:TAUT:: =(iminus5,iminus3) -> =(iminus3,iminus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 202:4:0:TAUT:: =(iplus5,iminus3),=(iplus5,iplus7),=(iplus7,iT) -> =(iT,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 203:4:0:TAUT:: =(iplus8,iplus6),=(iminus2,iF),=(iplus6,iF) -> =(iminus2,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 204:4:0:TAUT:: =(iminus5,iminus3),=(iplus2,iminus3),=(iplus9,iplus2) -> =(iminus5,iplus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 205:3:0:TAUT:: =(iplus7,iF),=(iplus7,iplus2) -> =(iplus2,iF)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 206:3:0:TAUT:: =(iminus5,iplus8),=(iminus5,iminus4) -> =(iplus8,iminus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 208:2:0:[105.0,207.2]:: =(iplus1,iF),=(iplus1,iT) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 209:7:0:TAUT:: =(iplus3,iplus4),=(iplus3,iminus6),=(iminus6,iminus1),=(iminus5,iminus1),=(iplus1,iminus3),=(iminus5,iminus3) -> =(iplus1,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 210:6:0:TAUT:: =(iminus5,iminus3),=(iplus5,iT),=(iT,iplus4),=(iplus4,iminus4),=(iminus4,iminus5) -> =(iplus5,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 211:4:0:TAUT:: =(iplus3,iminus8),=(iplus8,iplus9),=(iplus9,iminus8) -> =(iplus8,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 212:3:0:TAUT:: =(iminus4,iminus5),=(iminus5,iplus5) -> =(iminus4,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 213:5:0:TAUT:: =(iminus6,iF),=(iminus1,iminus6),=(iplus5,iT),=(iminus1,iT) -> =(iplus5,iF)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 214:3:0:TAUT:: =(iplus7,iplus5),=(iplus2,iplus5) -> =(iplus2,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 215:5:0:TAUT:: =(iminus4,iminus6),=(iminus8,iplus6),=(iplus8,iplus6),=(iplus8,iminus4) -> =(iminus8,iminus6)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 216:2:0:TAUT:: =(iplus7,iminus3) -> =(iminus3,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 217:7:2:[10.2,4.1,4.1,8.2,5.3,4.2,59.2,5.1,8.2,5.1]:TopTop: cTorF(x0),xsd_integer(x0),=(iplus3,x1),xsd_string(x1),xsd_string(iT) -> xsd_string(iminus8),xsd_string(iplus7)
% 13.58/3.26 === CC is in false state. New clause to be learned: 218:5:0:TAUT:: =(iplus5,iminus9),=(iplus3,iT),=(iminus2,iplus3),=(iminus2,iplus5) -> =(iT,iminus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 219:6:0:TAUT:: =(iplus8,iminus4),=(iplus8,iminus6),=(iT,iminus6),=(iT,iminus8),=(iminus8,iplus3) -> =(iplus3,iminus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 220:4:0:TAUT:: =(iminus7,iminus5),=(iminus5,iminus9),=(iT,iminus9) -> =(iT,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 221:6:0:TAUT:: =(iplus4,iminus1),=(iplus3,iminus1),=(iT,iplus3),=(iplus1,iminus9),=(iminus9,iT) -> =(iplus1,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 222:3:0:TAUT:: =(iF,iminus9),=(iplus3,iminus9) -> =(iplus3,iF)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 223:4:0:TAUT:: =(iminus3,iminus7),=(iplus8,iminus9),=(iminus3,iplus8) -> =(iminus9,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 224:4:0:[10.1,20.2,4.1,59.3,4.1]:: xsd_integer(iT) -> xsd_integer(iplus3),=(iT,iminus3),xsd_integer(iminus8)
% 13.58/3.26 === CC is in false state. New clause to be learned: 225:3:0:TAUT:: =(iminus3,iplus2),=(iplus2,iminus7) -> =(iminus7,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 226:3:0:TAUT:: =(iminus1,iplus1),=(iplus9,iplus1) -> =(iplus9,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 227:4:0:TAUT:: =(iminus4,iminus1),=(iminus4,iminus8),=(iT,iminus8) -> =(iminus1,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 228:1:0:TAUT:: -> =(iminus3,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 229:6:0:TAUT:: =(iT,iplus7),=(iminus3,iF),=(iminus3,iminus7),=(iminus7,iminus8),=(iT,iminus8) -> =(iF,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 230:7:1:[54.3,4.1,4.1,8.2,8.2,5.3,19.3,5.1,5.3,28.3,5.1,9.2,4.1]:Top: cTorF(iminus2),cTorF(x0),xsd_integer(iT) -> xsd_string(iplus7),xsd_string(iplus2),xsd_integer(x0),xsd_integer(iminus3)
% 13.58/3.26 === CC is in false state. New clause to be learned: 231:4:0:TAUT:: =(iT,iminus7),=(iminus2,iplus7),=(iT,iplus7) -> =(iminus2,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 232:4:0:TAUT:: =(iminus3,iminus2),=(iminus2,iplus7),=(iT,iplus7) -> =(iT,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 233:6:0:TAUT:: =(iminus3,iplus8),=(iminus3,iplus2),=(iplus7,iplus2),=(iT,iplus7),=(iT,iminus8) -> =(iminus8,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 234:3:0:TAUT:: =(iminus5,iminus7),=(iminus5,iT) -> =(iT,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 235:6:1:[19.3,5.1,5.1,9.2,8.1,4.3,54.3,4.1]:Top: cTorF(x0),xsd_integer(iT) -> xsd_string(iplus7),xsd_integer(x0),=(iT,iminus3),xsd_integer(iminus2)
% 13.58/3.26 === CC is in false state. New clause to be learned: 236:3:0:TAUT:: =(iminus2,iplus7),=(iT,iplus7) -> =(iT,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 237:4:0:TAUT:: =(iminus2,iplus7),=(iplus7,iplus3),=(iT,iplus3) -> =(iT,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 238:3:0:TAUT:: =(iminus2,iplus7),=(iminus2,iplus3) -> =(iplus3,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 239:4:0:TAUT:: =(iT,iminus1),=(iminus6,iplus1),=(iT,iplus1) -> =(iminus6,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 240:3:0:TAUT:: =(iT,iplus2),=(iminus3,iplus2) -> =(iT,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 241:4:1:[10.2,5.1,5.1,20.2,8.1]:Top: xsd_string(x0),=(x0,iplus7),xsd_integer(iplus3) -> xsd_string(iminus3)
% 13.58/3.26 === CC is in false state. New clause to be learned: 242:7:0:TAUT:: =(iminus2,iminus3),=(iminus6,iminus8),=(iT,iminus8),=(iT,iminus1),=(iF,iminus1),=(iminus2,iF) -> =(iminus6,iminus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 243:3:0:TAUT:: =(iminus2,iplus6),=(iminus2,iplus7) -> =(iplus7,iplus6)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 244:3:0:TAUT:: =(iT,iminus7),=(iT,iplus5) -> =(iplus5,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 245:4:0:TAUT:: =(iT,iplus3),=(iminus2,iplus3),=(iminus2,iplus7) -> =(iT,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 246:7:0:TAUT:: =(iplus5,iplus7),=(iminus2,iplus7),=(iminus2,iF),=(iplus1,iF),=(iplus1,iminus8),=(iT,iminus8) -> =(iT,iplus5)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Conflict found: 245:4:0:TAUT:: =(iT,iplus3),=(iminus2,iplus3),=(iminus2,iplus7) -> =(iT,iplus7) {}
% 13.58/3.26 === Backtracking. Learning clause 247:3:0:[245.1,63.3,236.2]:: =(iminus2,iplus3),=(iminus2,iplus7) -> =(iT,iminus2)
% 13.58/3.26 === Backtracking. Learning clause 249:9:1:[5.0,248.8,4.1,31.2,8.2,5.3,157.2,10.3,5.1,5.3,68.1,5.1]:Top: xsd_integer(iplus2),cTorF(iplus2),cTorF(iminus8),=(x0,iminus8),xsd_string(x0),xsd_string(iT) -> =(iplus2,iplus3),xsd_string(iminus3),xsd_string(iplus6)
% 13.58/3.26 === CC is in false state. New clause to be learned: 250:9:0:TAUT:: =(iT,iminus9),=(iT,iminus2),=(iminus2,iplus7),=(iminus3,iplus2),=(iminus3,iminus7),=(iminus7,iplus9),=(iplus9,iminus4),=(iminus4,iplus7) -> =(iplus2,iminus9)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 251:5:0:TAUT:: =(iplus4,iplus2),=(iT,iplus2),=(iT,iminus8),=(iminus8,iplus3) -> =(iplus3,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 252:3:0:[30.1,110.1,19.1,5.1,9.2]:: -> =(iminus2,iplus7),xsd_string(iminus7),xsd_integer(iminus2)
% 13.58/3.26 === CC is in false state. New clause to be learned: 253:4:0:TAUT:: =(iT,iplus7),=(iminus2,iminus7),=(iT,iminus7) -> =(iminus2,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 254:5:0:TAUT:: =(iplus1,iminus2),=(iminus2,iminus6),=(iT,iminus6),=(iT,iplus6) -> =(iplus6,iplus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 256:7:3:[36.1,255.1,50.2,4.1,4.1,8.2,8.2,5.3,13.2,5.1,5.2,5.3,5.3]:TopTopTop: xsd_integer(iT),=(iplus1,x0),=(x1,iminus9),=(x2,x1),xsd_string(x2) -> =(iT,iplus7),xsd_string(x0)
% 13.58/3.26 === CC is in false state. New clause to be learned: 257:2:0:TAUT:: =(iT,iminus1) -> =(iminus1,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 258:6:0:TAUT:: =(iminus2,iplus7),=(iminus2,iminus3),=(iminus3,iplus1),=(iT,iplus1),=(iT,iplus3) -> =(iplus3,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 259:3:0:TAUT:: =(iminus2,iminus3),=(iminus2,iplus7) -> =(iminus3,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 260:5:0:TAUT:: =(iminus2,iplus7),=(iminus2,iminus8),=(iT,iminus8),=(iT,iplus3) -> =(iplus3,iplus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 261:3:0:TAUT:: =(iT,iminus9),=(iT,iplus3) -> =(iminus9,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 262:5:1:[74.1,4.1,4.1,4.3,9.1]:Top: =(x0,iT) -> =(iT,iplus7),xsd_integer(iminus5),xsd_integer(iplus4),xsd_string(x0)
% 13.58/3.26 === CC is in false state. New clause to be learned: 263:5:0:TAUT:: =(iT,iminus8),=(iminus2,iplus7),=(iplus7,iminus1),=(iT,iminus1) -> =(iminus2,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 264:5:0:TAUT:: =(iminus2,iminus3),=(iminus3,iplus1),=(iplus1,iminus8),=(iT,iminus8) -> =(iminus2,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 265:4:0:TAUT:: =(iminus8,iplus4),=(iT,iminus8),=(iT,iminus9) -> =(iminus9,iplus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 266:4:0:TAUT:: =(iplus3,iminus1),=(iT,iplus4),=(iT,iplus3) -> =(iplus4,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 267:5:0:TAUT:: =(iT,iminus4),=(iminus2,iminus3),=(iminus2,iplus1),=(iT,iplus1) -> =(iminus3,iminus4)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 268:4:0:TAUT:: =(iT,iminus8),=(iminus7,iminus2),=(iT,iminus7) -> =(iminus2,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 269:6:0:TAUT:: =(iminus2,iplus7),=(iminus2,iplus1),=(iplus2,iplus1),=(iT,iplus2),=(iT,iplus3) -> =(iplus7,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 270:3:0:TAUT:: =(iminus2,iplus8),=(iminus2,iF) -> =(iF,iplus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 271:4:0:TAUT:: =(iminus2,iminus3),=(iminus2,iplus9),=(iT,iplus9) -> =(iminus3,iT)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 273:4:0:[159.1,272.4]:: =(iminus2,iF),=(iminus8,iminus2),=(iT,iminus8),=(iT,iplus3) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 274:3:0:TAUT:: =(iT,iminus1),=(iT,iplus3) -> =(iplus3,iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 275:4:0:TAUT:: =(iminus2,iplus1),=(iT,iplus1),=(iT,iplus3) -> =(iminus2,iplus3)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 276:6:0:TAUT:: =(iminus2,iplus7),=(iplus7,iplus8),=(iplus8,iplus5),=(iT,iplus5),=(iT,iminus8) -> =(iminus8,iminus2)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 278:4:0:[143.0,277.4]:: =(iplus7,iF),=(iplus7,iplus9),=(iT,iplus9),=(iT,iminus7) ->
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 279:5:0:TAUT:: =(iT,iminus8),=(iminus2,iplus1),=(iminus7,iplus1),=(iT,iminus7) -> =(iminus2,iminus8)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 280:7:1:[44.3,275.2,4.1,8.2,5.3]:Top: =(iminus2,iplus1),=(iT,iplus3),xsd_integer(iT),=(x0,iminus9),xsd_string(x0) -> =(iT,iminus2),=(iminus2,iplus3)
% 13.58/3.26 === CC is in false state. New clause to be learned: 281:4:0:TAUT:: =(iT,iplus6),=(iT,iminus1),xsd_string(iplus6) -> xsd_string(iminus1)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 282:3:0:TAUT:: =(iT,iminus7),=(iT,iminus9) -> =(iminus9,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === Backtracking. Learning clause 284:6:0:[20.1,283.0,13.3,275.1,5.1,13.3,5.1,9.2,247.1,63.3,236.2]:: xsd_string(iminus2),cTorF(iT),=(iminus2,iplus7) -> xsd_string(iminus1),xsd_integer(iT),=(iT,iminus2)
% 13.58/3.26 === Backtracking. Learning clause 286:9:2:[9.0,285.1,22.2,126.1,1.3,13.2,4.1,8.2,5.3,76.2,4.1,4.3,5.1]:TopTop: cTorF(x0),xsd_string(iT),=(x1,x0),xsd_integer(x1),xsd_string(iplus6) -> =(iT,iplus2),=(iT,iminus3),xsd_integer(iplus1),xsd_string(iminus1)
% 13.58/3.26 === CC is in false state. New clause to be learned: 287:6:0:TAUT:: =(iplus8,iminus7),=(iminus3,iplus8),=(iminus3,iplus6),=(iT,iplus6),=(iT,iplus3) -> =(iplus3,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 288:4:0:TAUT:: =(iminus2,iminus7),=(iminus2,iplus3),=(iT,iplus3) -> =(iT,iminus7)
% 13.58/3.26 === Restarting.
% 13.58/3.26 === CC is in false state. New clause to be learned: 289:4:0:TAUT:: =(iminus2,iminus1),=(iT,iminus1),=(iT,iplus1) -> =(iminus2,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 290:6:2:[5.1,54.2,8.1,4.3,9.1,5.2]:TopTop: xsd_string(iT),=(x0,iminus3),=(x0,x1) -> =(iT,iminus2),=(iT,iminus7),xsd_string(x1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 291:4:0:TAUT:: =(iminus2,iminus1),=(iminus2,iminus3),=(iT,iminus3) -> =(iT,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 293:5:0:[21.1,292.0,13.2,289.1,275.1,288.2]:: =(iT,iminus1),=(iT,iplus1),=(iminus2,iminus7),=(iT,iplus3) -> =(iT,iminus7)
% 13.58/3.27 === Backtracking. Learning clause 294:4:0:[13.2,289.1]:: cTorF(iminus2),=(iT,iminus1),=(iT,iplus1) -> =(iminus2,iplus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 295:4:0:TAUT:: =(iminus2,iminus7),=(iminus2,iplus1),=(iT,iplus1) -> =(iT,iminus7)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 296:3:1:[12.2,13.1]:Top: =(x0,iplus3) -> =(x0,iminus1),=(x0,iplus1)
% 13.58/3.27 === Backtracking. Learning clause 297:2:0:[30.1,110.1,13.1]:: -> =(iminus2,iminus1),=(iminus2,iplus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 298:3:0:TAUT:: =(iT,iplus3),=(iminus2,iplus3) -> =(iT,iminus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 299:4:0:TAUT:: =(iT,iplus1),=(iT,iplus3),=(iminus2,iplus3) -> =(iminus2,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 300:5:0:TAUT:: =(iminus3,iplus9),=(iminus2,iplus9),=(iT,iplus3),=(iminus2,iplus3) -> =(iT,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 301:3:0:TAUT:: =(iplus7,iplus1),=(iT,iplus7) -> =(iT,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 303:6:0:[12.1,302.3,34.1,11.2,4.1,228.1,300.1,34.2]:: xsd_integer(iminus3),=(iT,iplus3),=(iminus2,iplus3) -> xsd_integer(iminus9),=(iT,iminus3),=(iminus2,iminus9)
% 13.58/3.27 === CC is in false state. New clause to be learned: 304:5:0:TAUT:: =(iplus1,iplus9),=(iminus3,iplus9),=(iT,iminus3),=(iT,iplus7) -> =(iplus7,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 305:4:0:TAUT:: =(iT,iplus9),=(iT,iplus3),=(iminus2,iplus3) -> =(iminus2,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Conflict found: 305:4:0:TAUT:: =(iT,iplus9),=(iT,iplus3),=(iminus2,iplus3) -> =(iminus2,iplus9) {}
% 13.58/3.27 === Backtracking. Learning clause 306:5:0:[305.1,72.1,300.2]:: =(iminus3,iplus9),=(iT,iplus3),=(iminus2,iplus3) -> =(iT,iplus1),=(iT,iminus3)
% 13.58/3.27 === CC is in false state. New clause to be learned: 307:5:0:TAUT:: =(iT,iplus9),=(iminus3,iminus9),=(iminus9,iminus5),=(iT,iminus5) -> =(iminus3,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 308:3:0:TAUT:: =(iminus2,iminus1),=(iT,iminus1) -> =(iT,iminus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 309:3:0:[83.2,308.2]:: =(iminus2,iminus1) -> =(iT,iplus3),=(iT,iminus2)
% 13.58/3.27 === CC is in false state. New clause to be learned: 310:3:0:TAUT:: =(iminus2,iplus3),=(iT,iminus2) -> =(iT,iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Conflict found: 298:3:0:TAUT:: =(iT,iplus3),=(iminus2,iplus3) -> =(iT,iminus2) {}
% 13.58/3.27 === Backtracking. Learning clause 311:3:0:[298.1,309.2]:: =(iminus2,iplus3),=(iminus2,iminus1) -> =(iT,iminus2)
% 13.58/3.27 === Backtracking. Learning clause 312:4:1:[16.2,5.1,5.1]:Top: cTorF(x0),xsd_string(x0) -> xsd_string(iplus4),xsd_string(iminus4)
% 13.58/3.27 === CC is in false state. New clause to be learned: 313:7:0:TAUT:: =(iplus4,iplus9),=(iminus3,iplus9),=(iT,iminus3),=(iminus9,iminus4),=(iplus7,iminus4),=(iT,iplus7) -> =(iminus9,iplus4)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 314:4:0:TAUT:: =(iminus2,iminus1),=(iminus2,iplus9),=(iT,iplus9) -> =(iT,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 315:3:0:TAUT:: =(iminus3,iplus9),=(iT,iplus9) -> =(iT,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Conflict found: 291:4:0:TAUT:: =(iminus2,iminus1),=(iminus2,iminus3),=(iT,iminus3) -> =(iT,iminus1) {}
% 13.58/3.27 === Backtracking. Learning clause 319:3:0:[14.1,316.1,311.0,317.3,308.1,318.5,291.2,10.2,315.3,53.2]:: =(iminus2,iminus1),=(iminus3,iplus9) -> =(iT,iminus2)
% 13.58/3.27 === Backtracking. Learning clause 320:5:0:[19.3,253.2,232.2]:: cTorF(iminus2),=(iT,iminus7),=(iminus3,iminus2),=(iT,iplus7) -> =(iT,iminus3)
% 13.58/3.27 === CC is in false state. New clause to be learned: 321:4:0:TAUT:: =(iT,iplus2),=(iminus3,iminus9),=(iT,iminus9) -> =(iminus3,iplus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Conflict found: 275:4:0:TAUT:: =(iminus2,iplus1),=(iT,iplus1),=(iT,iplus3) -> =(iminus2,iplus3) {}
% 13.58/3.27 === Backtracking. Learning clause 322:5:0:[275.2,72.3,298.2]:: =(iminus2,iplus1),=(iT,iplus3) -> =(iT,iplus9),=(iT,iminus3),=(iT,iminus2)
% 13.58/3.27 === CC is in false state. New clause to be learned: 323:3:0:TAUT:: =(iT,iplus1),=(iminus2,iplus1) -> =(iT,iminus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 324:4:0:TAUT:: =(iT,iminus1),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 325:6:0:TAUT:: =(iminus3,iplus9),=(iplus7,iplus9),=(iT,iplus7),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 326:5:2:[13.2,4.1,4.1,4.3,9.1]:TopTop: cTorF(x0),=(x1,x0) -> xsd_integer(iminus1),xsd_integer(iplus1),xsd_string(x1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 327:4:0:TAUT:: =(iT,iminus1),=(iplus9,iplus1),=(iT,iplus1) -> =(iplus9,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 328:6:0:TAUT:: =(iminus3,iplus9),=(iplus9,iplus1),=(iT,iplus1),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 329:5:0:TAUT:: =(iplus9,iplus1),=(iT,iplus1),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 330:4:2:[13.1,1.3]:TopTop: =(x0,x1),cTorF(x0) -> =(x1,iminus1),=(x1,iplus1)
% 13.58/3.27 === Backtracking. Learning clause 331:6:0:[76.1,240.1,5.1,8.1,4.3,22.3,126.1]:: =(iminus3,iplus2),xsd_string(iT),xsd_integer(iminus1),cTorF(iminus1) -> =(iT,iminus3),=(iplus6,iminus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 332:8:0:TAUT:: =(iT,iplus3),=(iplus6,iminus1),=(iplus9,iminus1),=(iminus3,iplus9),=(iminus3,iplus2),=(iplus2,iminus8),=(iT,iminus8) -> =(iplus6,iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Conflict found: 330:4:2:[13.1,1.3]:TopTop: =(x0,x1),cTorF(x0) -> =(x1,iminus1),=(x1,iplus1) {x0 -> iminus3, x1 -> iplus9}
% 13.58/3.27 === Backtracking. Learning clause 333:5:0:[330.2,35.2,329.1,300.2,306.4]:: =(iminus3,iplus9),=(iT,iplus3),=(iminus2,iplus3) -> =(iplus9,iminus1),=(iT,iminus3)
% 13.58/3.27 === CC is in false state. New clause to be learned: 334:3:0:TAUT:: =(iminus3,iplus9),=(iT,iminus3) -> =(iT,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 335:3:0:TAUT:: =(iplus9,iplus1),=(iT,iplus1) -> =(iT,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 336:6:0:[28.3,232.1,240.2,19.2]:: cTorF(iminus3),=(iT,iplus7),=(iT,iplus2),cTorF(iminus2) -> =(iT,iminus3),=(iminus2,iminus7)
% 13.58/3.27 === CC is in false state. New clause to be learned: 337:5:0:TAUT:: =(iT,iplus2),=(iminus3,iminus2),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus3,iplus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 338:5:0:TAUT:: =(iminus1,iminus6),=(iT,iminus6),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 339:5:0:TAUT:: =(iminus3,iminus9),=(iT,iminus9),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 340:1:0:TAUT:: -> =(iminus1,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 341:4:0:TAUT:: =(iminus3,iplus2),=(iminus3,iminus9),=(iT,iminus9) -> =(iT,iplus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 342:3:0:TAUT:: =(iminus3,iminus9),=(iminus2,iminus9) -> =(iminus2,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 343:4:0:TAUT:: =(iplus9,iplus1),=(iT,iminus8),=(iT,iplus1) -> =(iminus8,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 344:3:0:TAUT:: =(iT,iminus6),=(iT,iplus3) -> =(iplus3,iminus6)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 345:3:0:TAUT:: =(iminus3,iplus2),=(iplus2,iminus8) -> =(iminus8,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 346:4:0:TAUT:: =(iminus3,iminus9),=(iminus3,iplus1),=(iT,iplus1) -> =(iT,iminus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 347:3:0:[10.2,5.1,18.2,5.1,152.1]:: xsd_string(iminus4) -> xsd_string(iminus3),xsd_string(iplus3)
% 13.58/3.27 === Backtracking. Learning clause 348:2:0:[14.1,340.1,22.1,126.1]:: -> =(iminus1,iminus6),=(iplus6,iminus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 349:4:0:TAUT:: =(iT,iminus8),=(iT,iplus1),=(iplus9,iplus1) -> =(iplus9,iminus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 351:8:0:[12.1,350.0,11.1,228.1,336.1,76.1,338.2,314.1,245.4,305.4]:: =(iminus1,iminus6),=(iminus2,iplus7),=(iT,iplus9),=(iT,iplus3),=(iminus2,iplus3) -> =(iminus2,iminus7),=(iT,iminus3),=(iT,iminus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 352:5:0:TAUT:: =(iT,iplus3),=(iT,iplus1),=(iminus2,iplus9),=(iplus9,iplus1) -> =(iminus2,iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 353:4:0:TAUT:: =(iminus2,iplus1),=(iT,iplus9),=(iminus2,iplus9) -> =(iT,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 354:5:0:[72.1,353.2,323.1,330.4,309.1,310.2,337.4,28.3,240.2,76.1]:: =(iminus2,iplus9),=(iminus2,iplus3),cTorF(iminus3) -> =(iT,iminus6),=(iT,iminus3)
% 13.58/3.27 === Backtracking. Learning clause 355:5:0:[28.3,337.2,240.2]:: cTorF(iminus3),=(iminus2,iplus3),=(iT,iplus3),=(iT,iplus2) -> =(iT,iminus3)
% 13.58/3.27 === CC is in false state. New clause to be learned: 356:4:0:TAUT:: =(iminus3,iminus2),=(iT,iplus1),=(iminus2,iplus1) -> =(iT,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 357:5:0:TAUT:: =(iminus2,iplus9),=(iminus3,iminus2),=(iminus3,iplus2),=(iT,iplus2) -> =(iT,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 358:11:4:[31.2,5.1,5.1,5.2,347.1,5.2,8.1,4.3,51.1,4.1,5.2,4.3,9.1]:TopTopTopTop: cTorF(x0),xsd_string(x0),=(iminus8,iminus4),=(iplus3,x1),=(x1,x2),=(x3,iT) -> xsd_string(iminus3),=(iT,iminus7),xsd_integer(iplus4),xsd_string(x2),xsd_string(x3)
% 13.58/3.27 === Backtracking. Learning clause 359:5:2:[28.2,4.1,4.1,8.2,5.3]:TopTop: cTorF(x0),xsd_integer(x0),=(x1,iplus2),xsd_string(x1) -> xsd_integer(iminus2)
% 13.58/3.27 === CC is in false state. New clause to be learned: 360:3:0:TAUT:: =(iplus8,iplus2),=(iT,iplus2) -> =(iT,iplus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 361:5:0:TAUT:: =(iT,iplus3),=(iT,iplus2),=(iminus3,iplus2),xsd_string(iplus3) -> xsd_string(iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 362:7:0:TAUT:: =(iminus1,iplus6),=(iT,iplus6),=(iT,iplus2),=(iminus3,iplus2),=(iminus2,iplus9),=(iminus3,iminus2) -> =(iplus9,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 363:7:0:[22.1,29.2,362.2]:: =(iminus1,iplus6),=(iT,iplus2),=(iminus3,iplus2),=(iminus2,iplus9),=(iminus3,iminus2) -> =(iT,iminus6),=(iplus9,iminus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 364:6:0:TAUT:: =(iplus9,iminus1),=(iminus2,iplus9),=(iminus3,iminus2),=(iminus3,iplus2),=(iT,iplus2) -> =(iT,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 365:7:0:TAUT:: =(iT,iplus1),=(iT,iplus2),=(iminus3,iplus2),=(iminus1,iminus6),=(iminus6,iminus2),=(iminus3,iminus2) -> =(iminus1,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 366:4:0:TAUT:: =(iminus3,iminus2),=(iminus6,iplus2),=(iminus3,iplus2) -> =(iminus6,iminus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 367:6:0:TAUT:: =(iminus7,iplus9),=(iminus2,iplus9),=(iminus3,iminus2),=(iT,iplus2),=(iminus3,iplus2) -> =(iT,iminus7)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 368:4:0:TAUT:: =(iplus1,iminus1),=(iT,iplus1),=(iT,iplus6) -> =(iplus6,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 370:7:0:[15.1,369.1,28.2,366.2,365.5,226.1,1.3,22.3,14.2,340.1,330.4,362.1,357.5]:: =(iT,iplus1),=(iT,iplus6),=(iminus2,iplus9),=(iminus3,iminus2),=(iminus3,iplus2),=(iT,iplus2) -> =(iplus9,iminus1)
% 13.58/3.27 === CC is in false state. New clause to be learned: 371:6:0:TAUT:: =(iminus1,iplus6),=(iT,iplus6),=(iminus3,iminus2),=(iminus3,iplus2),=(iT,iplus2) -> =(iminus2,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 372:5:0:TAUT:: =(iplus9,iplus1),=(iminus2,iplus9),=(iminus3,iminus2),=(iT,iminus3) -> =(iT,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 373:5:0:TAUT:: =(iminus1,iplus6),=(iT,iplus6),=(iminus2,iplus3),=(iT,iplus3) -> =(iminus2,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 374:4:0:TAUT:: =(iminus1,iminus6),=(iminus1,iplus6),=(iT,iplus6) -> =(iT,iminus6)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 375:4:0:TAUT:: =(iT,iplus7),=(iminus2,iminus3),=(iT,iminus3) -> =(iminus2,iplus7)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 376:5:0:[10.2,375.2,35.2,236.1]:: =(iT,iminus3),=(iminus2,iplus9),=(iT,iplus7) -> =(iminus2,iplus3),=(iT,iminus2)
% 13.58/3.27 === CC is in false state. New clause to be learned: 377:3:0:TAUT:: =(iT,iplus3),=(iT,iminus2) -> =(iminus2,iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 378:3:0:TAUT:: =(iminus2,iminus3),=(iminus2,iplus9) -> =(iminus3,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 379:3:0:TAUT:: =(iT,iplus7),=(iT,iminus5) -> =(iminus5,iplus7)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 380:6:0:TAUT:: =(iT,iminus3),=(iT,iplus7),=(iplus7,iminus6),=(iminus4,iminus6),=(iminus4,iplus3) -> =(iminus3,iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 381:3:0:TAUT:: =(iminus6,iF),=(iminus8,iminus6) -> =(iF,iminus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 382:5:0:TAUT:: =(iminus2,iminus7),=(iminus5,iminus2),=(iT,iminus5),=(iT,iminus9) -> =(iminus9,iminus7)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 383:4:0:TAUT:: =(iminus2,iplus3),=(iminus2,iplus9),xsd_integer(iplus9) -> xsd_integer(iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 384:5:0:TAUT:: =(iplus5,iplus4),=(iminus9,iplus4),=(iT,iminus9),=(iT,iplus2) -> =(iplus5,iplus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 385:2:0:TAUT:: =(iplus2,iplus1) -> =(iplus1,iplus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 386:5:0:TAUT:: =(iT,iplus6),=(iT,iplus2),=(iminus2,iplus9),=(iplus9,iplus2) -> =(iminus2,iplus6)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 387:7:0:TAUT:: =(iT,iminus3),=(iT,iplus2),=(iminus4,iplus3),=(iminus2,iplus3),=(iminus2,iplus9),=(iplus9,iplus2) -> =(iminus4,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 388:4:0:TAUT:: =(iT,iminus3),=(iminus4,iminus9),=(iT,iminus9) -> =(iminus4,iminus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 389:10:0:TAUT:: =(iminus9,iplus5),=(iT,iminus9),=(iplus1,iminus8),=(iplus9,iplus1),=(iminus2,iplus9),=(iminus2,iminus7),=(iminus6,iminus7),=(iminus6,iminus5),=(iT,iminus5) -> =(iminus8,iplus5)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 390:7:4:[31.3,5.1,5.1,9.2,4.2,8.2,5.2,8.1,4.3]:TopTopTopTop: cTorF(x0),=(x0,x1),xsd_string(x1),=(iminus8,x2),=(x3,x2),xsd_integer(x3) -> xsd_string(iplus8)
% 13.58/3.27 === CC is in false state. New clause to be learned: 391:3:0:TAUT:: =(iT,iminus5),=(iT,iplus2) -> =(iplus2,iminus5)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 392:5:0:TAUT:: =(iT,iminus9),=(iminus2,iplus9),=(iminus2,iplus8),=(iT,iplus8) -> =(iplus9,iminus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 393:5:0:TAUT:: =(iminus4,iplus7),=(iT,iplus7),=(iT,iplus8),xsd_string(iminus4) -> xsd_string(iplus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 394:3:0:TAUT:: =(iminus2,iplus3),=(iminus2,iminus8) -> =(iminus8,iplus3)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 395:3:0:TAUT:: =(iminus1,iplus6),=(iplus6,iminus8) -> =(iminus8,iminus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 396:4:0:TAUT:: =(iplus9,iminus5),=(iT,iminus5),=(iT,iplus7) -> =(iplus7,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 397:3:0:TAUT:: =(iminus2,iplus3),=(iminus2,iplus9) -> =(iplus3,iplus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 398:6:0:TAUT:: =(iminus2,iplus3),=(iminus4,iplus3),=(iminus4,iminus5),=(iT,iminus5),=(iT,iplus7) -> =(iplus7,iminus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 399:7:0:TAUT:: =(iT,iminus5),=(iminus2,iplus3),=(iminus2,iminus8),=(iminus8,iplus5),=(iplus5,iminus9),=(iT,iminus9) -> =(iplus3,iminus5)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 400:4:0:TAUT:: =(iT,iminus9),=(iminus5,iminus2),=(iT,iminus5) -> =(iminus2,iminus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 402:2:0:[105.0,401.2]:: =(iplus4,iF),=(iT,iplus4) ->
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Backtracking. Learning clause 403:8:2:[5.1,25.3,5.3,8.1,396.1,4.3]:TopTop: cTorF(iplus9),=(x0,iplus9),xsd_string(x0),=(iT,iminus5),=(iT,iplus7),=(x1,iplus5),xsd_integer(x1) -> =(iplus7,iplus9)
% 13.58/3.27 === CC is in false state. New clause to be learned: 404:4:0:TAUT:: =(iminus2,iminus7),=(iminus2,iplus9),=(iplus9,iplus1) -> =(iplus1,iminus7)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 405:3:0:TAUT:: =(iminus2,iminus8),=(iminus2,iplus9) -> =(iplus9,iminus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 406:2:0:TAUT:: =(iT,iplus8) -> =(iplus8,iT)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 407:4:0:TAUT:: =(iT,iminus9),=(iminus2,iplus8),=(iT,iplus8) -> =(iminus2,iminus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 408:3:0:TAUT:: =(iT,iminus5),=(iT,iplus8) -> =(iplus8,iminus5)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 409:3:0:TAUT:: =(iminus2,iminus8),xsd_string(iminus8) -> xsd_string(iminus2)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 410:4:0:TAUT:: =(iplus9,iF),=(iminus2,iminus8),=(iminus2,iplus9) -> =(iminus8,iF)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 411:5:0:TAUT:: =(iminus9,iminus4),=(iT,iminus9),=(iT,iplus8),xsd_string(iminus4) -> xsd_string(iplus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 412:7:0:TAUT:: =(iplus9,iplus1),=(iminus2,iplus9),=(iminus2,iplus8),=(iT,iplus8),=(iminus1,iplus6),=(iT,iplus6) -> =(iminus1,iplus1)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 413:5:0:TAUT:: =(iplus3,iF),=(iminus2,iplus3),=(iminus2,iplus9),=(iplus9,iplus5) -> =(iplus5,iF)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === Conflict found: 379:3:0:TAUT:: =(iT,iplus7),=(iT,iminus5) -> =(iminus5,iplus7) {}
% 13.58/3.27 === Backtracking. Learning clause 415:3:0:[63.1,414.0,379.2,79.1]:: -> =(iminus5,iplus7),=(iT,iminus2),=(iT,iplus3)
% 13.58/3.27 === CC is in false state. New clause to be learned: 416:5:0:TAUT:: =(iplus7,iminus6),=(iT,iplus7),=(iminus1,iplus6),=(iT,iplus6) -> =(iminus1,iminus6)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 417:5:0:TAUT:: =(iplus6,iminus4),=(iT,iplus6),=(iT,iplus8),xsd_string(iminus4) -> xsd_string(iplus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 418:3:0:TAUT:: =(iT,iminus9),=(iT,iplus8) -> =(iplus8,iminus9)
% 13.58/3.27 === Restarting.
% 13.58/3.27 === CC is in false state. New clause to be learned: 419:6:0:TAUT:: =(iminus2,iminus8),=(iminus2,iplus3),=(iminus4,iplus3),=(iminus4,iplus6),=(iminus1,iplus6) -> =(iminus1,iminus8)
% 13.58/3.27 === Restarting.
% 13.58/3.27
% 13.58/3.27 Linear Model Building succeeded.
% 13.58/3.27 SZS status Satisfiable
% 13.58/3.27
% 13.58/3.27 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.58/3.27
% 13.58/3.27 SPASS-SCL-FOL Statistics:
% 13.58/3.27 Number of learned clauses: 44
% 13.58/3.27 Number of propagations: 24277
% 13.58/3.27 Number of decisions: 2956
% 13.58/3.27 Number of resolutions: 205
% 13.58/3.27 Number of condensations: 1
% 13.58/3.27 Number of sub resolutions: 21
% 13.58/3.27 Number of input literals (deduplicated): 45
% 13.58/3.27 Number of grows: 0
% 13.58/3.27 Number of considered ground atoms: 500
% 13.58/3.27
% 13.58/3.27 Needed: 0:00:02.67
% 13.58/3.27
%------------------------------------------------------------------------------