%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : COM003+1 : 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 : n007.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 1.40s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM003+1 : TPTP v9.2.1. Released v2.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n007.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 11:34:54 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.40/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.40/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.40/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.40/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.40/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.40/0.83 Execution normal ended with status: unsatisfiable
% 1.40/0.83 Used heuristic: normal
% 1.40/0.83
% 1.40/0.83 Input Clauses:
% 1.40/0.83
% 1.40/0.83 Predicates: algorithm program decides halts2 halts3 outputs ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15
% 1.40/0.83 Fol Constants: good bad skc3 skc8 skc11 skc12
% 1.40/0.83 Fol Functions: skf1 skf2 skf4 skf5 skf6 skf7 skf9 skf10
% 1.40/0.83 Problem Properties:
% 1.40/0.83 This is a full first-order problem without equality.
% 1.40/0.83
% 1.40/0.83 After reduction: Problem Properties:
% 1.40/0.83 This is a full first-order problem without equality.
% 1.40/0.83
% 1.40/0.83
% 1.40/0.83 Reduced Input Clauses:
% 1.40/0.83
% 1.40/0.83 Most General Atoms: ren1(x1,x0) ren2(x0) program(x1) decides(x0,x1,x2) algorithm(x0) ren3(x1,x0) halts3(x0,x1,x2) outputs(x0,good) outputs(x0,bad) halts2(x0,x1) ren4(x2,x0,x1) ren5(x2,x0,x1) ren6(x1,x2,x0) ren7(x1,x0) ren8(x1,x0) ren9(x0,x1) ren10(x0,x1) ren11(x0) ren12(x1,x0) ren13(x1,x0) ren14(x0,x1) ren15(x0)
% 1.40/0.83
% 1.40/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 70 atoms initially, heuristics mode: normal ===
% 1.40/0.83
% 1.40/0.83 === Backtracking. Learning clause 44:2:1:[25.1,43.2,27.4,23.1,38.3]:Top: ren11(x0),ren15(x0) ->
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 134
% 1.40/0.83 === Backtracking. Learning clause 45:4:3:[9.1,12.4]:TopTopTop: ren6(x0,x1,x2),program(x0),halts2(x0,x1) -> outputs(x2,good)
% 1.40/0.83 === Backtracking. Learning clause 48:2:2:[15.0,46.1,16.0,47.2,8.2,17.1,12.4,45.4]:TopTop: ren6(x0,x0,x1) -> ren7(x0,x1)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 198
% 1.40/0.83 === Backtracking. Learning clause 49:2:2:[4.3,7.1,6.1]:TopTop: ren2(x0) -> ren3(x1,x0)
% 1.40/0.83 === Backtracking. Learning clause 50:2:3:[14.1,3.2,49.2]:TopTopTop: ren2(x0) -> ren6(x1,x2,x0)
% 1.40/0.83 === Backtracking. Learning clause 51:3:2:[23.2,34.1,27.4,32.1,33.1]:TopTop: outputs(x0,bad),ren11(x0) -> ren13(x1,x0)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 262
% 1.40/0.83 === Backtracking. Learning clause 52:3:2:[26.3,27.3,21.1,23.1]:TopTop: ren11(x0),program(x1) -> halts2(x0,x1)
% 1.40/0.83 === Conflict found: 52:3:2:[26.3,27.3,21.1,23.1]:TopTop: ren11(x0),program(x1) -> halts2(x0,x1) {x0 -> good, x1 -> skf9(good)}
% 1.40/0.83 === Backtracking. Learning clause 54:5:2:[25.1,53.2,52.2,29.1,31.1,40.2,37.1,52.2]:TopTop: ren11(x0),outputs(x0,good),ren13(skf10(x0),x0),ren11(x1) -> halts2(x1,skc11)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 326
% 1.40/0.83 === Backtracking. Learning clause 55:4:2:[36.1,39.4]:TopTop: ren15(x0),program(x1) -> outputs(x0,bad),halts2(x1,x1)
% 1.40/0.83 === Backtracking. Learning clause 56:3:1:[39.4,35.1,38.3,37.2,40.4]:Top: program(x0),ren12(skf9(x0),x0),ren13(skf10(x0),x0) ->
% 1.40/0.83 === Backtracking. Learning clause 57:3:2:[22.2,31.2,26.4,52.3,29.1,56.2,25.2,51.3,24.2]:TopTop: halts2(x0,x0),ren11(x0),ren10(x0,x1) ->
% 1.40/0.83 === Backtracking. Learning clause 58:4:2:[27.3,33.1,32.1,57.3,56.3,25.2]:TopTop: halts2(x0,x0),ren11(x0),ren12(skf9(x1),x1),ren11(x1) ->
% 1.40/0.83 === Backtracking. Learning clause 59:3:3:[27.3,33.1,32.1]:TopTopTop: ren11(x0) -> ren10(x0,x1),ren13(x1,x2)
% 1.40/0.83 === Backtracking. Learning clause 60:2:1:[22.1,26.4,31.2,52.3,29.1,25.2,58.3]:Top: halts2(x0,x0),ren11(x0) ->
% 1.40/0.83 === Conflict found: 52:3:2:[26.3,27.3,21.1,23.1]:TopTop: ren11(x0),program(x1) -> halts2(x0,x1) {x0 -> good, x1 -> good}
% 1.40/0.83 === Backtracking. Learning clause 61:1:1:[52.3,60.1,25.2]:Top: ren11(x0) ->
% 1.40/0.83 === Conflict found: 45:4:3:[9.1,12.4]:TopTopTop: ren6(x0,x1,x2),program(x0),halts2(x0,x1) -> outputs(x2,good) {x0 -> skf6(good), x1 -> skf6(good), x2 -> bad}
% 1.40/0.83 === Backtracking. Learning clause 62:3:3:[45.3,16.1,15.1]:TopTopTop: ren6(x0,x0,x1) -> outputs(x1,good),ren7(x0,x2)
% 1.40/0.83 === Conflict found: 45:4:3:[9.1,12.4]:TopTopTop: ren6(x0,x1,x2),program(x0),halts2(x0,x1) -> outputs(x2,good) {x0 -> skf6(good), x1 -> skf6(good), x2 -> bad}
% 1.40/0.83 === Backtracking. Learning clause 63:3:3:[45.1,50.2,15.1,16.1]:TopTopTop: ren2(x0) -> outputs(x0,good),ren7(x1,x2)
% 1.40/0.83 === Conflict found: 45:4:3:[9.1,12.4]:TopTopTop: ren6(x0,x1,x2),program(x0),halts2(x0,x1) -> outputs(x2,good) {x0 -> skf9(bad), x1 -> skf9(bad), x2 -> bad}
% 1.40/0.83 === Backtracking. Learning clause 64:3:3:[45.3,30.1,29.1]:TopTopTop: ren6(x0,x0,x1) -> outputs(x1,good),ren12(x0,x2)
% 1.40/0.83 === Backtracking. Learning clause 65:2:1:[37.2,38.2]:Top: ren15(x0),halts2(x0,x0) ->
% 1.40/0.83 === Backtracking. Learning clause 67:1:1:[41.0,66.0,42.2,2.1,1.1,5.2,49.1]:Top: -> ren3(x0,skc3)
% 1.40/0.83 === Backtracking. Learning clause 68:1:1:[35.1,39.4,65.2,37.2]:Top: ren15(x0) ->
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 390
% 1.40/0.83 === Conflict found: 48:2:2:[15.0,46.1,16.0,47.2,8.2,17.1,12.4,45.4]:TopTop: ren6(x0,x0,x1) -> ren7(x0,x1) {x0 -> skf6(bad), x1 -> bad}
% 1.40/0.83 === Backtracking. Learning clause 71:2:1:[3.1,69.1,61.0,70.3,48.1,50.2,28.2]:Top: ren2(x0),ren8(skf7(x0),x0) ->
% 1.40/0.83 === Backtracking. Learning clause 72:2:2:[4.3,2.1,1.1]:TopTop: ren2(x0) -> ren1(x1,x0)
% 1.40/0.83 === Backtracking. Learning clause 73:1:1:[42.2,2.1,1.1]:Top: -> ren1(x0,skc12)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 454
% 1.40/0.83 === Backtracking. Learning clause 74:5:3:[14.3,45.1]:TopTopTop: program(x0),ren3(skf5(x0),x0),program(x1),halts2(x1,x2) -> outputs(x0,good)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 518
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 582
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 646
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 710
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 774
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 838
% 1.40/0.83 === Conflict found: 48:2:2:[15.0,46.1,16.0,47.2,8.2,17.1,12.4,45.4]:TopTop: ren6(x0,x0,x1) -> ren7(x0,x1) {x0 -> skf6(skf6(good)), x1 -> skf6(good)}
% 1.40/0.83 === Backtracking. Learning clause 75:2:2:[48.1,50.2]:TopTop: ren2(x0) -> ren7(x1,x0)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 902
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 966
% 1.40/0.83 === Backtracking. Learning clause 76:4:3:[11.1,13.4]:TopTopTop: ren6(x0,x1,x2),program(x0) -> outputs(x2,bad),halts2(x0,x1)
% 1.40/0.83 === Clause set with instances from active satisfied. Growing active. New size: 1030
% 1.40/0.83 === Backtracking. Learning clause 79:3:3:[18.0,77.0,19.0,78.3,13.1,50.2,10.1,20.1,36.2]:TopTopTop: ren2(x0),ren14(x0,x1) -> ren8(x2,x0)
% 1.40/0.83
% 1.40/0.83 SZS status Unsatisfiable
% 1.40/0.83
% 1.40/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.40/0.83
% 1.40/0.83 SPASS-SCL-FOL Statistics:
% 1.40/0.83 Number of learned clauses: 28
% 1.40/0.83 Number of propagations: 2541
% 1.40/0.83 Number of decisions: 2203
% 1.40/0.83 Number of resolutions: 88
% 1.40/0.83 Number of condensations: 12
% 1.40/0.83 Number of sub resolutions: 9
% 1.40/0.83 Number of input literals (deduplicated): 37
% 1.40/0.83 Number of grows: 15
% 1.40/0.83 Number of considered ground atoms: 1030
% 1.40/0.83
% 1.40/0.83 Needed: 0:00:00.26
% 1.40/0.83
%------------------------------------------------------------------------------