%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN755-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.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 : Unsatisfiable 0.45s 0.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN755-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.35 % Computer : n031.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Thu May 7 13:51:26 EDT 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.45/0.64 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.64 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.64 Execution resolution_1 ended with status: unsatisfiable
% 0.45/0.64 Used heuristic: resolution_1
% 0.45/0.64
% 0.45/0.64 Input Clauses:
% 0.45/0.64
% 0.45/0.64 Predicates: ssRr ssPv1 ssPv2 ssPv3 ssPv4
% 0.45/0.64 Fol Constants: a
% 0.45/0.64 Fol Functions: skf1
% 0.45/0.64 Problem Properties:
% 0.45/0.64 This is a full first-order problem without equality.
% 0.45/0.64
% 0.45/0.64 After reduction: Problem Properties:
% 0.45/0.64 This is a full first-order problem without equality.
% 0.45/0.64
% 0.45/0.64
% 0.45/0.64 Reduced Input Clauses:
% 0.45/0.64 52:5:3:[24.1,12.3]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2) -> ssPv2(x0),ssPv4(x0)
% 0.45/0.64 53:5:3:[20.3,14.5]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2) -> ssPv3(x2),ssPv2(x0)
% 0.45/0.64 54:5:3:[36.1,27.4]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2),ssPv3(x0) -> ssPv1(x0)
% 0.45/0.64 55:5:3:[53.4,30.3]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2),ssPv4(x0) -> ssPv3(x2)
% 0.45/0.64
% 0.45/0.64 Most General Atoms: ssRr(x0,x3) ssPv1(x3) ssPv4(x3) ssPv2(x3) ssPv3(x3)
% 0.45/0.64
% 0.45/0.64 === Starting SPASS-SCL-FOL A Little Less Naive, considering 10 atoms initially, heuristics mode: resolution_1 ===
% 0.45/0.64
% 0.45/0.64 === Backtracking. Learning clause 56:4:1:[24.1,1.1]:Top: ssPv4(skf1(x0)),ssPv3(skf1(x0)) -> ssPv2(x0),ssPv4(x0)
% 0.45/0.64 === Conflict found: 52:5:3:[24.1,12.3]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2) -> ssPv2(x0),ssPv4(x0) {x0 -> a, x1 -> skf1(a), x2 -> skf1(a)}
% 0.45/0.64 === Backtracking. Learning clause 57:3:1:[52.1,1.1]:Top: ssPv3(skf1(x0)) -> ssPv2(x0),ssPv4(x0)
% 0.45/0.64 === Backtracking. Learning clause 58:4:1:[16.1,1.1,57.1]:Top: ssPv1(skf1(x0)) -> ssPv1(x0),ssPv2(x0),ssPv4(x0)
% 0.45/0.64 === Clause set with instances from active satisfied. Growing active. New size: 74
% 0.45/0.64 === Backtracking. Learning clause 59:4:1:[42.6,33.4,29.4,8.3,2.2,1.1]:Top: ssPv4(x0) -> ssPv1(x0),ssPv2(x0),ssPv3(x0)
% 0.45/0.64 === Conflict found: 59:4:1:[42.6,33.4,29.4,8.3,2.2,1.1]:Top: ssPv4(x0) -> ssPv1(x0),ssPv2(x0),ssPv3(x0) {x0 -> skf1(skf1(skf1(a)))}
% 0.45/0.64 === Backtracking. Learning clause 60:12:6:[59.3,13.2,8.3,1.1,58.1,57.1,42.2,16.2,15.2,29.4,54.2]:TopTopTopTopTopTop: ssRr(x0,x1),ssPv4(x0),ssRr(x2,x1),ssRr(x3,x4),ssPv4(x4),ssRr(x3,x2),ssRr(x5,x1),ssPv3(x5) -> ssPv1(x2),ssPv1(x3),ssPv3(x3),ssPv1(x5)
% 0.45/0.64 === Conflict found: 59:4:1:[42.6,33.4,29.4,8.3,2.2,1.1]:Top: ssPv4(x0) -> ssPv1(x0),ssPv2(x0),ssPv3(x0) {x0 -> skf1(a)}
% 0.45/0.64 === Backtracking. Learning clause 61:3:1:[59.3,29.4,60.8,8.3,2.2,1.1,1.1]:Top: -> ssPv1(x0),ssPv2(x0),ssPv3(x0)
% 0.45/0.64 === Conflict found: 54:5:3:[36.1,27.4]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2),ssPv3(x0) -> ssPv1(x0) {x0 -> a, x1 -> skf1(a), x2 -> skf1(a)}
% 0.45/0.64 === Backtracking. Learning clause 62:4:2:[54.4,61.3]:TopTop: ssRr(x0,x1),ssPv3(x1) -> ssPv1(x0),ssPv2(x0)
% 0.45/0.64 === Conflict found: 61:3:1:[59.3,29.4,60.8,8.3,2.2,1.1,1.1]:Top: -> ssPv1(x0),ssPv2(x0),ssPv3(x0) {x0 -> skf1(a)}
% 0.45/0.64 === Backtracking. Learning clause 63:2:1:[61.1,16.2,15.2,62.2,1.1]:Top: -> ssPv1(x0),ssPv2(x0)
% 0.45/0.64 === Backtracking. Learning clause 64:4:2:[19.4,63.2,63.1]:TopTop: ssRr(x0,x1) -> ssPv2(x1),ssPv3(x0),ssPv1(x0)
% 0.45/0.64 === Backtracking. Learning clause 65:2:1:[28.5,29.2,63.2,64.2,54.4,1.1]:Top: ssPv3(skf1(x0)) -> ssPv1(x0)
% 0.45/0.64 === Backtracking. Learning clause 67:7:4:[19.5,66.6,17.6,7.5]:TopTopTopTop: ssRr(x0,x1),ssPv4(x1),ssRr(x0,x2),ssRr(x0,x3),ssPv1(x3),ssPv2(x0) -> ssPv2(x2)
% 0.45/0.64 === Conflict found: 61:3:1:[59.3,29.4,60.8,8.3,2.2,1.1,1.1]:Top: -> ssPv1(x0),ssPv2(x0),ssPv3(x0) {x0 -> skf1(skf1(a))}
% 0.45/0.64 === Backtracking. Learning clause 68:4:2:[61.2,37.2,11.2,57.1,1.1,67.2,61.1,63.2]:TopTop: ssRr(x0,x1) -> ssPv2(x1),ssPv3(x1),ssPv1(x0)
% 0.45/0.64 === Backtracking. Learning clause 71:6:4:[67.6,69.1,63.1,70.6,51.7,5.5]:TopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv1(x2),ssRr(x0,x3),ssPv4(x3) -> ssPv1(x0)
% 0.45/0.64 === Backtracking. Learning clause 72:10:6:[31.5,37.7,71.3]:TopTopTopTopTopTop: ssPv2(x0),ssRr(x0,x1),ssPv2(x1),ssRr(x0,x2),ssRr(x0,x3),ssRr(x4,x3),ssRr(x4,x5),ssPv4(x5) -> ssPv3(x2),ssPv1(x4)
% 0.45/0.64 === Backtracking. Learning clause 73:1:1:[37.6,4.2,10.5,3.2,1.1,72.8,63.2,68.2,1.1,65.1]:Top: -> ssPv1(x0)
% 0.45/0.64 === Backtracking. Learning clause 74:5:3:[22.4,73.1]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2) -> ssPv2(x2),ssPv2(x0)
% 0.45/0.64 === Backtracking. Learning clause 75:3:1:[11.2,73.1,57.1,1.1,34.2,74.2,35.2,73.1,1.1,74.2,67.6,1.1]:Top: ssPv4(skf1(x0)),ssPv1(skf1(x0)) -> ssPv2(skf1(x0))
% 0.45/0.64 === Backtracking. Learning clause 76:3:1:[7.2,73.1,1.1]:Top: ssPv2(x0),ssPv3(x0),ssPv4(x0) ->
% 0.45/0.64 === Backtracking. Learning clause 77:2:1:[48.6,73.1,1.1,76.2,75.3]:Top: ssPv4(skf1(x0)),ssPv1(skf1(x0)) ->
% 0.45/0.64 === Backtracking. Learning clause 79:7:5:[73.0,78.1,19.6,50.6,74.5]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x0,x3),ssPv3(x3),ssRr(x0,x4) -> ssPv4(x2),ssPv2(x4)
% 0.45/0.64 === Backtracking. Learning clause 80:5:3:[21.4,73.1]:TopTopTop: ssRr(x0,x1),ssPv2(x1),ssRr(x0,x2) -> ssPv4(x2),ssPv2(x0)
% 0.45/0.64 === Backtracking. Learning clause 81:2:1:[47.6,73.1,79.7,1.1,77.1]:Top: ssPv3(skf1(x0)),ssPv1(skf1(x0)) ->
% 0.45/0.64 === Backtracking. Learning clause 83:2:1:[81.0,82.1,11.4,57.1,73.1,1.1,77.1]:Top: ssPv1(skf1(x0)) -> ssPv2(skf1(x0))
% 0.45/0.64
% 0.45/0.64 SZS status Unsatisfiable
% 0.45/0.64
% 0.45/0.64 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.64
% 0.45/0.64 SPASS-SCL-FOL Statistics:
% 0.45/0.64 Number of learned clauses: 23
% 0.45/0.64 Number of propagations: 219
% 0.45/0.64 Number of decisions: 34
% 0.45/0.64 Number of resolutions: 92
% 0.45/0.64 Number of condensations: 7
% 0.45/0.64 Number of sub resolutions: 9
% 0.45/0.64 Number of input literals (deduplicated): 6
% 0.45/0.64 Number of grows: 1
% 0.45/0.64 Number of considered ground atoms: 74
% 0.45/0.64
% 0.45/0.64 Needed: 0:00:00.10
% 0.45/0.64
%------------------------------------------------------------------------------