%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : KRS138+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 : n010.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:24 PM UTC 2026
% Result : Theorem 0.64s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS138+1 : TPTP v9.2.1. Released v3.1.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n010.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 12:19:37 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.18/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.64/0.69 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.69 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.69 Execution normal ended with status: unsatisfiable
% 0.64/0.69 Used heuristic: normal
% 0.64/0.69
% 0.64/0.69 Input Clauses:
% 0.64/0.69
% 0.64/0.69 Predicates: = cA cowlNothing cowlThing requalityOnA xsd_integer xsd_string ren1 ren2 ren3
% 0.64/0.69 Fol Constants: ib ia ic skc1 skc2 skc3 skc4 skc5 skc6 skc7
% 0.64/0.69 Fol Functions:
% 0.64/0.69 Problem Properties:
% 0.64/0.69 This is a Bernays Schoenfinkel Ramsey problem.
% 0.64/0.69
% 0.64/0.69
% 0.64/0.69 Reduced Input Clauses:
% 0.64/0.69 40:3:0:[8.0,32.0,8.0,35.4,18.0,36.5,8.0,37.6,8.0,38.7,9.0,39.8]:: ren1(skc3),ren2(skc4,skc5),ren3(skc6,skc7) ->
% 0.64/0.69 33:2:1:[11.1,24.0]:Top: -> xsd_integer(x0),ren1(x0)
% 0.64/0.69 34:2:1:[11.0,25.0]:Top: -> xsd_string(x0),ren1(x0)
% 0.64/0.69
% 0.64/0.69 Most General Atoms: cA(x1) requalityOnA(x2,x1) xsd_integer(x1) xsd_string(x1) cowlThing(x0) cowlNothing(x0) =(x0,x2) ren3(x0,x1) ren2(x0,x1) ren1(x0)
% 0.64/0.69
% 0.64/0.69 === Starting SPASS-SCL-FOL A Little Less Naive, considering 460 atoms initially, heuristics mode: normal ===
% 0.64/0.69
% 0.64/0.69 === CC is in false state. New clause to be learned: 42:2:0:[18.0,41.1]:: =(skc3,ia) -> requalityOnA(ia,skc3)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === Backtracking. Learning clause 43:6:5:[12.3,5.1,5.1,15.2,5.1,16.2,15.2,5.1,15.2,15.2,26.1,27.1,28.1]:TopTopTopTopTop: requalityOnA(x0,x1),requalityOnA(x2,ib),requalityOnA(ib,x2),requalityOnA(x3,ia),requalityOnA(ia,x3) -> ren2(x4,x0)
% 0.64/0.69 === CC is in false state. New clause to be learned: 44:4:0:TAUT:: =(ia,skc7),=(ib,skc7),=(skc5,ib) -> =(skc5,ia)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 45:4:0:TAUT:: =(skc7,ia),=(skc2,ia),ren3(ia,ia) -> ren3(skc2,skc7)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 47:3:0:[18.0,46.2]:: =(ia,skc7),=(skc2,ia) -> requalityOnA(skc2,skc7)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 49:2:0:[18.0,48.1]:: =(skc7,ia) -> requalityOnA(skc7,ia)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === Backtracking. Learning clause 52:1:2:[18.0,50.0,20.0,51.1,12.2,5.1,5.1,15.1,15.1,28.1,16.2,26.1,27.1]:TopTop: -> ren2(x0,x1)
% 0.64/0.69 === CC is in false state. New clause to be learned: 53:4:0:TAUT:: =(skc1,ib),=(skc2,ib),=(skc2,ia) -> =(ia,skc1)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 54:4:0:TAUT:: =(skc1,ib),=(skc7,ia),=(skc1,ia) -> =(skc7,ib)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 55:4:0:TAUT:: =(skc1,ia),=(skc2,ib),=(skc2,ia) -> =(ib,skc1)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 56:3:0:TAUT:: =(skc7,ib),=(skc5,skc7) -> =(ib,skc5)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 57:3:0:TAUT:: =(skc3,ib),=(ib,skc7) -> =(skc7,skc3)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 58:4:0:TAUT:: =(skc2,ib),=(skc2,skc6),ren3(ib,ib) -> ren3(skc6,ib)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === Backtracking. Learning clause 59:4:4:[15.2,30.1,5.1,31.1]:TopTopTopTop: requalityOnA(x0,x1),requalityOnA(x2,x0) -> ren3(x3,x1),ren3(x3,x2)
% 0.64/0.69 === Backtracking. Learning clause 60:3:1:[10.1,34.1,33.1,40.1,59.3,52.1,49.2,12.3,16.2,5.1]:Top: requalityOnA(ia,skc7),requalityOnA(x0,skc7) -> requalityOnA(x0,ib)
% 0.64/0.69 === CC is in false state. New clause to be learned: 62:2:0:[20.0,61.1]:: =(skc7,ib) -> requalityOnA(skc7,skc7)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 63:3:0:TAUT:: =(skc7,ib),requalityOnA(ib,ia) -> requalityOnA(skc7,ia)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === Backtracking. Learning clause 65:2:1:[52.0,64.0,10.2,33.1,34.1,40.1,59.3]:Top: requalityOnA(x0,skc7),requalityOnA(skc7,x0) ->
% 0.64/0.69 === CC is in false state. New clause to be learned: 67:2:0:[20.0,66.1]:: =(skc7,ib) -> requalityOnA(skc7,ib)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === CC is in false state. New clause to be learned: 69:2:0:[67.1,68.1]:: =(skc7,ib) -> requalityOnA(ib,skc7)
% 0.64/0.69 === Restarting.
% 0.64/0.69 === Conflict found: 65:2:1:[52.0,64.0,10.2,33.1,34.1,40.1,59.3]:Top: requalityOnA(x0,skc7),requalityOnA(skc7,x0) -> {x0 -> ib}
% 0.64/0.69 === Backtracking. Learning clause 70:1:0:[65.2,67.2,69.2,12.2,49.1,16.2,65.2]:: requalityOnA(ia,skc7) ->
% 0.64/0.69 === Conflict found: 65:2:1:[52.0,64.0,10.2,33.1,34.1,40.1,59.3]:Top: requalityOnA(x0,skc7),requalityOnA(skc7,x0) -> {x0 -> ib}
% 0.64/0.69 === Backtracking. Learning clause 71:1:0:[65.2,67.2,69.2]:: =(skc7,ib) ->
% 0.64/0.69 === Backtracking. Learning clause 73:2:0:[52.0,72.0,30.1,16.1,40.3,34.2]:: -> cA(skc7),xsd_string(skc3)
% 0.64/0.69 === Conflict found: 40:3:0:[8.0,32.0,8.0,35.4,18.0,36.5,8.0,37.6,8.0,38.7,9.0,39.8]:: ren1(skc3),ren2(skc4,skc5),ren3(skc6,skc7) -> {}
% 0.64/0.69 === Backtracking. Learning clause 74:2:0:[40.2,52.1]:: ren1(skc3),ren3(skc6,skc7) ->
% 0.64/0.69 === Backtracking. Learning clause 76:1:0:[71.0,75.0,30.1,16.1,74.2,33.2,10.2,73.2,12.1,49.1]:: -> requalityOnA(skc7,ia)
% 0.64/0.69 === Backtracking. Learning clause 77:1:0:[10.2,33.1,34.1,74.1]:: ren3(skc6,skc7) ->
% 0.64/0.69 === CC is in false state. New clause to be learned: 80:1:0:[49.1,78.1,70.0,79.2]:: =(skc7,ia) ->
% 0.64/0.69 === Restarting.
% 0.64/0.69
% 0.64/0.69 SZS status Unsatisfiable
% 0.64/0.69
% 0.64/0.69 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.69
% 0.64/0.69 SPASS-SCL-FOL Statistics:
% 0.64/0.69 Number of learned clauses: 11
% 0.64/0.69 Number of propagations: 2784
% 0.64/0.69 Number of decisions: 124
% 0.64/0.69 Number of resolutions: 63
% 0.64/0.69 Number of condensations: 4
% 0.64/0.69 Number of sub resolutions: 21
% 0.64/0.69 Number of input literals (deduplicated): 18
% 0.64/0.69 Number of grows: 0
% 0.64/0.69 Number of considered ground atoms: 460
% 0.64/0.69
% 0.64/0.69 Needed: 0:00:00.16
% 0.64/0.69
%------------------------------------------------------------------------------