%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN535-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 : 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:39:59 PM UTC 2026
% Result : Satisfiable 0.37s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : SYN535-1 : TPTP v9.2.1. Released v2.1.0.
% 0.13/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.37 % Computer : n011.cluster.edu
% 0.20/0.37 % Model : x86_64 x86_64
% 0.20/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.37 % Memory : 8042.1875MB
% 0.20/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.20/0.37 % CPULimit : 300
% 0.20/0.37 % WCLimit : 300
% 0.20/0.37 % DateTime : Thu May 7 13:44:48 EDT 2026
% 0.20/0.37 % CPUTime :
% 0.20/0.37 SPASS-SCL-FOL version:
% 0.30/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.37/0.58 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.58 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.58 Execution resolution_1 ended with status: satisfiable
% 0.37/0.58 Used heuristic: resolution_1
% 0.37/0.58
% 0.37/0.58 Input Clauses:
% 0.37/0.58
% 0.37/0.58 Predicates: ndr1_0 c1_0 c3_0 c4_0 ssSkC8 ssSkC7 ssSkC6 ssSkC5 ssSkC4 ssSkC2 ssSkC0 c2_0 ssSkC3 ndr1_1 c2_1 c4_1 c1_1 c3_1 c5_1 ssSkC1 c4_2 c2_2 c5_0 c3_2 c5_2 c1_2
% 0.37/0.58 Fol Constants: a495 a517 a513 a507 a500 a492 a516 a514 a508 a499 a498 a496 a518 a511 a509 a501 a519 a515 a512 a494 a493 a506 a503 a504 a505 a497 a502 a510
% 0.37/0.58 Fol Functions:
% 0.37/0.58 Problem Properties:
% 0.37/0.58 This is a Bernays Schoenfinkel problem.
% 0.37/0.58
% 0.37/0.58 After reduction: Problem Properties:
% 0.37/0.58 This is a Bernays Schoenfinkel problem.
% 0.37/0.58
% 0.37/0.58
% 0.37/0.58 Reduced Input Clauses:
% 0.37/0.58 101:1:0:[11.0,1.1]:: -> ndr1_0
% 0.37/0.58 128:7:2:[101.0,100.2,108.4,127.5]:TopTop: c3_1(x0),c1_1(x0),c3_2(a503,x1),c5_2(a503,x1) -> c2_1(x0),c1_2(a503,x1),c2_0
% 0.37/0.58 126:8:3:[101.0,99.5]:TopTopTop: c3_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c4_1(x0),c1_1(x0),c2_0 -> c5_2(x0,x1),c5_1(x2)
% 0.37/0.58 125:8:3:[101.0,98.4]:TopTopTop: ssSkC5,c4_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c3_2(x2,a510),c3_1(x2) -> c3_1(x0),c2_1(x2)
% 0.37/0.58 124:8:3:[101.0,97.4]:TopTopTop: ssSkC5,c4_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c2_2(x2,a510),c3_1(x2) -> c3_1(x0),c2_1(x2)
% 0.37/0.58 123:7:2:[101.0,96.5]:TopTop: c4_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c4_1(x0),c3_1(x0),c4_0,c5_0 ->
% 0.37/0.58 122:8:2:[101.0,95.4]:TopTop: ssSkC2,c4_2(x0,x1),ndr1_1(x0),c3_2(x0,a502),c2_0 -> c3_2(x0,x1),c1_2(x0,x1),c5_1(x0)
% 0.37/0.58 121:8:2:[101.0,94.4]:TopTop: ssSkC2,c4_2(x0,x1),ndr1_1(x0),c2_2(x0,a502),c2_0 -> c3_2(x0,x1),c1_2(x0,x1),c5_1(x0)
% 0.37/0.58 120:8:2:[101.0,93.3]:TopTop: ssSkC2,c4_2(x0,x1),ndr1_1(x0),c2_0 -> c3_2(x0,x1),c1_2(x0,x1),c5_2(x0,a502),c5_1(x0)
% 0.37/0.58 119:8:3:[101.0,92.4]:TopTopTop: ssSkC5,c4_2(x0,x1),c3_2(x0,x1),ndr1_1(x0),c3_1(x2) -> c3_1(x0),ndr1_1(x2),c2_1(x2)
% 0.37/0.58 102:4:1:[101.0,69.0]:Top: c3_0 -> c4_1(x0),c5_1(x0),c5_0
% 0.37/0.58 103:4:1:[101.0,70.1]:Top: c5_1(x0) -> ndr1_1(x0),c4_1(x0),ssSkC3
% 0.37/0.58 104:4:1:[101.0,71.1]:Top: c5_1(x0) -> c4_2(x0,a506),c4_1(x0),ssSkC3
% 0.37/0.58 105:4:1:[101.0,72.1]:Top: c5_1(x0) -> c5_2(x0,a506),c4_1(x0),ssSkC3
% 0.37/0.58 106:3:1:[14.0,74.2]:Top: c5_2(a495,x0),c3_2(a495,x0) -> c3_0
% 0.37/0.58 107:4:1:[101.0,75.2]:Top: c3_2(x0,a506),c5_1(x0) -> c4_1(x0),ssSkC3
% 0.37/0.58 108:5:1:[101.0,76.2]:Top: c3_1(x0),c1_1(x0) -> c2_1(x0),ndr1_1(a503),c2_0
% 0.37/0.58 109:5:1:[101.0,77.2]:Top: c3_1(x0),c1_1(x0) -> c2_1(x0),c4_2(a503,a504),c2_0
% 0.37/0.58 110:5:1:[27.1,81.2]:Top: ssSkC7,c4_2(a514,x0) -> c5_2(a514,x0),c3_2(a514,x0),c2_0
% 0.37/0.58 111:5:1:[101.0,82.2]:Top: c3_1(x0),c1_1(x0),c3_2(a503,a505) -> c2_1(x0),c2_0
% 0.37/0.58 112:5:1:[101.0,83.2]:Top: c3_1(x0),c1_1(x0),c5_2(a503,a505) -> c2_1(x0),c2_0
% 0.37/0.58 113:5:1:[101.0,84.2]:Top: c3_1(x0),c1_1(x0),c2_2(a503,a505) -> c2_1(x0),c2_0
% 0.37/0.58 114:5:1:[101.0,85.2]:Top: c3_1(x0),c1_1(x0),c2_2(a503,a504) -> c2_1(x0),c2_0
% 0.37/0.58 115:5:1:[101.0,86.2]:Top: c3_1(x0),c1_1(x0),c5_2(a503,a504) -> c2_1(x0),c2_0
% 0.37/0.58 116:6:2:[101.0,88.1]:TopTop: ndr1_1(x0) -> c2_2(x0,x1),c1_2(x0,x1),c5_2(x0,a497),c3_1(x0),ssSkC1
% 0.37/0.58 117:6:2:[101.0,89.1]:TopTop: ndr1_1(x0) -> c2_2(x0,x1),c1_2(x0,x1),c1_2(x0,a497),c3_1(x0),ssSkC1
% 0.37/0.58 118:6:2:[101.0,90.1]:TopTop: ndr1_1(x0) -> c2_2(x0,x1),c1_2(x0,x1),c3_2(x0,a497),c3_1(x0),ssSkC1
% 0.37/0.58
% 0.37/0.58 Most General Atoms: ndr1_0 c1_1(x0) c2_0 c4_0 c1_0 c3_2(x0,x1) c1_2(x0,x1) c4_1(x0) c5_2(x0,x1) ssSkC5 c4_2(x0,x1) c3_1(x2) c2_1(x2) c5_0 ssSkC2 c5_1(x0) ndr1_1(x2) ssSkC3 ssSkC4 c3_0 ssSkC8 ssSkC7 ssSkC0 ssSkC6 ssSkC1 c2_2(x0,x1)
% 0.37/0.58
% 0.37/0.58 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_1 ===
% 0.37/0.58
% 0.37/0.58 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.37/0.58 === Restarting.
% 0.37/0.58 === Conflict found: 108:5:1:[101.0,76.2]:Top: c3_1(x0),c1_1(x0) -> c2_1(x0),ndr1_1(a503),c2_0 {x0 -> a513}
% 0.37/0.58 === Backtracking. Learning clause 129:4:0:[108.1,19.1,18.1]:: -> c2_1(a513),ndr1_1(a503),c2_0,ssSkC7
% 0.37/0.58 === Clause set with instances from active satisfied. Growing active. New size: 178
% 0.37/0.58
% 0.37/0.58 Linear Model Building succeeded.
% 0.37/0.58 SZS status Satisfiable
% 0.37/0.58
% 0.37/0.58 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.58
% 0.37/0.58 SPASS-SCL-FOL Statistics:
% 0.37/0.58 Number of learned clauses: 1
% 0.37/0.58 Number of propagations: 57
% 0.37/0.58 Number of decisions: 204
% 0.37/0.58 Number of resolutions: 2
% 0.37/0.58 Number of condensations: 0
% 0.37/0.58 Number of sub resolutions: 28
% 0.37/0.58 Number of input literals (deduplicated): 124
% 0.37/0.58 Number of grows: 2
% 0.37/0.58 Number of considered ground atoms: 178
% 0.37/0.58
% 0.37/0.58 Needed: 0:00:00.01
% 0.37/0.58
%------------------------------------------------------------------------------