%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : KRS140+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 : n003.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.62s 0.60s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS140+1 : TPTP v9.2.1. Released v3.1.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n003.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:42 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.62/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.60 Execution normal ended with status: unsatisfiable % 0.62/0.60 Used heuristic: normal % 0.62/0.60 % 0.62/0.60 Input Clauses: % 0.62/0.60 % 0.62/0.60 Predicates: = cowlNothing cowlThing rsymProp xsd_integer xsd_string ren1 ren2 % 0.62/0.60 Fol Constants: ia ib skc1 skc2 skc3 skc4 skc5 skc6 % 0.62/0.60 Fol Functions: % 0.62/0.60 Problem Properties: % 0.62/0.60 This is a Bernays Schoenfinkel Ramsey problem. % 0.62/0.60 % 0.62/0.60 % 0.62/0.60 Reduced Input Clauses: % 0.62/0.60 29:3:1:[7.0,24.0,7.0,27.4,8.0,28.5]:Top: ren1(skc3),ren2(skc4,skc5,skc6),rsymProp(ia,x0) -> % 0.62/0.60 26:2:1:[10.0,20.0]:Top: -> xsd_string(x0),ren1(x0) % 0.62/0.60 25:2:1:[10.1,19.0]:Top: -> xsd_integer(x0),ren1(x0) % 0.62/0.60 % 0.62/0.60 Most General Atoms: =(x0,x1) xsd_integer(x1) xsd_string(x1) cowlThing(x0) cowlNothing(x0) rsymProp(x1,x0) ren2(x0,x1,x2) ren1(x0) % 0.62/0.60 % 0.62/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 680 atoms initially, heuristics mode: normal === % 0.62/0.60 % 0.62/0.60 === Backtracking. Learning clause 30:2:4:[23.1,21.1]:TopTopTopTop: -> ren2(x0,x1,x2),ren2(x0,x2,x3) % 0.62/0.60 === Backtracking. Learning clause 31:2:2:[9.1,26.1,25.1,29.1,23.2,22.1]:TopTop: rsymProp(ia,x0) -> ren2(x1,skc4,skc6) % 0.62/0.60 === CC is in false state. New clause to be learned: 33:3:0:[14.0,32.2]:: =(skc4,ia),=(skc6,ia) -> rsymProp(skc6,skc4) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 34:3:0:TAUT:: =(skc4,ia),ren2(skc4,skc4,skc1) -> ren2(ia,skc4,skc1) % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 35:2:4:[23.1,22.1]:TopTopTopTop: -> ren2(x0,x1,x2),ren2(x3,x0,x2) % 0.62/0.60 === Backtracking. Learning clause 36:1:0:[9.2,25.1,26.1,29.1,14.1]:: ren2(skc4,skc5,skc6) -> % 0.62/0.60 === CC is in false state. New clause to be learned: 37:2:0:TAUT:: =(skc3,ia) -> =(ia,skc3) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 38:3:0:TAUT:: =(skc6,ib),ren2(ib,ib,skc2) -> ren2(skc6,ib,skc2) % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 39:2:4:[12.1,21.1,23.1]:TopTopTopTop: -> ren2(x0,x1,x2),ren2(x1,x3,x0) % 0.62/0.60 === Backtracking. Learning clause 40:5:3:[11.2,33.2,4.1,11.2,23.1,12.1]:TopTopTop: rsymProp(x0,skc6),rsymProp(x1,skc4) -> =(skc4,ib),ren2(x0,x2,ib),rsymProp(skc4,skc6) % 0.62/0.60 === CC is in false state. New clause to be learned: 41:3:0:TAUT:: =(skc6,ib),rsymProp(ib,skc4) -> rsymProp(skc6,skc4) % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 42:3:3:[4.2,12.2]:TopTopTop: =(x0,x1),rsymProp(x0,x2) -> rsymProp(x2,x1) % 0.62/0.60 === CC is in false state. New clause to be learned: 43:3:0:TAUT:: =(skc5,ia),=(skc4,ia) -> =(skc5,skc4) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 44:3:0:TAUT:: =(skc6,ia),ren2(skc6,skc6,skc1) -> ren2(skc6,ia,skc1) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 46:3:0:[14.0,45.2]:: =(skc6,ia),=(skc4,skc6) -> rsymProp(skc6,skc4) % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 48:7:3:[4.0,47.3,11.2,43.1,3.3,3.1,11.3,33.2,4.3,11.2,4.1,12.1,12.2,21.1]:TopTopTop: rsymProp(skc6,skc5),rsymProp(x0,skc6),rsymProp(x1,skc4) -> rsymProp(skc6,skc4),rsymProp(x1,ib),rsymProp(ia,ib),ren2(skc4,skc5,x2) % 0.62/0.60 === CC is in false state. New clause to be learned: 49:4:0:TAUT:: =(skc5,ib),=(skc6,ib),rsymProp(skc5,skc4) -> rsymProp(skc6,skc4) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 51:3:0:[36.0,50.3]:: =(skc6,ia),=(skc4,ib),ren2(ib,skc5,ia) -> % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 52:1:0:[21.2,36.1,12.1]:: -> rsymProp(skc5,skc4) % 0.62/0.60 === CC is in false state. New clause to be learned: 53:4:0:TAUT:: =(skc6,ia),=(skc4,ib),rsymProp(ib,ia) -> rsymProp(skc4,skc6) % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 54:3:3:[11.1,22.1]:TopTopTop: -> =(x0,ia),=(x0,ib),ren2(x1,x2,x0) % 0.62/0.60 === Backtracking. Learning clause 55:3:1:[12.2,23.1,33.3,54.1]:Top: =(skc4,ia) -> ren2(skc4,x0,skc6),=(skc6,ib) % 0.62/0.60 === CC is in false state. New clause to be learned: 56:4:0:TAUT:: =(skc5,ia),=(skc4,ia),rsymProp(skc5,skc6) -> rsymProp(skc4,skc6) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 57:4:0:TAUT:: =(skc6,ia),=(skc4,ib),=(skc6,ib) -> =(skc4,ia) % 0.62/0.60 === Restarting. % 0.62/0.60 === CC is in false state. New clause to be learned: 59:3:0:[16.0,58.2]:: =(skc6,ib),=(skc4,ib) -> rsymProp(skc4,skc6) % 0.62/0.60 === Restarting. % 0.62/0.60 === Backtracking. Learning clause 61:1:0:[52.0,60.1,11.2,4.1,3.1,53.3,3.3,11.3,4.3,22.1,33.1,12.1,23.1,36.1,12.2]:: =(skc6,ia) -> % 0.62/0.60 % 0.62/0.60 SZS status Unsatisfiable % 0.62/0.60 % 0.62/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.62/0.60 % 0.62/0.60 SPASS-SCL-FOL Statistics: % 0.62/0.60 Number of learned clauses: 12 % 0.62/0.60 Number of propagations: 3727 % 0.62/0.60 Number of decisions: 94 % 0.62/0.60 Number of resolutions: 60 % 0.62/0.60 Number of condensations: 4 % 0.62/0.60 Number of sub resolutions: 11 % 0.62/0.60 Number of input literals (deduplicated): 15 % 0.62/0.60 Number of grows: 0 % 0.62/0.60 Number of considered ground atoms: 680 % 0.62/0.60 % 0.62/0.60 Needed: 0:00:00.10 % 0.62/0.60 %------------------------------------------------------------------------------