%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : COM003+3 : TPTP v9.2.1. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n022.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:19:09 PM UTC 2026
% Result : Theorem 0.46s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : COM003+3 : TPTP v9.2.1. Released v2.0.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n022.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 11:35:36 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.27/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.46/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.61 Execution resolution_1 ended with status: unsatisfiable
% 0.46/0.61 Used heuristic: resolution_1
% 0.46/0.61
% 0.46/0.61 Input Clauses:
% 0.46/0.61
% 0.46/0.61 Predicates: algorithm program decides halts2 halts3 outputs ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10
% 0.46/0.61 Fol Constants: good bad skc3 skc11
% 0.46/0.61 Fol Functions: skf1 skf2 skf4 skf5 skf6 skf7 skf8 skf9 skf10
% 0.46/0.61 Problem Properties:
% 0.46/0.61 This is a full first-order problem without equality.
% 0.46/0.61
% 0.46/0.61 After reduction: Problem Properties:
% 0.46/0.61 This is a full first-order problem without equality.
% 0.46/0.61
% 0.46/0.61
% 0.46/0.61 Reduced Input Clauses:
% 0.46/0.61
% 0.46/0.61 Most General Atoms: ren1(x1,x0) ren2(x0) decides(x0,x1,x2) algorithm(x0) ren3(x1,x0) halts3(x0,x1,x2) ren4(x2,x0,x1) ren5(x2,x0,x1) ren6(x1,x2,x0) ren7(x1,x2,x0) ren8(x1,x2,x0) ren10(x0,x1) program(x2) outputs(x1,good) halts2(x0,x2) outputs(x1,bad) ren9(x0,x2)
% 0.46/0.61
% 0.46/0.61 === Starting SPASS-SCL-FOL A Little Less Naive, considering 26 atoms initially, heuristics mode: resolution_1 ===
% 0.46/0.61
% 0.46/0.61 === Backtracking. Learning clause 29:3:1:[1.2,5.2]:Top: algorithm(x0) -> program(skf2(x0)),ren2(skc3)
% 0.46/0.61 === Backtracking. Learning clause 30:5:3:[12.1,14.3]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> ren4(x2,x0,x1)
% 0.46/0.61 === Backtracking. Learning clause 32:2:2:[1.0,31.1,2.1,4.3]:TopTop: ren2(x0) -> ren1(x1,x0)
% 0.46/0.61 === Backtracking. Learning clause 33:3:1:[5.2,32.2]:Top: algorithm(x0),ren2(x0) -> ren2(skc3)
% 0.46/0.61 === Backtracking. Learning clause 35:2:2:[6.0,34.1,7.1,4.3]:TopTop: ren2(x0) -> ren3(x1,x0)
% 0.46/0.61 === Backtracking. Learning clause 37:1:1:[1.0,36.0,2.1,28.2]:Top: -> ren1(x0,skc11)
% 0.46/0.61 === Backtracking. Learning clause 39:1:1:[6.0,38.0,7.1,28.2]:Top: -> ren3(x0,skc11)
% 0.46/0.61 === Backtracking. Learning clause 40:4:1:[26.3,18.2]:Top: program(x0),ren7(skf6(x0),skf7(x0),x0) -> ren10(skf10(x0),x0),program(skf8(x0))
% 0.46/0.61 === Clause set with instances from active satisfied. Growing active. New size: 34
% 0.46/0.61 === Restarting.
% 0.46/0.61 === Backtracking. Learning clause 42:1:0:[27.0,41.0,5.2,37.1]:: -> ren2(skc3)
% 0.46/0.61 === Clause set with instances from active satisfied. Growing active. New size: 35
% 0.46/0.61 === Restarting.
% 0.46/0.61 === Backtracking. Learning clause 43:5:3:[13.1,14.3]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts2(x0,x2),ren5(x1,x0,x2)
% 0.46/0.61 === Backtracking. Learning clause 44:5:1:[26.3,19.2,17.3]:Top: program(x0),halts2(skf8(x0),skf9(x0)),halts3(x0,skf6(x0),skf7(x0)),outputs(x0,good) -> ren10(skf10(x0),x0)
% 0.46/0.61 === Clause set with instances from active satisfied. Growing active. New size: 99
% 0.46/0.61 === Backtracking. Learning clause 45:7:1:[8.1,30.5,44.3]:Top: program(skf6(x0)),halts2(skf6(x0),skf7(x0)),ren3(skf5(x0),x0),program(x0),halts2(skf8(x0),skf9(x0)),outputs(x0,good) -> ren10(skf10(x0),x0)
% 0.46/0.61 === Clause set with instances from active satisfied. Growing active. New size: 163
% 0.46/0.61 === Backtracking. Learning clause 46:8:1:[10.1,43.5,20.1,26.3,17.3,8.2,30.5,45.5]:Top: program(skf8(x0)),outputs(x0,bad),program(skf6(x0)),halts2(skf6(x0),skf7(x0)),ren3(skf5(x0),x0),program(x0),outputs(x0,good) -> ren10(skf10(x0),x0)
% 0.46/0.61 === Backtracking. Learning clause 47:7:1:[10.2,20.1,43.5,44.2,26.3,17.3]:Top: outputs(x0,bad),program(skf8(x0)),ren3(skf5(x0),x0),program(x0),halts3(x0,skf6(x0),skf7(x0)),outputs(x0,good) -> ren10(skf10(x0),x0)
% 0.46/0.61 === Backtracking. Learning clause 49:7:2:[15.0,48.2,16.1,46.4]:TopTop: program(skf8(x0)),outputs(x0,bad),ren3(skf5(x0),x0),program(x0),outputs(x0,good) -> ren7(skf6(x0),skf7(x0),x1),ren10(skf10(x0),x0)
% 0.46/0.61 === Backtracking. Learning clause 50:6:1:[10.2,20.1,43.5,19.1,26.3,49.6]:Top: program(skf8(x0)),outputs(x0,bad),ren3(skf5(x0),x0),program(x0),outputs(x0,good) -> ren10(skf10(x0),x0)
% 0.46/0.61 === Conflict found: 30:5:3:[12.1,14.3]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> ren4(x2,x0,x1) {x0 -> skf6(good), x1 -> skf7(good), x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 52:4:3:[15.0,51.0,30.5,8.1,16.1,17.1]:TopTopTop: program(x0),ren3(skf5(x0),x0),outputs(x0,good) -> ren7(x1,x2,x0)
% 0.46/0.61 === Conflict found: 43:5:3:[13.1,14.3]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts2(x0,x2),ren5(x1,x0,x2) {x0 -> good, x1 -> good, x2 -> bad}
% 0.46/0.61 === Backtracking. Learning clause 53:4:3:[43.5,10.1,30.2,8.1]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts3(x1,x0,x2)
% 0.46/0.61 === Clause set with instances from active satisfied. Growing active. New size: 227
% 0.46/0.61 === Backtracking. Learning clause 54:6:5:[11.1,43.5,20.2]:TopTopTopTopTop: program(x0),program(x1),ren3(skf5(x1),x1),halts3(x1,x2,x3) -> halts2(x0,x4),ren8(x2,x3,x1)
% 0.46/0.61 === Backtracking. Learning clause 56:6:2:[3.1,55.4,21.2,24.5,25.5,50.6,35.2]:TopTop: program(x0),halts3(x1,x0,x0),program(skf8(x1)),outputs(x1,bad),outputs(x1,good),ren2(x1) ->
% 0.46/0.61 === Conflict found: 53:4:3:[43.5,10.1,30.2,8.1]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts3(x1,x0,x2) {x0 -> good, x1 -> good, x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 58:4:1:[3.1,57.0,53.3,35.2,56.2]:Top: program(skf8(x0)),outputs(x0,bad),outputs(x0,good),ren2(x0) ->
% 0.46/0.61 === Conflict found: 53:4:3:[43.5,10.1,30.2,8.1]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts3(x1,x0,x2) {x0 -> skf6(good), x1 -> good, x2 -> skf7(good)}
% 0.46/0.61 === Backtracking. Learning clause 61:3:3:[15.0,59.0,3.1,60.1,53.3,35.2,17.1]:TopTopTop: ren2(x0),outputs(x0,good) -> ren7(x1,x2,x0)
% 0.46/0.61 === Backtracking. Learning clause 63:5:3:[3.1,62.1,11.1,43.5,58.2,35.2]:TopTopTop: program(x0),program(skf8(x1)),outputs(x1,good),ren2(x1) -> halts2(x0,x2)
% 0.46/0.61 === Backtracking. Learning clause 67:5:6:[15.0,64.3,3.1,65.4,35.1,66.5,9.2,63.3,30.5,16.1]:TopTopTopTopTopTop: program(x0),program(skf8(x1)),ren2(x1) -> halts2(x0,x2),ren7(x3,x4,x5)
% 0.46/0.61 === Conflict found: 30:5:3:[12.1,14.3]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> ren4(x2,x0,x1) {x0 -> skf8(good), x1 -> skf9(good), x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 68:5:3:[30.5,9.1]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> outputs(x2,good)
% 0.46/0.61 === Conflict found: 68:5:3:[30.5,9.1]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> outputs(x2,good) {x0 -> skf10(good), x1 -> good, x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 70:4:3:[3.1,69.0,68.1,23.2,21.2,25.5,26.4,20.3,53.4,53.4,11.2,43.5,68.2,63.3,35.2,67.5]:TopTopTop: program(skf8(x0)),ren2(x0),program(x1) -> halts2(x1,x2)
% 0.46/0.61 === Conflict found: 68:5:3:[30.5,9.1]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> outputs(x2,good) {x0 -> skf8(good), x1 -> skf9(good), x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 72:4:4:[3.1,71.0,68.5,61.2,70.4,35.2]:TopTopTopTop: program(skf8(x0)),ren2(x0),ren2(x1) -> ren7(x2,x3,x1)
% 0.46/0.61 === Conflict found: 70:4:3:[3.1,69.0,68.1,23.2,21.2,25.5,26.4,20.3,53.4,53.4,11.2,43.5,68.2,63.3,35.2,67.5]:TopTopTop: program(skf8(x0)),ren2(x0),program(x1) -> halts2(x1,x2) {x0 -> good, x1 -> skf10(good), x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 74:2:1:[3.1,73.0,70.3,23.2,24.5,26.4,53.4,19.2,68.5,70.4,35.2,72.4]:Top: program(skf8(x0)),ren2(x0) ->
% 0.46/0.61 === Conflict found: 30:5:3:[12.1,14.3]:TopTopTop: program(x0),halts2(x0,x1),program(x2),ren3(skf5(x2),x2) -> ren4(x2,x0,x1) {x0 -> skf6(good), x1 -> skf7(good), x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 76:2:3:[3.1,75.0,30.1,15.1,9.1,16.1,61.2,35.2]:TopTopTop: ren2(x0) -> ren7(x1,x2,x0)
% 0.46/0.61 === Conflict found: 53:4:3:[43.5,10.1,30.2,8.1]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts3(x1,x0,x2) {x0 -> bad, x1 -> good, x2 -> bad}
% 0.46/0.61 === Backtracking. Learning clause 77:5:5:[53.1,18.1,54.4]:TopTopTopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts2(x0,x2),ren8(x3,x4,x1)
% 0.46/0.61 === Clause set with instances from active satisfied. Growing active. New size: 291
% 0.46/0.61 === Backtracking. Learning clause 78:5:3:[25.5,21.1]:TopTopTop: ren10(x0,x1),program(x2),halts3(x1,x2,x2),outputs(x1,bad) -> halts2(x0,x2)
% 0.46/0.61 === Conflict found: 43:5:3:[13.1,14.3]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts2(x0,x2),ren5(x1,x0,x2) {x0 -> skf10(good), x1 -> good, x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 80:4:1:[52.3,79.1,43.5,11.1,23.2,78.4,24.5,26.4,53.4,19.2]:Top: outputs(x0,good),program(x0),ren3(skf5(x0),x0),halts2(skf8(x0),skf9(x0)) ->
% 0.46/0.61 === Conflict found: 43:5:3:[13.1,14.3]:TopTopTop: program(x0),program(x1),ren3(skf5(x1),x1) -> halts2(x0,x2),ren5(x1,x0,x2) {x0 -> skf10(good), x1 -> good, x2 -> good}
% 0.46/0.61 === Backtracking. Learning clause 83:5:2:[53.3,81.2,52.3,82.5,43.5,11.1,23.2,78.4,24.5,26.4]:TopTop: ren3(skf5(x0),x0),program(x1),outputs(x0,good),program(x0),ren8(skf8(x0),skf9(x0),x0) ->
% 0.46/0.61 === Backtracking. Learning clause 86:2:1:[35.1,84.1,3.1,85.3,18.1,74.1,83.5]:Top: ren2(x0),outputs(x0,good) ->
% 0.46/0.61 === Backtracking. Learning clause 87:7:2:[11.1,43.5,78.4,53.4,68.2,23.2,26.4]:TopTop: ren3(skf5(x0),x0),program(x1),ren3(skf5(x1),x1),program(x0),ren7(skf6(x0),skf7(x0),x0),ren8(skf8(x0),skf9(x0),x0) -> outputs(x1,good)
% 0.46/0.61 === Backtracking. Learning clause 89:1:1:[3.1,88.0,18.1,74.1,87.6,35.2,86.2,76.2]:Top: ren2(x0) ->
% 0.46/0.61 === Conflict found: 89:1:1:[3.1,88.0,18.1,74.1,87.6,35.2,86.2,76.2]:Top: ren2(x0) -> {x0 -> skc3}
% 0.46/0.61
% 0.46/0.61 SZS status Unsatisfiable
% 0.46/0.61
% 0.46/0.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.61
% 0.46/0.61 SPASS-SCL-FOL Statistics:
% 0.46/0.61 Number of learned clauses: 36
% 0.46/0.61 Number of propagations: 1103
% 0.46/0.61 Number of decisions: 352
% 0.46/0.61 Number of resolutions: 114
% 0.46/0.61 Number of condensations: 11
% 0.46/0.61 Number of sub resolutions: 25
% 0.46/0.61 Number of input literals (deduplicated): 28
% 0.46/0.61 Number of grows: 6
% 0.46/0.61 Number of considered ground atoms: 291
% 0.46/0.61
% 0.46/0.61 Needed: 0:00:00.07
% 0.46/0.61
%------------------------------------------------------------------------------