%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL640+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 : n011.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:04 PM UTC 2026
% Result : Theorem 77.36s 19.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL640+1.001 : TPTP v9.2.1. Released v4.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 : n011.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:34:33 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.21/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 77.36/19.80 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.36/19.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.36/19.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.36/19.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.36/19.80 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.36/19.80 Execution resolution_1 ended with status: unsatisfiable
% 77.36/19.80 Used heuristic: resolution_1
% 77.36/19.80
% 77.36/19.80 Input Clauses:
% 77.36/19.80
% 77.36/19.80 Predicates: r1 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10
% 77.36/19.80 Fol Constants: skc13 skc14 skc15 skc16
% 77.36/19.80 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf17
% 77.36/19.80 Problem Properties:
% 77.36/19.80 This is a full first-order problem without equality.
% 77.36/19.80
% 77.36/19.80 After reduction: Problem Properties:
% 77.36/19.80 This is a full first-order problem without equality.
% 77.36/19.80
% 77.36/19.80
% 77.36/19.80 Reduced Input Clauses:
% 77.36/19.80
% 77.36/19.80 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)
% 77.36/19.80
% 77.36/19.80 === Starting SPASS-SCL-FOL A Little Less Naive, considering 61 atoms initially, heuristics mode: resolution_1 ===
% 77.36/19.80
% 77.36/19.80 === Backtracking. Learning clause 42:1:0:[35.1,36.1]:: -> ren9(skc14)
% 77.36/19.80 === Backtracking. Learning clause 43:2:1:[35.1,2.1]:Top: -> ren9(skf1(skc13)),ren1(x0,skc13)
% 77.36/19.80 === Backtracking. Learning clause 46:5:5:[4.0,44.2,3.0,45.4,12.3,2.1]:TopTopTopTopTop: r1(x0,x1),r1(x1,x2),ren2(x1) -> ren3(x3,x0),ren1(x4,x2)
% 77.36/19.80 === Backtracking. Learning clause 47:2:1:[35.1,21.1]:Top: -> ren9(skf4(skc13)),ren7(x0,skc13)
% 77.36/19.80 === Backtracking. Learning clause 48:2:1:[32.1,35.1]:Top: -> ren10(x0,skc13),ren9(skf12(skc13))
% 77.36/19.80 === Backtracking. Learning clause 50:1:1:[3.0,49.1,2.1,40.1]:Top: -> ren1(x0,skc16)
% 77.36/19.80 === Backtracking. Learning clause 51:1:0:[40.1,5.1,6.1]:: -> ren2(skc16)
% 77.36/19.80 === Backtracking. Learning clause 53:1:1:[10.0,52.1,9.1,40.1]:Top: -> ren3(x0,skc16)
% 77.36/19.80 === Backtracking. Learning clause 55:1:1:[22.0,54.1,21.1,40.1]:Top: -> ren7(x0,skc16)
% 77.36/19.80 === Backtracking. Learning clause 57:1:1:[33.0,56.1,32.1,40.1]:Top: -> ren10(x0,skc16)
% 77.36/19.80 === Backtracking. Learning clause 58:7:3:[27.6,11.2]:TopTopTop: ren9(x0),r1(x0,x1),p1(x0),r1(x0,x2),ren1(x2,skf5(x2)) -> p1(x1),p1(skf6(x0))
% 77.36/19.80 === Backtracking. Learning clause 60:5:4:[22.0,59.4,29.5,19.2,21.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),p1(skf9(x1)) -> ren7(x3,x2)
% 77.36/19.80 === Backtracking. Learning clause 62:5:4:[3.0,61.4,29.5,19.2,2.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),p1(skf9(x1)) -> ren1(x3,x2)
% 77.36/19.80 === Backtracking. Learning clause 63:2:1:[35.1,9.1]:Top: -> ren9(skf3(skc13)),ren3(x0,skc13)
% 77.36/19.80 === Backtracking. Learning clause 66:5:5:[11.0,64.2,10.0,65.4,12.3,9.1]:TopTopTopTopTop: r1(x0,x1),r1(x1,x2),ren2(x1) -> ren3(x3,x0),ren3(x4,x2)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 69
% 77.36/19.80 === Restarting.
% 77.36/19.80 === Backtracking. Learning clause 67:3:1:[33.2,41.2]:Top: p1(skf12(skf17(x0))),r1(skc14,x0) -> p1(x0)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 133
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 197
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 261
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 325
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 389
% 77.36/19.80 === Backtracking. Learning clause 69:3:3:[7.0,68.1,17.4,6.1,5.1]:TopTopTop: r1(x0,x1) -> ren5(x2,x0),ren2(x1)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 453
% 77.36/19.80 === Backtracking. Learning clause 70:4:3:[17.2,32.1,34.1,31.1,67.1]:TopTopTop: r1(skc14,x0) -> ren5(x1,x2),ren10(x2,skf17(x0)),p1(x0)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 517
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 581
% 77.36/19.80 === Backtracking. Learning clause 72:2:3:[33.0,71.0,26.2,32.1,31.1,34.1]:TopTopTop: -> ren8(x0,x1),ren10(x1,x2)
% 77.36/19.80 === Backtracking. Learning clause 73:2:2:[41.2,70.3,16.1]:TopTop: r1(skc14,x0) -> ren5(x1,x0)
% 77.36/19.80 === Backtracking. Learning clause 74:4:4:[17.4,25.1,24.1]:TopTopTopTop: r1(x0,x1),p1(x1) -> ren5(x2,x0),ren8(x1,x3)
% 77.36/19.80 === Backtracking. Learning clause 75:4:4:[17.2,18.1,19.1]:TopTopTopTop: r1(x0,x1),p1(x1) -> ren5(x2,x0),ren6(x1,x3)
% 77.36/19.80 === Backtracking. Learning clause 76:4:4:[17.2,15.1,16.1]:TopTopTopTop: r1(x0,x1),p1(x1) -> ren5(x2,x0),ren5(x1,x3)
% 77.36/19.80 === Backtracking. Learning clause 77:1:1:[40.2,14.1,13.1]:Top: -> ren4(skc16,x0)
% 77.36/19.80 === Backtracking. Learning clause 78:1:1:[40.2,16.1,15.1]:Top: -> ren5(skc16,x0)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 645
% 77.36/19.80 === Backtracking. Learning clause 79:7:6:[29.4,2.1,3.1,75.4]:TopTopTopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),r1(x3,x1),p1(x1) -> ren1(x4,x2),ren5(x5,x3)
% 77.36/19.80 === Backtracking. Learning clause 80:2:0:[35.2,62.1,1.1]:: p1(skf9(skc13)) -> ren1(skc13,skc13)
% 77.36/19.80 === Backtracking. Learning clause 81:1:1:[40.1,18.1,19.1]:Top: -> ren6(skc16,x0)
% 77.36/19.80 === Backtracking. Learning clause 82:1:1:[40.2,25.1,24.1]:Top: -> ren8(skc16,x0)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 709
% 77.36/19.80 === Backtracking. Learning clause 83:1:1:[15.1,73.1,28.4,39.1,16.1,77.1,42.1]:Top: -> ren5(x0,skc14)
% 77.36/19.80 === Backtracking. Learning clause 84:4:3:[29.6,3.1,1.1,2.1]:TopTopTop: ren9(x0),r1(x0,x1),ren6(x1,skf9(x1)) -> ren1(x1,x2)
% 77.36/19.80 === Backtracking. Learning clause 85:6:4:[19.2,29.5,7.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),r1(x2,x3) -> p1(x3),ren2(skf9(x1))
% 77.36/19.80 === Backtracking. Learning clause 87:3:1:[42.0,86.0,15.1,73.1,28.4]:Top: r1(skc14,x0),ren4(x0,skf7(x0)) -> p1(skc14)
% 77.36/19.80 === Backtracking. Learning clause 88:5:4:[29.6,33.1,32.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren10(x3,x2)
% 77.36/19.80 === Backtracking. Learning clause 89:5:4:[29.4,21.1,22.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren7(x3,x2)
% 77.36/19.80 === Backtracking. Learning clause 90:1:1:[15.1,73.1]:Top: -> ren5(skc14,x0)
% 77.36/19.80 === Backtracking. Learning clause 91:5:4:[29.6,10.1,9.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren3(x3,x2)
% 77.36/19.80 === Backtracking. Learning clause 92:5:3:[29.6,6.1,5.1]:TopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren2(x2)
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 773
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 837
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 901
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 965
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 1029
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 1093
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 1157
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 1221
% 77.36/19.80 === Clause set with instances from active satisfied. Growing active. New size: 1285
% 77.36/19.80 === Backtracking. Learning clause 93:4:3:[29.3,31.1,33.1,32.1]:TopTopTop: ren9(x0),r1(x0,x1),ren6(x1,skf9(x1)) -> ren10(x1,x2)
% 77.36/19.80 === Backtracking. Learning clause 94:4:3:[8.1,91.3]:TopTopTop: ren9(x0),r1(x0,x1),ren6(x1,skf9(x1)) -> ren3(x1,x2)
% 77.36/19.80 === Backtracking. Learning clause 95:5:4:[29.4,15.1,16.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren5(x2,x3)
% 77.36/19.80 === Conflict found: 76:4:4:[17.2,15.1,16.1]:TopTopTopTop: r1(x0,x1),p1(x1) -> ren5(x2,x0),ren5(x1,x3) {x0 -> skf1(skc13), x1 -> skf2(skf1(skc13)), x2 -> skf2(skf1(skc13)), x3 -> skf1(skc13)}
% 77.36/19.80 === Backtracking. Learning clause 96:3:4:[76.2,34.1,31.1]:TopTopTopTop: -> ren5(x0,x1),ren5(x2,x3),ren10(x1,x2)
% 77.36/19.80 === Backtracking. Learning clause 97:2:1:[11.1,80.1]:Top: -> ren3(x0,skf9(skc13)),ren1(skc13,skc13)
% 77.36/19.81 === Backtracking. Learning clause 99:1:1:[25.0,98.0,41.2,72.2,24.1]:Top: -> ren8(skc14,x0)
% 77.36/19.81 === Backtracking. Learning clause 100:3:2:[29.5,81.1,10.1,9.1,8.1]:TopTop: ren9(x0),r1(x0,skc16) -> ren3(skc16,x1)
% 77.36/19.81 === Backtracking. Learning clause 101:1:1:[23.1,38.1]:Top: -> ren7(x0,skc15)
% 77.36/19.81 === Backtracking. Learning clause 102:2:1:[29.2,39.1,42.1,9.1,10.1,8.1]:Top: ren6(skc16,skf9(skc16)) -> ren3(skc16,x0)
% 77.36/19.81 === Backtracking. Learning clause 103:4:3:[20.1,89.3]:TopTopTop: ren9(x0),r1(x0,x1),ren6(x1,skf9(x1)) -> ren7(x1,x2)
% 77.36/19.81 === Backtracking. Learning clause 104:6:2:[29.6,3.1,2.1,27.5,4.1,3.1,2.1,35.2,1.1]:TopTop: ren9(x0),r1(x0,x1),r1(x1,skf5(skc13)),ren6(x1,skf9(x1)),ren3(skc13,skf6(skc13)) -> ren1(skc13,skc13)
% 77.36/19.81 === Backtracking. Learning clause 105:5:4:[29.4,2.1,3.1]:TopTopTopTop: ren9(x0),r1(x0,x1),r1(x1,x2),ren6(x1,skf9(x1)) -> ren1(x3,x2)
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1349
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1413
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1477
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1541
% 77.36/19.81 === Backtracking. Learning clause 106:2:3:[17.4,22.1,23.1,20.1,21.1]:TopTopTop: -> ren5(x0,x1),ren7(x1,x2)
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1605
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1669
% 77.36/19.81 === Clause set with instances from active satisfied. Growing active. New size: 1733
% 77.36/19.81
% 77.36/19.81 SZS status Unsatisfiable
% 77.36/19.81
% 77.36/19.81 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.36/19.81
% 77.36/19.81 SPASS-SCL-FOL Statistics:
% 77.36/19.81 Number of learned clauses: 51
% 77.36/19.81 Number of propagations: 10385
% 77.36/19.81 Number of decisions: 3608
% 77.36/19.81 Number of resolutions: 126
% 77.36/19.81 Number of condensations: 28
% 77.36/19.81 Number of sub resolutions: 14
% 77.36/19.81 Number of input literals (deduplicated): 37
% 77.36/19.81 Number of grows: 27
% 77.36/19.81 Number of considered ground atoms: 1733
% 77.36/19.81
% 77.36/19.81 Needed: 0:0:19.23
% 77.36/19.81
%------------------------------------------------------------------------------