%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN674-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 : n005.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:09 PM UTC 2026
% Result : Unsatisfiable 131.42s 26.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN674-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n005.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 13:47:01 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.39 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 131.42/26.87 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 131.42/26.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 131.42/26.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 131.42/26.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 131.42/26.87 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 131.42/26.87 Execution resolution_2 ended with status: unsatisfiable
% 131.42/26.87 Used heuristic: resolution_2
% 131.42/26.87
% 131.42/26.87 Input Clauses:
% 131.42/26.87
% 131.42/26.87 Predicates: p22 p10 p7 p6 p3 p2 p19 p18 p14 p12 p25 p26 p23 p27 p24
% 131.42/26.87 Fol Constants: c28 c37 c34 c33 c36 c32 c31 c29 c30 c35
% 131.42/26.87 Fol Functions: f9 f8 f20 f5 f4 f17 f16 f11 f21 f13 f15
% 131.42/26.87 Problem Properties:
% 131.42/26.87 This is a full first-order problem without equality.
% 131.42/26.87
% 131.42/26.87 After reduction: Problem Properties:
% 131.42/26.87 This is a full first-order problem without equality.
% 131.42/26.87
% 131.42/26.87
% 131.42/26.87 Reduced Input Clauses:
% 131.42/26.87
% 131.42/26.87 Most General Atoms: p22(x1) p6(x1,x2) p19(x1,x2) p14(x1,x2) p2(x2,x3) p27(x3,x1) p12(x2,x3) p24(x1,x3) p25(x3,x1) p10(x2,x3) p26(x1,x3) p7(x2,x3) p3(x2,x3) p18(x4,x5) p23(x5,x3,x1)
% 131.42/26.87
% 131.42/26.87 === Starting SPASS-SCL-FOL A Little Less Naive, considering 58 atoms initially, heuristics mode: resolution_2 ===
% 131.42/26.87
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 58
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 58
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 58
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 58
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 122
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 122
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 122
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 122
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 122
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 186
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 186
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 186
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 188
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 56:3:2:[38.3,11.1]:TopTop: p19(x0,x1),p26(x0,c37) -> p26(x1,c34)
% 131.42/26.87 === Backtracking. Learning clause 57:2:2:[48.1,11.1]:TopTop: p3(x0,x1) -> p2(f11(x0,c37),f11(x1,c34))
% 131.42/26.87 === Backtracking. Learning clause 58:2:1:[26.1,11.1]:Top: p10(c37,x0) -> p10(c34,x0)
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 191
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 59:3:2:[37.2,12.1]:TopTop: p2(c36,x0),p2(c33,x1) -> p25(x1,x0)
% 131.42/26.87 === Backtracking. Learning clause 61:1:0:[14.0,60.0,51.1,12.1]:: -> p2(f11(f4(c33),c34),f11(f4(c32),c34))
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 255
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 258
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 62:2:0:[51.2,13.1]:: p25(c36,c36) -> p2(f11(f4(c36),c34),f11(f4(c32),c34))
% 131.42/26.87 === Backtracking. Learning clause 63:2:0:[50.2,13.1]:: p25(c36,c33) -> p2(f11(f4(c36),c34),f11(f4(c32),c34))
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 258
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Conflict found: 57:2:2:[48.1,11.1]:TopTop: p3(x0,x1) -> p2(f11(x0,c37),f11(x1,c34)) {x0 -> c28, x1 -> c28}
% 131.42/26.87 === Backtracking. Learning clause 64:2:3:[57.1,5.1,49.1]:TopTopTop: p2(x0,x1) -> p2(f16(f11(x2,c37),x0),f16(f11(x2,c34),x1))
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 266
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 65:3:2:[37.1,15.1]:TopTop: p25(x0,c32),p2(x0,x1) -> p25(x1,f9(c31))
% 131.42/26.87 === Backtracking. Learning clause 66:3:2:[35.1,15.1]:TopTop: p27(x0,c32),p2(x0,x1) -> p27(x1,f9(c31))
% 131.42/26.87 === Backtracking. Learning clause 67:2:1:[30.1,15.1]:Top: p2(c32,x0) -> p2(f9(c31),x0)
% 131.42/26.87 === Conflict found: 64:2:3:[57.1,5.1,49.1]:TopTopTop: p2(x0,x1) -> p2(f16(f11(x2,c37),x0),f16(f11(x2,c34),x1)) {x0 -> c32, x1 -> f9(c31), x2 -> c28}
% 131.42/26.87 === Backtracking. Learning clause 68:1:1:[64.1,15.1]:Top: -> p2(f16(f11(x0,c37),c32),f16(f11(x0,c34),f9(c31)))
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 268
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 69:2:1:[27.1,16.1]:Top: p7(f8(c29),x0) -> p7(c30,x0)
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 332
% 131.42/26.87 === Backtracking. Learning clause 70:2:2:[30.2,6.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 333
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 71:3:2:[38.2,17.1]:TopTop: p19(f20(c28,c35),x0),p10(c34,x1) -> p26(x0,x1)
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 335
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 72:4:4:[53.4,18.1]:TopTopTopTop: p3(f4(x0),x1),p3(f4(f5(x0)),x2),p18(c28,x3) -> p23(x3,x2,x1)
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 340
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 73:2:2:[30.3,19.1]:TopTop: p2(x0,x1),p2(x0,f16(x1,f9(f17(c31)))) ->
% 131.42/26.87 === Conflict found: 73:2:2:[30.3,19.1]:TopTop: p2(x0,x1),p2(x0,f16(x1,f9(f17(c31)))) -> {x0 -> c32, x1 -> f9(c31)}
% 131.42/26.87 === Backtracking. Learning clause 74:1:0:[73.1,15.1]:: p2(c32,f16(f9(c31),f9(f17(c31)))) ->
% 131.42/26.87 === Clause set with instances from active satisfied. Growing active. New size: 360
% 131.42/26.87 === Restarting.
% 131.42/26.87 === Backtracking. Learning clause 75:2:1:[30.2,39.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f16(f11(f4(c33),c34),f9(f17(c31))))
% 131.42/26.87 === Conflict found: 73:2:2:[30.3,19.1]:TopTop: p2(x0,x1),p2(x0,f16(x1,f9(f17(c31)))) -> {x0 -> f11(f4(c32),c34), x1 -> f11(f4(c33),c34)}
% 131.42/26.87 === Backtracking. Learning clause 76:1:0:[73.2,39.1]:: p2(f11(f4(c32),c34),f11(f4(c33),c34)) ->
% 131.42/26.87 === Conflict found: 70:2:2:[30.2,6.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f11(f4(c33),c34), x1 -> f11(f4(c32),c34)}
% 131.42/26.87
% 131.42/26.87 SZS status Unsatisfiable
% 131.42/26.87
% 131.42/26.87 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 131.42/26.87
% 131.42/26.87 SPASS-SCL-FOL Statistics:
% 131.42/26.87 Number of learned clauses: 20
% 131.42/26.87 Number of propagations: 3014
% 131.42/26.87 Number of decisions: 1378
% 131.42/26.87 Number of resolutions: 23
% 131.42/26.87 Number of condensations: 0
% 131.42/26.87 Number of sub resolutions: 1
% 131.42/26.87 Number of input literals (deduplicated): 58
% 131.42/26.87 Number of grows: 24
% 131.42/26.87 Number of considered ground atoms: 360
% 131.42/26.87
% 131.42/26.87 Needed: 0:0:26.32
% 131.42/26.87
%------------------------------------------------------------------------------