%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL658+1.001 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:28:09 PM UTC 2026
% Result : Theorem 92.22s 18.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : LCL658+1.001 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n004.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 12:35:48 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 SPASS-SCL-FOL version:
% 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 92.22/18.99 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.22/18.99 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.22/18.99 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.22/18.99 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.22/18.99 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.22/18.99 Execution normal ended with status: unsatisfiable
% 92.22/18.99 Used heuristic: normal
% 92.22/18.99
% 92.22/18.99 Input Clauses:
% 92.22/18.99
% 92.22/18.99 Predicates: r1 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10
% 92.22/18.99 Fol Constants: skc13 skc14 skc15 skc16
% 92.22/18.99 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf17
% 92.22/18.99 Problem Properties:
% 92.22/18.99 This is a full first-order problem without equality.
% 92.22/18.99
% 92.22/18.99 After reduction: Problem Properties:
% 92.22/18.99 This is a full first-order problem without equality.
% 92.22/18.99
% 92.22/18.99
% 92.22/18.99 Reduced Input Clauses:
% 92.22/18.99
% 92.22/18.99 Most General Atoms: ren1(x1,x0) ren2(x1) ren3(x4,x0) ren4(x1,x0) p1(x1) ren5(x3,x0) ren6(x1,x0) ren7(x1,x0) ren8(x3,x0) ren9(x0) r1(x0,x2) ren10(x1,x0)
% 92.22/18.99
% 92.22/18.99 === Starting SPASS-SCL-FOL A Little Less Naive, considering 72 atoms initially, heuristics mode: normal ===
% 92.22/18.99
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 136
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 200
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 264
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 328
% 92.22/18.99 === Backtracking. Learning clause 43:2:3:[27.2,33.1,35.1,34.1,32.1]:TopTopTop: -> ren8(x0,x1),ren10(x1,x2)
% 92.22/18.99 === Backtracking. Learning clause 44:1:1:[41.1,22.1,23.1]:Top: -> ren7(x0,skc16)
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 392
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 456
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 520
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 584
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 648
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 712
% 92.22/18.99 === Backtracking. Learning clause 45:6:2:[41.1,19.1,20.1,30.5,2.1,3.1,4.1,28.5]:TopTop: ren9(x0),r1(x0,x1),p1(x0),r1(x0,skc16),ren3(x0,skf6(x0)) -> p1(x1)
% 92.22/18.99 === Backtracking. Learning clause 46:5:4:[30.4,33.1,32.1,34.1]:TopTopTopTop: ren9(x0),r1(x1,x2),ren6(x1,skf9(x1)) -> ren10(x0,x1),ren10(x3,x2)
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 776
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 840
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 904
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 968
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1032
% 92.22/18.99 === Conflict found: 43:2:3:[27.2,33.1,35.1,34.1,32.1]:TopTopTop: -> ren8(x0,x1),ren10(x1,x2) {x0 -> skc14, x1 -> skf2(skc14), x2 -> skf17(skf2(skc14))}
% 92.22/18.99 === Backtracking. Learning clause 48:2:2:[26.0,47.2,43.2,42.2]:TopTop: r1(skc14,x0) -> ren8(x1,x0)
% 92.22/18.99 === Backtracking. Learning clause 49:1:1:[25.1,48.1]:Top: -> ren8(skc14,x0)
% 92.22/18.99 === Backtracking. Learning clause 50:4:4:[13.6,23.1,22.1,24.1,21.1]:TopTopTopTop: r1(x0,x1),ren2(x1) -> ren3(x2,x0),ren7(x1,x3)
% 92.22/18.99 === Backtracking. Learning clause 51:2:3:[27.2,3.1,2.1,5.1,4.1]:TopTopTop: -> ren8(x0,x1),ren1(x1,x2)
% 92.22/18.99 === Backtracking. Learning clause 52:5:3:[30.4,6.1,7.1]:TopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren2(x2)
% 92.22/18.99 === Backtracking. Learning clause 53:4:3:[30.3,2.1,3.1,4.1]:TopTopTop: ren9(x0),r1(x0,x1),ren6(x1,skf9(x1)) -> ren1(x1,x2)
% 92.22/18.99 === Backtracking. Learning clause 54:5:4:[30.4,22.1,23.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren7(x3,x2)
% 92.22/18.99 === Backtracking. Learning clause 55:3:2:[41.1,19.1,20.1,54.4,21.1]:TopTop: ren9(x0),r1(x0,skc16) -> ren7(skc16,x1)
% 92.22/18.99 === Backtracking. Learning clause 56:1:1:[41.1,19.1,20.1]:Top: -> ren6(skc16,x0)
% 92.22/18.99 === Backtracking. Learning clause 57:2:1:[36.2,30.1,37.1,40.1,22.1,23.1,21.1]:Top: ren6(skc16,skf9(skc16)) -> ren7(skc16,x0)
% 92.22/18.99 === Backtracking. Learning clause 58:4:3:[13.3,10.1,1.1,52.5,11.1,9.1,12.1]:TopTopTop: ren9(x0),r1(x0,x1),ren6(x1,skf9(x1)) -> ren3(x1,x2)
% 92.22/18.99 === Backtracking. Learning clause 59:5:4:[30.6,34.1,33.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren10(x3,x2)
% 92.22/18.99 === Backtracking. Learning clause 60:1:1:[41.2,4.1,3.1]:Top: -> ren1(x0,skc16)
% 92.22/18.99 === Backtracking. Learning clause 61:7:5:[30.4,19.1,20.1,54.4,21.1]:TopTopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)),ren9(x3),r1(x3,x2) -> ren7(x2,x4)
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1096
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1160
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1224
% 92.22/18.99 === Conflict found: 50:4:4:[13.6,23.1,22.1,24.1,21.1]:TopTopTopTop: r1(x0,x1),ren2(x1) -> ren3(x2,x0),ren7(x1,x3) {x0 -> skf6(skc14), x1 -> skf3(skf6(skc14)), x2 -> skc14, x3 -> skf10(skf3(skf6(skc14)))}
% 92.22/18.99 === Backtracking. Learning clause 62:7:3:[50.2,8.2,31.4,11.1,10.1,9.1,28.6]:TopTopTop: ren8(x0,skf11(x0)),ren9(x0),r1(x0,x1),p1(x0),r1(x0,x2),ren1(x2,skf5(x2)) -> p1(x1)
% 92.22/18.99 === Backtracking. Learning clause 63:7:4:[31.3,19.1,24.2,20.1,30.5]:TopTopTopTop: ren9(x0),r1(x0,x1),ren8(x0,skf11(x0)),r1(x1,x2),r1(x2,x3) -> p1(skf10(skf9(x1))),p1(x3)
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1288
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1352
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1416
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1480
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1544
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1608
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1672
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1736
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1800
% 92.22/18.99 === Conflict found: 62:7:3:[50.2,8.2,31.4,11.1,10.1,9.1,28.6]:TopTopTop: ren8(x0,skf11(x0)),ren9(x0),r1(x0,x1),p1(x0),r1(x0,x2),ren1(x2,skf5(x2)) -> p1(x1) {x0 -> skc16, x1 -> skf7(skc16), x2 -> skf1(skc13)}
% 92.22/18.99 === Backtracking. Learning clause 65:6:3:[15.0,64.5,62.3,14.1]:TopTopTop: ren8(x0,skf11(x0)),ren9(x0),p1(x0),r1(x0,x1),ren1(x1,skf5(x1)) -> ren4(x0,x2)
% 92.22/18.99 === Backtracking. Learning clause 66:4:1:[41.1,14.1,15.1,29.3,17.2]:Top: ren9(x0),r1(x0,skc16),p1(skf8(x0)) -> p1(x0)
% 92.22/18.99 === Backtracking. Learning clause 67:4:2:[31.3,3.1,4.1,2.1]:TopTop: ren9(x0),ren7(skf1(x1),skf10(skf1(x1))),ren8(x0,skf11(x0)) -> ren1(x0,x1)
% 92.22/18.99 === Backtracking. Learning clause 68:7:5:[30.6,20.1,19.1,58.3]:TopTopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)),ren9(x3),r1(x3,x2) -> ren3(x2,x4)
% 92.22/18.99 === Backtracking. Learning clause 69:5:4:[30.4,3.1,4.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren1(x3,x2)
% 92.22/18.99 === Backtracking. Learning clause 70:5:4:[30.4,16.1,17.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren5(x2,x3)
% 92.22/18.99 === Backtracking. Learning clause 71:6:5:[30.6,17.1,16.1]:TopTopTopTopTop: ren9(x0),r1(x1,x2),r1(x2,x3),ren6(x1,skf9(x1)) -> ren5(x4,x3),ren5(x0,x1)
% 92.22/18.99 === Backtracking. Learning clause 72:5:4:[2.1,69.2]:TopTopTopTop: ren9(x0),r1(x1,x2),ren6(x1,skf9(x1)) -> ren1(x0,x1),ren1(x3,x2)
% 92.22/18.99 === Backtracking. Learning clause 73:5:4:[30.6,15.1,14.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren4(x2,x3)
% 92.22/18.99 === Backtracking. Learning clause 74:5:4:[30.6,26.1,25.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren8(x2,x3)
% 92.22/18.99 === Backtracking. Learning clause 76:4:2:[26.0,75.3,28.2,25.1,51.2]:TopTop: ren9(x0),p1(x0),ren3(x0,skf6(x0)) -> ren8(x0,x1)
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1864
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1928
% 92.22/18.99 === Clause set with instances from active satisfied. Growing active. New size: 1992
% 92.22/18.99 === Backtracking. Learning clause 77:2:3:[18.4,23.1,22.1,24.1,21.1]:TopTopTop: -> ren5(x0,x1),ren7(x1,x2)
% 92.22/18.99 === Backtracking. Learning clause 79:5:2:[40.0,78.0,31.2,16.1,1.1,77.2,66.3,29.4,62.4,39.1,38.1,49.1,53.4,14.2]:TopTop: r1(skc14,x0),ren9(skc14),r1(skc14,x1),ren6(x1,skf9(x1)) -> r1(x0,skf7(x0))
% 92.22/18.99
% 92.22/18.99 SZS status Unsatisfiable
% 92.22/18.99
% 92.22/18.99 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.22/18.99
% 92.22/18.99 SPASS-SCL-FOL Statistics:
% 92.22/18.99 Number of learned clauses: 33
% 92.22/18.99 Number of propagations: 13547
% 92.22/18.99 Number of decisions: 3524
% 92.22/18.99 Number of resolutions: 125
% 92.22/18.99 Number of condensations: 25
% 92.22/18.99 Number of sub resolutions: 4
% 92.22/18.99 Number of input literals (deduplicated): 38
% 92.22/18.99 Number of grows: 30
% 92.22/18.99 Number of considered ground atoms: 1992
% 92.22/18.99
% 92.22/18.99 Needed: 0:0:18.43
% 92.22/18.99
%------------------------------------------------------------------------------