%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN532-1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/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:39:58 PM UTC 2026
% Result : Satisfiable 0.15s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SYN532-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.07 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.25 % Computer : n012.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Thu May 7 13:45:16 EDT 2026
% 0.07/0.26 % CPUTime :
% 0.07/0.26 SPASS-SCL-FOL version:
% 0.07/0.31 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.15/0.38 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38 Execution normal ended with status: satisfiable
% 0.15/0.38 Used heuristic: normal
% 0.15/0.38
% 0.15/0.38 Input Clauses:
% 0.15/0.38
% 0.15/0.38 Predicates: ndr1_0 c3_0 c4_0 ssSkC6 ssSkC5 ssSkC3 ssSkC1 ssSkC0 c5_0 c1_0 c5_1 ssSkC4 ndr1_1 c4_1 ssSkC2 ssSkP1 ssSkP0 c2_1 c1_1 c3_1 c1_2 c2_0 c3_2 c5_2 c4_2 c2_2
% 0.15/0.38 Fol Constants: a439 a420 a437 a434 a425 a416 a440 a438 a432 a431 a421 a418 a436 a435 a429 a427 a426 a412 a419 a411 a428 a433 a415 a413 a414 a417 a430 a441 a442 a424
% 0.15/0.38 Fol Functions:
% 0.15/0.38 Problem Properties:
% 0.15/0.38 This is a Bernays Schoenfinkel problem.
% 0.15/0.38
% 0.15/0.38 After reduction: Problem Properties:
% 0.15/0.38 This is a Bernays Schoenfinkel problem.
% 0.15/0.38
% 0.15/0.38
% 0.15/0.38 Reduced Input Clauses:
% 0.15/0.38 103:1:0:[4.1,10.0,3.1,102.1]:: -> ndr1_0
% 0.15/0.38 137:9:3:[2.0,101.5]:TopTopTop: c2_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c4_2(x0,x2),c2_2(x0,x2),c3_0 -> c1_2(x0,x1),c5_2(x0,x2),c4_0
% 0.15/0.38 136:6:2:[2.0,100.1,121.4,135.3]:TopTop: c1_1(x0),c4_2(a441,x1) -> c5_1(x0),c2_1(x0),c5_2(a441,x1),c4_0
% 0.15/0.38 104:2:0:[1.1,31.0]:: -> ndr1_0,c5_0
% 0.15/0.38 134:7:2:[103.2,99.1]:TopTop: c4_1(x0),c5_2(x1,a424) -> c5_1(x0),c2_1(x0),c2_1(x1),c3_1(x1),c5_0
% 0.15/0.38 105:2:0:[103.2,68.2]:: ssSkC0,c2_1(a413) ->
% 0.15/0.38 106:2:0:[16.1,69.0]:: c3_0,c5_0 ->
% 0.15/0.38 107:3:1:[103.2,72.2]:Top: ssSkC0,c2_1(x0) -> ndr1_1(a413)
% 0.15/0.38 108:3:1:[103.2,73.1]:Top: c2_1(x0) -> ndr1_1(x0),ssSkC2
% 0.15/0.38 111:2:1:[20.1,74.0,19.1,109.1,103.2,110.2]:Top: -> ndr1_1(x0),ssSkC4
% 0.15/0.38 112:3:1:[103.2,75.2]:Top: ssSkC0,c2_1(x0) -> c1_2(a413,a414)
% 0.15/0.38 113:3:1:[103.2,76.1]:Top: c2_1(x0) -> c2_2(x0,a417),ssSkC2
% 0.15/0.38 114:4:1:[103.2,78.2]:Top: ssSkP0(x0),ssSkP1(x0) -> c1_2(x0,a430),ssSkC4
% 0.15/0.38 115:4:1:[103.2,79.2]:Top: ssSkP0(x0),ssSkP1(x0) -> c5_2(x0,a430),ssSkC4
% 0.15/0.38 116:3:1:[103.2,80.2]:Top: ssSkC0,c2_1(x0),c3_2(a413,a414) ->
% 0.15/0.38 117:3:1:[103.2,81.2]:Top: ssSkC0,c2_1(x0),c5_2(a413,a414) ->
% 0.15/0.38 118:3:1:[103.2,82.2]:Top: c4_2(x0,a417),c2_1(x0) -> ssSkC2
% 0.15/0.38 119:4:1:[103.2,83.1]:Top: c3_1(x0),c3_0,c4_0 -> c5_1(x0)
% 0.15/0.38 120:4:1:[103.2,84.3]:Top: ssSkP0(x0),ssSkP1(x0),c4_2(x0,a430) -> ssSkC4
% 0.15/0.38 121:5:1:[2.0,85.1]:Top: c1_1(x0) -> c5_1(x0),c2_1(x0),ndr1_1(a441),c4_0
% 0.15/0.38 122:5:1:[2.0,86.1]:Top: c1_1(x0) -> c5_1(x0),c2_1(x0),c2_1(a441),c4_0
% 0.15/0.38 123:5:1:[2.0,88.1]:Top: c1_1(x0) -> c5_1(x0),c2_1(x0),c3_2(a441,a442),c4_0
% 0.15/0.38 124:3:1:[71.1,89.0]:Top: c2_2(a416,x0),ndr1_1(a416) -> ssSkC1
% 0.15/0.38 125:5:1:[2.0,90.1]:Top: c1_1(x0),c1_2(a441,a442) -> c5_1(x0),c2_1(x0),c4_0
% 0.15/0.38 126:7:2:[103.2,91.1]:TopTop: c4_1(x0) -> c5_1(x0),c2_1(x0),ndr1_1(x1),c2_1(x1),c3_1(x1),c5_0
% 0.15/0.38 127:5:1:[26.0,93.1]:Top: c2_2(a432,x0) -> c5_2(a432,x0),c4_2(a432,x0),c1_0,c5_0
% 0.15/0.38 128:5:1:[106.2,94.5]:Top: ndr1_1(a411),c3_0 -> c1_2(a411,x0),c3_2(a411,x0),c5_2(a411,x0)
% 0.15/0.38 129:7:2:[103.2,95.1]:TopTop: c4_1(x0) -> c5_1(x0),c2_1(x0),c2_2(x1,a424),c2_1(x1),c3_1(x1),c5_0
% 0.15/0.38 130:4:1:[18.0,96.2]:Top: c4_2(a434,x0),c3_2(a434,x0) -> c2_2(a434,x0),ssSkC5
% 0.15/0.38 132:4:2:[103.2,97.2,107.3,131.4]:TopTop: ssSkC0,c2_1(x0),c1_2(a413,x1) -> c5_2(a413,x1)
% 0.15/0.38 133:7:2:[103.2,98.1]:TopTop: c4_1(x0),c3_2(x1,a424) -> c5_1(x0),c2_1(x0),c2_1(x1),c3_1(x1),c5_0
% 0.15/0.38
% 0.15/0.38 Most General Atoms: ndr1_0 c3_0 c4_0 ssSkC6 ssSkC5 ssSkC3 ssSkC1 ssSkC0 c5_0 c1_0 c3_2(x0,x1) c4_2(x0,x2) c2_2(x0,x2) c1_2(x0,x1) c5_2(x0,x2) c1_1(x0) c5_1(x0) ssSkP1(x0) ssSkP0(x0) ssSkC4 ssSkC2 c2_0 c4_1(x0) c2_1(x1) c3_1(x0) ndr1_1(x1)
% 0.15/0.38
% 0.15/0.38 === Starting SPASS-SCL-FOL A Little Less Naive, considering 120 atoms initially, heuristics mode: normal ===
% 0.15/0.38
% 0.15/0.38 === Conflict found: 132:4:2:[103.2,97.2,107.3,131.4]:TopTop: ssSkC0,c2_1(x0),c1_2(a413,x1) -> c5_2(a413,x1) {x0 -> a411, x1 -> a414}
% 0.15/0.38 === Backtracking. Learning clause 138:2:1:[132.3,112.3,117.3]:Top: ssSkC0,c2_1(x0) ->
% 0.15/0.38
% 0.15/0.38 Linear Model Building succeeded.
% 0.15/0.38 SZS status Satisfiable
% 0.15/0.38
% 0.15/0.38 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38
% 0.15/0.38 SPASS-SCL-FOL Statistics:
% 0.15/0.38 Number of learned clauses: 1
% 0.15/0.38 Number of propagations: 42
% 0.15/0.38 Number of decisions: 118
% 0.15/0.38 Number of resolutions: 2
% 0.15/0.38 Number of condensations: 1
% 0.15/0.38 Number of sub resolutions: 36
% 0.15/0.38 Number of input literals (deduplicated): 120
% 0.15/0.38 Number of grows: 0
% 0.15/0.38 Number of considered ground atoms: 120
% 0.15/0.38
% 0.15/0.38 Needed: 0:00:00.00
% 0.15/0.38
%------------------------------------------------------------------------------