%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NUN067+1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:31:02 PM UTC 2026
% Result : Theorem 5.84s 1.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN067+1 : TPTP v9.2.1. Released v7.3.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 : n002.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:54:47 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.84/1.92 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/1.92 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/1.92 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/1.92 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/1.92 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/1.92 Execution resolution_2 ended with status: unsatisfiable
% 5.84/1.92 Used heuristic: resolution_2
% 5.84/1.92
% 5.84/1.92 Input Clauses:
% 5.84/1.92
% 5.84/1.92 Predicates: id r1 r2 r3 r4 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18
% 5.84/1.92 Fol Constants: skc1
% 5.84/1.92 Fol Functions: skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21
% 5.84/1.92 Problem Properties:
% 5.84/1.92 This is a full first-order problem without equality.
% 5.84/1.92
% 5.84/1.92 After reduction: Problem Properties:
% 5.84/1.92 This is a full first-order problem without equality.
% 5.84/1.92
% 5.84/1.92
% 5.84/1.92 Reduced Input Clauses:
% 5.84/1.92
% 5.84/1.92 Most General Atoms: ren1(x0,x1) ren2(x0,x1) ren3(x0,x1,x2) ren4(x0,x1,x2) ren5(x0,x1,x2,x3) ren6(x0,x1,x2,x3) ren7(x0,x1,x2,x3) ren8(x0,x1,x2,x3) ren9(x0,x1) r1(x1) ren10(x0,x1) ren11(x0,x2,x1,x3) ren12(x0,x2,x1,x3) r3(x3,x4,x5) id(x4,x5) ren13(x0,x2,x4,x1,x3,x5) ren14(x0,x2,x4,x1,x3,x5) r4(x3,x4,x5) ren15(x0,x2,x4,x1,x3,x5) ren16(x0,x2,x4,x1,x3,x5) ren17(x0,x1) ren18(x0,x1,x2) r2(x2,x1)
% 5.84/1.92
% 5.84/1.92 === Starting SPASS-SCL-FOL A Little Less Naive, considering 53 atoms initially, heuristics mode: resolution_2 ===
% 5.84/1.92
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 53
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Backtracking. Learning clause 70:2:1:[43.1,21.1]:Top: -> ren15(x0,x0,x0,x0,x0,x0),ren16(x0,x0,x0,x0,x0,x0)
% 5.84/1.92 === Backtracking. Learning clause 71:2:1:[38.1,21.1]:Top: -> ren13(x0,x0,x0,x0,x0,x0),ren14(x0,x0,x0,x0,x0,x0)
% 5.84/1.92 === Backtracking. Learning clause 72:2:1:[33.1,21.1,31.1]:Top: -> ren11(x0,x0,x0,x0),r2(x0,x0)
% 5.84/1.92 === Backtracking. Learning clause 73:2:1:[28.1,21.1]:Top: -> ren9(x0,x0),ren10(x0,x0)
% 5.84/1.92 === Backtracking. Learning clause 74:1:3:[19.2,21.1]:TopTopTop: ren8(x0,x1,x2,x2) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 71
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Backtracking. Learning clause 75:4:6:[43.1,44.1]:TopTopTopTopTopTop: id(x0,x1),id(x2,x3) -> ren15(skf6(x4,x5),x0,x2,skf5(x4,x5),x1,x3),ren16(skf6(x4,x5),x0,x2,skf5(x4,x5),x1,x3)
% 5.84/1.92 === Backtracking. Learning clause 76:4:6:[38.1,44.1]:TopTopTopTopTopTop: id(x0,x1),id(x2,x3) -> ren13(skf6(x4,x5),x0,x2,skf5(x4,x5),x1,x3),ren14(skf6(x4,x5),x0,x2,skf5(x4,x5),x1,x3)
% 5.84/1.92 === Backtracking. Learning clause 77:3:4:[33.1,44.1]:TopTopTopTop: id(x0,x1) -> ren11(skf6(x2,x3),x0,skf5(x2,x3),x1),ren12(skf6(x2,x3),x0,skf5(x2,x3),x1)
% 5.84/1.92 === Backtracking. Learning clause 78:2:2:[28.1,44.1,26.1]:TopTop: -> ren9(skf6(x0,x1),skf5(x0,x1)),r1(skf6(x0,x1))
% 5.84/1.92 === Backtracking. Learning clause 79:2:3:[23.1,44.1]:TopTopTop: id(skf5(x0,x1),x2) -> id(skf6(x0,x1),x2)
% 5.84/1.92 === Backtracking. Learning clause 80:1:4:[14.2,44.1]:TopTopTopTop: ren6(x0,x1,skf6(x2,x3),skf5(x2,x3)) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 76
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Backtracking. Learning clause 81:2:3:[22.2,9.2]:TopTopTop: id(x0,x1),ren4(x2,x1,x0) ->
% 5.84/1.92 === Backtracking. Learning clause 82:1:3:[8.2,45.1]:TopTopTop: ren4(x0,skf7(x1,x0),x2) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 79
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Backtracking. Learning clause 83:1:5:[35.2,46.1]:TopTopTopTopTop: ren13(x0,x1,x2,x3,skf7(x3,x4),skf6(x3,x4)) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 143
% 5.84/1.92 === Backtracking. Learning clause 84:4:4:[22.2,67.1,23.3]:TopTopTopTop: r1(x0),r2(x1,x2),id(x2,x3),id(x3,x0) ->
% 5.84/1.92 === Conflict found: 84:4:4:[22.2,67.1,23.3]:TopTopTopTop: r1(x0),r2(x1,x2),id(x2,x3),id(x3,x0) -> {x0 -> skc1, x1 -> skf8(skc1,skc1), x2 -> skf5(skc1,skc1), x3 -> skf6(skc1,skc1)}
% 5.84/1.92 === Backtracking. Learning clause 85:4:4:[84.3,22.2,2.2,5.1]:TopTopTopTop: r2(x0,x1),id(x2,x3),id(x2,x1) -> ren2(x3,skc1)
% 5.84/1.92 === Conflict found: 85:4:4:[84.3,22.2,2.2,5.1]:TopTopTopTop: r2(x0,x1),id(x2,x3),id(x2,x1) -> ren2(x3,skc1) {x0 -> skf8(skc1,skc1), x1 -> skf5(skc1,skc1), x2 -> skf6(skc1,skc1), x3 -> skc1}
% 5.84/1.92 === Backtracking. Learning clause 86:4:4:[85.4,4.1]:TopTopTopTop: r2(x0,x1),id(x2,x3),id(x2,x1),id(x3,skc1) ->
% 5.84/1.92 === Conflict found: 86:4:4:[85.4,4.1]:TopTopTopTop: r2(x0,x1),id(x2,x3),id(x2,x1),id(x3,skc1) -> {x0 -> skf8(skc1,skc1), x1 -> skf5(skc1,skc1), x2 -> skc1, x3 -> skc1}
% 5.84/1.92 === Backtracking. Learning clause 87:4:5:[86.1,47.1,22.2,23.3,22.2]:TopTopTopTopTop: id(x0,x1),id(x1,skc1),id(x2,x0),id(x2,skf5(x3,x4)) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 146
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Backtracking. Learning clause 88:1:5:[35.2,48.1]:TopTopTopTopTop: ren13(x0,x1,x2,x3,x4,skf8(x3,x4)) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 173
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Conflict found: 86:4:4:[85.4,4.1]:TopTopTopTop: r2(x0,x1),id(x2,x3),id(x2,x1),id(x3,skc1) -> {x0 -> skc1, x1 -> skf10(skc1,skc1), x2 -> skc1, x3 -> skc1}
% 5.84/1.92 === Backtracking. Learning clause 89:2:2:[86.2,21.1]:TopTop: r2(x0,x1),id(skc1,x1) ->
% 5.84/1.92 === Conflict found: 81:2:3:[22.2,9.2]:TopTopTop: id(x0,x1),ren4(x2,x1,x0) -> {x0 -> skf10(skc1,skc1), x1 -> skf9(skc1,skc1), x2 -> skc1}
% 5.84/1.92 === Backtracking. Learning clause 90:1:3:[81.1,49.1]:TopTopTop: ren4(x0,skf9(x1,x2),skf10(x1,x2)) ->
% 5.84/1.92 === Backtracking. Learning clause 91:5:5:[27.2,84.1,28.3]:TopTopTopTopTop: r2(x0,x1),id(x1,x2),id(x2,x3),id(x4,x3) -> ren9(x4,x3)
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 177
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Conflict found: 86:4:4:[85.4,4.1]:TopTopTopTop: r2(x0,x1),id(x2,x3),id(x2,x1),id(x3,skc1) -> {x0 -> skc1, x1 -> skf11(skc1,skc1), x2 -> skc1, x3 -> skf11(skc1,skc1)}
% 5.84/1.92 === Backtracking. Learning clause 92:3:4:[86.1,50.1,22.2]:TopTopTopTop: id(x0,x1),id(x0,skf11(x2,x3)),id(skc1,x1) ->
% 5.84/1.92 === Conflict found: 87:4:5:[86.1,47.1,22.2,23.3,22.2]:TopTopTopTopTop: id(x0,x1),id(x1,skc1),id(x2,x0),id(x2,skf5(x3,x4)) -> {x0 -> skc1, x1 -> skc1, x2 -> skf6(skc1,skc1), x3 -> skc1, x4 -> skc1}
% 5.84/1.92 === Backtracking. Learning clause 93:2:3:[87.1,21.1]:TopTopTop: id(x0,skc1),id(x0,skf5(x1,x2)) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 180
% 5.84/1.92 === Restarting.
% 5.84/1.92 === Backtracking. Learning clause 94:1:5:[40.2,51.1]:TopTopTopTopTop: ren15(x0,x1,x2,x3,skf11(x3,x4),skf10(x3,x4)) ->
% 5.84/1.92 === Clause set with instances from active satisfied. Growing active. New size: 244
% 5.84/1.92 === Backtracking. Learning clause 95:3:2:[28.2,24.1,27.1]:TopTop: id(x0,x1),r1(x0) -> r1(x1)
% 5.84/1.92
% 5.84/1.92 SZS status Unsatisfiable
% 5.84/1.92
% 5.84/1.92 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/1.92
% 5.84/1.92 SPASS-SCL-FOL Statistics:
% 5.84/1.92 Number of learned clauses: 26
% 5.84/1.92 Number of propagations: 1321
% 5.84/1.92 Number of decisions: 274
% 5.84/1.92 Number of resolutions: 43
% 5.84/1.92 Number of condensations: 0
% 5.84/1.92 Number of sub resolutions: 0
% 5.84/1.92 Number of input literals (deduplicated): 53
% 5.84/1.92 Number of grows: 10
% 5.84/1.92 Number of considered ground atoms: 244
% 5.84/1.92
% 5.84/1.92 Needed: 0:00:01.36
% 5.84/1.92
%------------------------------------------------------------------------------