%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN712-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 : n007.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:11 PM UTC 2026
% Result : Unsatisfiable 0.41s 1.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.15 % Problem : SYN712-1 : TPTP v9.2.1. Released v2.5.0.
% 0.11/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.37 % Computer : n007.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:46:39 EDT 2026
% 0.20/0.38 % CPUTime :
% 0.20/0.38 SPASS-SCL-FOL version:
% 0.30/0.50 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.41/1.01 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.01 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.01 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.01 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.01 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.01 Execution resolution_1 ended with status: unsatisfiable
% 0.41/1.01 Used heuristic: resolution_1
% 0.41/1.01
% 0.41/1.01 Input Clauses:
% 0.41/1.01
% 0.41/1.01 Predicates: p10 p9 p7 p60 p6 p58 p56 p54 p52 p50 p48 p46 p44 p42 p40 p4 p38 p35 p34 p32 p30 p3 p28 p26 p24 p22 p20 p2 p18 p17 p15 p14 p12 p62 p63
% 0.41/1.01 Fol Constants: c64 c65 c66 c67 c68 c69 c74 c70 c71 c72 c73 c76 c75
% 0.41/1.01 Fol Functions: f13 f11 f8 f5 f43 f53 f61 f59 f57 f55 f51 f49 f47 f45 f23 f41 f36 f39 f16 f31 f29 f27 f25 f37 f21 f33 f19
% 0.41/1.01 Problem Properties:
% 0.41/1.01 This is a full first-order problem without equality.
% 0.41/1.01
% 0.41/1.01 After reduction: Problem Properties:
% 0.41/1.01 This is a full first-order problem without equality.
% 0.41/1.01
% 0.41/1.01
% 0.41/1.01 Reduced Input Clauses:
% 0.41/1.01
% 0.41/1.01 Most General Atoms: p10(x1,x2) p6(x1,x2) p56(x1,x2) p46(x1,x2) p35(x1,x2) p30(x1,x2) p26(x1,x2) p20(x1,x2) p2(x1,x2) p17(x1,x2) p14(x1,x2) p12(x1,x2) p15(x2,x3) p63(x1,x3) p32(x2,x3) p42(x2,x3) p4(x2,x3) p52(x2,x3) p9(x2,x3) p60(x2,x3) p58(x2,x3) p7(x2,x3) p54(x2,x3) p50(x2,x3) p48(x2,x3) p44(x2,x3) p3(x2,x3) p22(x2,x3) p40(x2,x3) p34(x2,x3) p38(x2,x3) p28(x2,x3) p24(x2,x3) p18(x2,x3) p62(x0,x5)
% 0.41/1.01
% 0.41/1.01 === Starting SPASS-SCL-FOL A Little Less Naive, considering 52 atoms initially, heuristics mode: resolution_1 ===
% 0.41/1.01
% 0.41/1.01 === Backtracking. Learning clause 105:2:2:[34.2,1.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 106:2:2:[35.2,2.1]:TopTop: p9(x0,x1) -> p9(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 107:2:2:[36.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 108:2:2:[38.2,5.1]:TopTop: p6(x0,x1) -> p6(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 109:2:2:[39.2,6.1]:TopTop: p58(x0,x1) -> p58(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 110:3:2:[69.4,67.1]:TopTop: p4(x0,f5(c64,f8(f11(f13(c65,c66),c67),c68))),p62(x0,x1),p32(x1,c69) ->
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 119
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Backtracking. Learning clause 111:2:2:[42.2,9.1]:TopTop: p52(x0,x1) -> p52(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 112:2:2:[45.2,12.1]:TopTop: p46(x0,x1) -> p46(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 113:2:2:[46.2,13.1]:TopTop: p44(x0,x1) -> p44(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 114:2:2:[59.2,26.1]:TopTop: p22(x0,x1) -> p22(x1,x0)
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 147
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Backtracking. Learning clause 115:2:2:[49.2,16.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 116:2:2:[51.2,18.1]:TopTop: p35(x0,x1) -> p35(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 117:2:2:[55.2,22.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 118:2:2:[56.2,23.1]:TopTop: p28(x0,x1) -> p28(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 119:2:1:[69.1,16.1,67.1]:Top: p62(f5(c64,f8(f11(f13(c65,c66),c67),c68)),x0),p32(x0,c69) ->
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 148
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Backtracking. Learning clause 120:2:2:[40.2,7.1]:TopTop: p56(x0,x1) -> p56(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 121:2:2:[41.2,8.1]:TopTop: p54(x0,x1) -> p54(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 122:2:2:[44.2,11.1]:TopTop: p48(x0,x1) -> p48(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 123:2:2:[47.2,14.1]:TopTop: p42(x0,x1) -> p42(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 124:2:2:[52.2,19.1]:TopTop: p34(x0,x1) -> p34(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 125:4:6:[69.4,97.1]:TopTopTopTopTopTop: p4(x0,f5(c64,f8(f11(f13(c65,x1),x2),x3))),p62(x0,x4),p32(x4,x5) -> p62(x1,x5)
% 0.41/1.01 === Backtracking. Learning clause 126:1:0:[98.2,67.1]:: p62(c66,c69) ->
% 0.41/1.01 === Backtracking. Learning clause 127:2:6:[55.1,104.1,117.1]:TopTopTopTopTopTop: p3(f16(f19(f21(c70,f8(f11(f13(c65,x0),x1),x2)),x3),x4),x5) -> p3(x5,f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,x0),x1),x2),x3),x4)),f43(f45(f47(f49(f51(c75,x0),x1),x2),x3),x4)),f53(f55(f57(f59(f61(c76,x0),x1),x2),x3),x4)))
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 152
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Backtracking. Learning clause 128:2:2:[57.2,24.1]:TopTop: p26(x0,x1) -> p26(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 129:2:2:[58.2,25.1]:TopTop: p24(x0,x1) -> p24(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 130:2:2:[65.2,32.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 131:5:7:[82.3,125.1]:TopTopTopTopTopTopTop: p2(x0,c64),p3(x1,f8(f11(f13(c65,x2),x3),x4)),p62(f5(x0,x1),x5),p32(x5,x6) -> p62(x2,x6)
% 0.41/1.01 === Backtracking. Learning clause 132:6:10:[101.1,68.4,69.4]:TopTopTopTopTopTopTopTopTopTop: p35(x0,f36(f39(f41(c73,x1),x2),f37(x3,x4))),p63(x0,x5),p15(x5,f33(x6,x4)),p4(x7,f23(f25(f27(f29(f31(c74,x8),x3),x6),x1),x2)),p62(x7,x9),p32(x9,x4) ->
% 0.41/1.01 === Conflict found: 127:2:6:[55.1,104.1,117.1]:TopTopTopTopTopTop: p3(f16(f19(f21(c70,f8(f11(f13(c65,x0),x1),x2)),x3),x4),x5) -> p3(x5,f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,x0),x1),x2),x3),x4)),f43(f45(f47(f49(f51(c75,x0),x1),x2),x3),x4)),f53(f55(f57(f59(f61(c76,x0),x1),x2),x3),x4))) {x0 -> c64, x1 -> c64, x2 -> c64, x3 -> c64, x4 -> c64, x5 -> c64}
% 0.41/1.01 === Backtracking. Learning clause 133:5:9:[127.2,131.2]:TopTopTopTopTopTopTopTopTop: p3(f16(f19(f21(c70,f8(f11(f13(c65,x0),x1),x2)),x3),x4),x5),p2(x6,c64),p62(f5(x6,x5),x7),p32(x7,x8) -> p62(f23(f25(f27(f29(f31(c74,x0),x1),x2),x3),x4),x8)
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 170
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Backtracking. Learning clause 134:2:2:[64.2,31.1]:TopTop: p15(x0,x1) -> p15(x1,x0)
% 0.41/1.01 === Backtracking. Learning clause 135:2:1:[98.2,119.1]:Top: p62(c66,x0),p32(x0,c69) ->
% 0.41/1.01 === Backtracking. Learning clause 136:4:5:[49.2,82.3]:TopTopTopTopTop: p4(f5(x0,x1),x2),p2(x0,x3),p3(x1,x4) -> p4(x2,f5(x3,x4))
% 0.41/1.01 === Backtracking. Learning clause 137:3:2:[69.2,100.1]:TopTop: p4(f5(c64,f16(f19(f21(c70,f8(f11(f13(c65,c66),c67),c68)),c71),c72)),x0),p32(c69,x1) -> p62(x0,x1)
% 0.41/1.01 === Conflict found: 133:5:9:[127.2,131.2]:TopTopTopTopTopTopTopTopTop: p3(f16(f19(f21(c70,f8(f11(f13(c65,x0),x1),x2)),x3),x4),x5),p2(x6,c64),p62(f5(x6,x5),x7),p32(x7,x8) -> p62(f23(f25(f27(f29(f31(c74,x0),x1),x2),x3),x4),x8) {x0 -> c64, x1 -> c64, x2 -> c64, x3 -> c64, x4 -> c64, x5 -> f16(f19(f21(c70,f8(f11(f13(c65,c64),c64),c64)),c64),c64), x6 -> c64, x7 -> c64, x8 -> c64}
% 0.41/1.01 === Backtracking. Learning clause 138:4:8:[133.1,22.1]:TopTopTopTopTopTopTopTop: p2(x0,c64),p62(f5(x0,f16(f19(f21(c70,f8(f11(f13(c65,x1),x2),x3)),x4),x5)),x6),p32(x6,x7) -> p62(f23(f25(f27(f29(f31(c74,x1),x2),x3),x4),x5),x7)
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 185
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Backtracking. Learning clause 139:4:5:[49.2,83.3]:TopTopTopTopTop: p4(f23(x0,x1),x2),p15(x1,x3),p22(x0,x4) -> p4(x2,f23(x4,x3))
% 0.41/1.01 === Conflict found: 138:4:8:[133.1,22.1]:TopTopTopTopTopTopTopTop: p2(x0,c64),p62(f5(x0,f16(f19(f21(c70,f8(f11(f13(c65,x1),x2),x3)),x4),x5)),x6),p32(x6,x7) -> p62(f23(f25(f27(f29(f31(c74,x1),x2),x3),x4),x5),x7) {x0 -> c64, x1 -> c66, x2 -> c67, x3 -> c68, x4 -> c71, x5 -> c72, x6 -> c69, x7 -> c64}
% 0.41/1.01 === Backtracking. Learning clause 140:3:2:[138.2,100.1,99.1,135.1,28.1,53.3]:TopTop: p32(x0,c69),p32(x1,c69),p32(x1,x0) ->
% 0.41/1.01 === Conflict found: 138:4:8:[133.1,22.1]:TopTopTopTopTopTopTopTop: p2(x0,c64),p62(f5(x0,f16(f19(f21(c70,f8(f11(f13(c65,x1),x2),x3)),x4),x5)),x6),p32(x6,x7) -> p62(f23(f25(f27(f29(f31(c74,x1),x2),x3),x4),x5),x7) {x0 -> c64, x1 -> c66, x2 -> c67, x3 -> c68, x4 -> c71, x5 -> c72, x6 -> c69, x7 -> c64}
% 0.41/1.01 === Backtracking. Learning clause 141:3:1:[138.2,100.1,99.1]:Top: p2(c64,c64),p32(c69,x0) -> p62(c66,x0)
% 0.41/1.01 === Clause set with instances from active satisfied. Growing active. New size: 196
% 0.41/1.01 === Restarting.
% 0.41/1.01 === Conflict found: 140:3:2:[138.2,100.1,99.1,135.1,28.1,53.3]:TopTop: p32(x0,c69),p32(x1,c69),p32(x1,x0) -> {x0 -> c69, x1 -> c69}
% 0.41/1.01
% 0.41/1.01 SZS status Unsatisfiable
% 0.41/1.01
% 0.41/1.01 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/1.01
% 0.41/1.01 SPASS-SCL-FOL Statistics:
% 0.41/1.01 Number of learned clauses: 37
% 0.41/1.01 Number of propagations: 2593
% 0.41/1.01 Number of decisions: 1369
% 0.41/1.01 Number of resolutions: 46
% 0.41/1.01 Number of condensations: 0
% 0.41/1.01 Number of sub resolutions: 0
% 0.41/1.01 Number of input literals (deduplicated): 103
% 0.41/1.01 Number of grows: 7
% 0.41/1.01 Number of considered ground atoms: 196
% 0.41/1.01
% 0.41/1.01 Needed: 0:00:00.39
% 0.41/1.01
%------------------------------------------------------------------------------