%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN757-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:40:14 PM UTC 2026
% Result : Satisfiable 51.58s 13.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SYN757-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.27 % Computer : n012.cluster.edu
% 0.09/0.27 % Model : x86_64 x86_64
% 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.27 % Memory : 8042.1875MB
% 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.27 % CPULimit : 300
% 0.09/0.27 % WCLimit : 300
% 0.09/0.27 % DateTime : Thu May 7 13:49:16 EDT 2026
% 0.09/0.27 % CPUTime :
% 0.09/0.27 SPASS-SCL-FOL version:
% 0.09/0.32 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 51.58/13.31 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.58/13.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.58/13.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.58/13.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.58/13.31 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.58/13.31 Execution lmodel_grow ended with status: satisfiable
% 51.58/13.31 Used heuristic: lmodel_grow
% 51.58/13.31
% 51.58/13.31 Input Clauses:
% 51.58/13.31
% 51.58/13.31 Predicates: ssRr ssPv3 ssPv2 ssPv4 ssPv1
% 51.58/13.31 Fol Constants: a
% 51.58/13.31 Fol Functions: skf1
% 51.58/13.31 Problem Properties:
% 51.58/13.31 This is a full first-order problem without equality.
% 51.58/13.31
% 51.58/13.31 After reduction: Problem Properties:
% 51.58/13.31 This is a full first-order problem without equality.
% 51.58/13.31
% 51.58/13.31
% 51.58/13.31 Reduced Input Clauses:
% 51.58/13.31 52:4:2:[9.2,5.3]:TopTop: ssRr(x0,x1),ssPv4(x1) -> ssPv1(x0),ssPv3(x0)
% 51.58/13.31 53:5:3:[17.1,11.3]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv4(x1),ssPv2(x0),ssPv4(x0)
% 51.58/13.31 54:5:3:[20.1,12.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv2(x2),ssPv1(x0),ssPv2(x0)
% 51.58/13.31 55:5:3:[22.3,13.5]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv2(x0) -> ssPv3(x1),ssPv1(x2)
% 51.58/13.31 56:5:3:[54.4,16.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv3(x1),ssPv2(x2),ssPv2(x0)
% 51.58/13.31 57:5:3:[56.3,21.1]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv2(x2),ssPv1(x0),ssPv2(x0)
% 51.58/13.31 58:5:3:[53.4,27.3]:TopTopTop: ssRr(x0,x1),ssPv2(x1),ssRr(x0,x2) -> ssPv4(x2),ssPv4(x0)
% 51.58/13.31 59:5:3:[54.4,29.3]:TopTopTop: ssRr(x0,x1),ssPv2(x1),ssRr(x0,x2) -> ssPv2(x2),ssPv2(x0)
% 51.58/13.31 61:6:4:[58.4,50.1]:TopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv2(x2),ssRr(x0,x3) -> ssPv2(x3),ssPv4(x0)
% 51.58/13.31 60:6:4:[47.1,46.4]:TopTopTopTop: ssRr(x0,x1),ssPv1(x1),ssRr(x0,x2),ssRr(x0,x3) -> ssPv1(x3),ssPv4(x0)
% 51.58/13.31
% 51.58/13.31 Most General Atoms: ssPv4(x2) ssRr(x0,x3) ssPv1(x3) ssPv2(x3) ssPv3(x3)
% 51.58/13.31
% 51.58/13.31 === Starting SPASS-SCL-FOL A Little Less Naive, considering 54 atoms initially, heuristics mode: lmodel_grow ===
% 51.58/13.31
% 51.58/13.31 === Backtracking. Learning clause 62:14:8:[23.4,58.5,55.5,15.3,55.3,43.2,56.4,30.2]:TopTopTopTopTopTopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2),ssRr(x1,x3),ssRr(x4,x2),ssRr(x4,x5),ssRr(x6,x2),ssRr(x6,x7),ssPv4(x6) -> ssPv3(x3),ssPv3(x5),ssPv2(x4),ssPv3(x7),ssPv1(x6)
% 51.58/13.31 === Backtracking. Learning clause 63:4:2:[41.6,18.2,15.4,7.3]:TopTop: ssRr(x0,x1),ssPv3(x0) -> ssPv3(x1),ssPv2(x0)
% 51.58/13.31 === Backtracking. Learning clause 64:5:3:[23.6,28.2,55.5,2.5,63.2]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2) -> ssPv3(x2),ssPv2(x1)
% 51.58/13.31 === Backtracking. Learning clause 65:10:5:[37.4,35.6]:TopTopTopTopTop: ssRr(x0,x1),ssPv4(x1),ssRr(x0,x2),ssPv1(x0),ssPv3(x0),ssRr(x3,x4),ssPv1(x4),ssRr(x3,x2),ssPv1(x3),ssPv2(x3) ->
% 51.58/13.31 === Backtracking. Learning clause 68:11:6:[55.4,66.6,64.4,67.7,43.2,52.3,30.2,34.5,65.5,30.6,49.6]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv4(x2),ssRr(x1,x3),ssPv2(x1),ssRr(x3,x4),ssRr(x3,x5),ssPv4(x3) -> ssPv2(x0),ssPv1(x2),ssPv3(x5)
% 51.58/13.31 === Backtracking. Learning clause 69:8:5:[48.5,58.5,35.4,34.2,22.6,64.5]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv3(x1),ssRr(x3,x1),ssPv2(x3),ssRr(x1,x4) -> ssPv4(x2),ssPv3(x4)
% 51.58/13.31 === Conflict found: 58:5:3:[53.4,27.3]:TopTopTop: ssRr(x0,x1),ssPv2(x1),ssRr(x0,x2) -> ssPv4(x2),ssPv4(x0) {x0 -> skf1(a), x1 -> skf1(skf1(a)), x2 -> skf1(skf1(a))}
% 51.58/13.31 === Backtracking. Learning clause 70:9:5:[58.5,49.5,64.5,55.5,69.3,68.8]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv4(x2),ssRr(x1,x3),ssPv2(x1),ssRr(x3,x4) -> ssPv2(x0),ssPv1(x2),ssPv3(x4)
% 51.58/13.31 === Backtracking. Learning clause 71:7:4:[34.4,63.4,8.4,37.6,32.5,6.5,58.4]:TopTopTopTop: ssRr(x0,x1),ssPv3(x0),ssRr(x1,x2),ssRr(x2,x3),ssPv2(x2) -> ssPv4(x1),ssPv4(x3)
% 51.58/13.31 === Backtracking. Learning clause 72:7:4:[15.6,22.3]:TopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x0,x3),ssPv3(x0) -> ssPv4(x1),ssPv3(x2),ssPv1(x3)
% 51.58/13.31 === Conflict found: 58:5:3:[53.4,27.3]:TopTopTop: ssRr(x0,x1),ssPv2(x1),ssRr(x0,x2) -> ssPv4(x2),ssPv4(x0) {x0 -> skf1(skf1(skf1(skf1(skf1(a))))), x1 -> skf1(skf1(skf1(skf1(skf1(skf1(a)))))), x2 -> skf1(skf1(skf1(skf1(skf1(skf1(a))))))}
% 51.58/13.31 === Backtracking. Learning clause 73:17:10:[58.5,48.5,3.4,32.4,69.8]:TopTopTopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv3(x2),ssRr(x1,x3),ssRr(x4,x5),ssRr(x4,x3),ssRr(x6,x7),ssRr(x6,x8),ssPv3(x7),ssRr(x9,x7),ssPv2(x9),ssRr(x7,x5) -> ssPv1(x1),ssPv4(x1),ssPv1(x4),ssPv4(x4),ssPv4(x8)
% 51.58/13.31 === Backtracking. Learning clause 74:6:4:[49.5,58.5,37.6,8.4,32.5,58.4]:TopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv3(x2),ssRr(x1,x3),ssPv2(x3) -> ssPv4(x1)
% 51.58/13.31 === Backtracking. Learning clause 76:12:8:[58.4,75.2,9.4,49.2,34.5,74.3,58.4]:TopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x2,x3),ssPv2(x3),ssRr(x2,x4),ssPv2(x2),ssRr(x5,x6),ssRr(x6,x4),ssRr(x6,x7),ssPv2(x7) -> ssPv4(x1),ssPv4(x6)
% 51.58/13.31 === Conflict found: 64:5:3:[23.6,28.2,55.5,2.5,63.2]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2) -> ssPv3(x2),ssPv2(x1) {x0 -> skf1(skf1(skf1(skf1(skf1(a))))), x1 -> skf1(skf1(skf1(skf1(skf1(skf1(a)))))), x2 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))}
% 51.58/13.31 === Backtracking. Learning clause 77:13:9:[64.5,76.6,74.3]:TopTopTopTopTopTopTopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x2,x3),ssRr(x2,x1),ssRr(x1,x4),ssPv2(x4),ssRr(x1,x5),ssRr(x6,x7),ssRr(x7,x5),ssRr(x7,x8),ssPv2(x8) -> ssPv4(x3),ssPv4(x7)
% 51.58/13.31 === Backtracking. Learning clause 78:18:11:[49.5,76.11,55.5]:TopTopTopTopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x0,x3),ssRr(x4,x0),ssRr(x4,x5),ssRr(x5,x6),ssPv2(x6),ssRr(x5,x7),ssPv2(x5),ssRr(x0,x7),ssRr(x0,x8),ssPv2(x8),ssRr(x9,x10),ssRr(x9,x1),ssPv2(x9) -> ssPv4(x2),ssPv3(x3),ssPv3(x10)
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 64
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 72
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 74
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 75
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 76
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 77
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 83
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 84
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 89
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 91
% 51.58/13.31 === Conflict found: 73:17:10:[58.5,48.5,3.4,32.4,69.8]:TopTopTopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv3(x2),ssRr(x1,x3),ssRr(x4,x5),ssRr(x4,x3),ssRr(x6,x7),ssRr(x6,x8),ssPv3(x7),ssRr(x9,x7),ssPv2(x9),ssRr(x7,x5) -> ssPv1(x1),ssPv4(x1),ssPv1(x4),ssPv4(x4),ssPv4(x8) {x0 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a))))))))), x1 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))))), x2 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))))), x3 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a))))))))))), x4 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))))), x5 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a))))))))))), x6 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a))))))))), x7 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))))), x8 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))))), x9 -> skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(skf1(a)))))))))}
% 51.58/13.31 === Backtracking. Learning clause 79:5:2:[73.4,1.1]:TopTop: ssPv3(x0),ssRr(x1,x0),ssPv2(x1) -> ssPv1(x0),ssPv4(x0)
% 51.58/13.31 === Backtracking. Learning clause 80:4:3:[2.4,63.2,76.6,74.3]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(x2) -> ssPv4(x1)
% 51.58/13.31 === Conflict found: 70:9:5:[58.5,49.5,64.5,55.5,69.3,68.8]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv4(x2),ssRr(x1,x3),ssPv2(x1),ssRr(x3,x4) -> ssPv2(x0),ssPv1(x2),ssPv3(x4) {x0 -> skf1(skf1(a)), x1 -> skf1(skf1(skf1(a))), x2 -> skf1(skf1(a)), x3 -> skf1(skf1(skf1(skf1(a)))), x4 -> skf1(skf1(skf1(skf1(skf1(a)))))}
% 51.58/13.31 === Backtracking. Learning clause 82:12:7:[80.3,81.7,70.9,33.4,57.3]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssPv4(x0),ssRr(x1,x2),ssRr(x2,x3),ssRr(x3,x4),ssPv2(x4),ssRr(x3,x5),ssRr(x6,x1) -> ssPv1(x0),ssPv3(x5),ssPv1(x6),ssPv2(x6)
% 51.58/13.31 === Backtracking. Learning clause 83:10:6:[4.5,64.2,25.3,64.4]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssRr(x0,x3),ssRr(x4,x5),ssPv2(x4),ssRr(x5,x0) -> ssPv3(x2),ssPv2(x1),ssPv3(x3),ssPv2(x5)
% 51.58/13.31 === Conflict found: 56:5:3:[54.4,16.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv3(x1),ssPv2(x2),ssPv2(x0) {x0 -> skf1(skf1(skf1(skf1(a)))), x1 -> skf1(skf1(skf1(skf1(skf1(a))))), x2 -> skf1(skf1(skf1(skf1(skf1(a)))))}
% 51.58/13.31 === Backtracking. Learning clause 84:7:5:[56.5,64.2,33.4,78.9,80.4]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x3,x0),ssRr(x0,x4),ssPv2(x4) -> ssPv4(x1),ssPv3(x2)
% 51.58/13.31 === Backtracking. Learning clause 85:9:5:[38.2,56.3]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv1(x2),ssPv1(x0),ssPv3(x0),ssRr(x3,x1),ssRr(x3,x4) -> ssPv2(x4),ssPv2(x3)
% 51.58/13.31 === Backtracking. Learning clause 86:9:7:[48.7,35.4,80.4,84.7,49.5,57.4,56.5,84.5]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x0),ssRr(x1,x3),ssRr(x1,x4),ssRr(x1,x5),ssRr(x3,x6) -> ssPv4(x4),ssPv3(x5),ssPv2(x6)
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 99
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 101
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 103
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 108
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 109
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 115
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 116
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 118
% 51.58/13.31 === Clause set with instances from active satisfied. Growing active. New size: 119
% 51.58/13.31
% 51.58/13.31 Linear Model Building succeeded.
% 51.58/13.31 SZS status Satisfiable
% 51.58/13.31
% 51.58/13.31 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.58/13.31
% 51.58/13.31 SPASS-SCL-FOL Statistics:
% 51.58/13.31 Number of learned clauses: 21
% 51.58/13.31 Number of propagations: 337
% 51.58/13.31 Number of decisions: 81
% 51.58/13.31 Number of resolutions: 76
% 51.58/13.31 Number of condensations: 19
% 51.58/13.31 Number of sub resolutions: 14
% 51.58/13.31 Number of input literals (deduplicated): 6
% 51.58/13.31 Number of grows: 19
% 51.58/13.31 Number of considered ground atoms: 119
% 51.58/13.31
% 51.58/13.31 Needed: 0:0:12.88
% 51.58/13.31
%------------------------------------------------------------------------------