%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN694-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 : n010.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:10 PM UTC 2026
% Result : Unsatisfiable 126.71s 32.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : SYN694-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 : n010.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:47:07 EDT 2026
% 0.20/0.37 % CPUTime :
% 0.20/0.37 SPASS-SCL-FOL version:
% 0.26/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 126.71/32.23 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 126.71/32.23 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 126.71/32.23 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 126.71/32.23 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 126.71/32.23 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 126.71/32.23 Execution resolution_1 ended with status: unsatisfiable
% 126.71/32.23 Used heuristic: resolution_1
% 126.71/32.23
% 126.71/32.23 Input Clauses:
% 126.71/32.24
% 126.71/32.24 Predicates: p25 p29 p30 p28 p10 p7 p6 p3 p21 p2 p17 p14 p12 p31 p26 p33 p27 p32
% 126.71/32.24 Fol Constants: c34 c36 c41 c38 c39 c40 c43 c47 c46 c42 c44 c45 c37 c35
% 126.71/32.24 Fol Functions: f18 f16 f5 f9 f8 f20 f23 f4 f24 f11 f19 f13 f22 f15
% 126.71/32.24 Problem Properties:
% 126.71/32.24 This is a full first-order problem without equality.
% 126.71/32.24
% 126.71/32.24 After reduction: Problem Properties:
% 126.71/32.24 This is a full first-order problem without equality.
% 126.71/32.24
% 126.71/32.24
% 126.71/32.24 Reduced Input Clauses:
% 126.71/32.24
% 126.71/32.24 Most General Atoms: p25(x1) p30(x1) p29(x1) p28(x1) p6(x1,x2) p17(x1,x2) p14(x1,x2) p33(x3,x1) p12(x2,x3) p27(x1,x3) p31(x3,x1) p10(x2,x3) p32(x1,x3) p3(x2,x3) p7(x2,x3) p21(x4,x5) p26(x5,x3,x1) p2(x1,x5)
% 126.71/32.24
% 126.71/32.24 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 ===
% 126.71/32.24
% 126.71/32.24 === Backtracking. Learning clause 74:2:1:[37.2,16.1]:Top: p10(c43,x0) -> p10(x0,c47)
% 126.71/32.24 === Backtracking. Learning clause 75:2:1:[42.2,18.1]:Top: p2(c44,x0) -> p2(x0,c45)
% 126.71/32.24 === Backtracking. Learning clause 76:2:1:[38.2,22.1]:Top: p7(f8(c35),x0) -> p7(x0,c36)
% 126.71/32.24 === Backtracking. Learning clause 77:2:1:[42.2,20.1]:Top: p2(c46,x0) -> p2(x0,f9(c37))
% 126.71/32.24 === Backtracking. Learning clause 78:2:2:[38.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 79:2:2:[40.2,10.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 80:2:2:[42.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 126.71/32.24 === Clause set with instances from active satisfied. Growing active. New size: 114
% 126.71/32.24 === Restarting.
% 126.71/32.24 === Backtracking. Learning clause 81:2:2:[43.2,13.1]:TopTop: p17(x0,x1) -> p17(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 82:3:2:[49.1,53.1]:TopTop: p33(x0,f11(f4(c46),c47)),p2(x0,x1) -> p33(x1,f19(f11(f4(c42),c47),f9(f20(c37))))
% 126.71/32.24 === Backtracking. Learning clause 83:3:2:[51.3,55.1]:TopTop: p2(x0,x1),p31(f11(f4(f23(c44,f9(f20(c37)))),c43),x0) -> p31(f11(f4(c44),c43),x1)
% 126.71/32.24 === Clause set with instances from active satisfied. Growing active. New size: 181
% 126.71/32.24 === Restarting.
% 126.71/32.24 === Conflict found: 74:2:1:[37.2,16.1]:Top: p10(c43,x0) -> p10(x0,c47) {x0 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 84:3:2:[74.1,37.3]:TopTop: p10(x0,c43),p10(x0,x1) -> p10(x1,c47)
% 126.71/32.24 === Backtracking. Learning clause 85:3:2:[51.2,21.1]:TopTop: p2(f5(c42),x0),p2(c44,x1) -> p31(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 86:4:3:[43.3,26.2]:TopTopTop: p17(x0,x1),p17(x0,x2),p30(x1) -> p30(x2)
% 126.71/32.24 === Backtracking. Learning clause 87:2:2:[44.2,14.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 88:3:3:[52.1,13.1]:TopTopTop: p32(x0,x1),p10(x1,x2) -> p32(x0,x2)
% 126.71/32.24 === Backtracking. Learning clause 89:3:2:[51.2,23.1]:TopTop: p2(c45,x0),p2(f23(c44,f9(f20(c37))),x1) -> p31(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 90:2:1:[42.1,53.1,80.1]:Top: p2(f11(f4(c46),c47),x0) -> p2(x0,f19(f11(f4(c42),c47),f9(f20(c37))))
% 126.71/32.24 === Backtracking. Learning clause 91:2:0:[61.3,56.1]:: p10(c43,c43),p3(f4(c45),f4(f23(c44,f9(f20(c37))))) ->
% 126.71/32.24 === Clause set with instances from active satisfied. Growing active. New size: 247
% 126.71/32.24 === Restarting.
% 126.71/32.24 === Conflict found: 78:2:2:[38.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c34, x1 -> f8(c35)}
% 126.71/32.24 === Backtracking. Learning clause 92:2:1:[78.2,76.1]:Top: p7(x0,f8(c35)) -> p7(x0,c36)
% 126.71/32.24 === Conflict found: 78:2:2:[38.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c35), x1 -> c36}
% 126.71/32.24 === Backtracking. Learning clause 94:1:0:[2.0,93.0,78.1,22.1,27.2]:: -> p29(f8(c35))
% 126.71/32.24 === Backtracking. Learning clause 95:4:3:[42.3,85.1]:TopTopTop: p2(x0,f5(c42)),p2(x0,x1),p2(c44,x2) -> p31(x2,x1)
% 126.71/32.24 === Backtracking. Learning clause 96:4:4:[42.2,42.3,80.2]:TopTopTopTop: p2(x0,x1),p2(x0,x2),p2(x3,x1) -> p2(x3,x2)
% 126.71/32.24 === Conflict found: 96:4:4:[42.2,42.3,80.2]:TopTopTopTop: p2(x0,x1),p2(x0,x2),p2(x3,x1) -> p2(x3,x2) {x0 -> f5(c42), x1 -> c45, x2 -> f5(c42), x3 -> c44}
% 126.71/32.24 === Backtracking. Learning clause 97:3:3:[96.2,12.1]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0)
% 126.71/32.24 === Backtracking. Learning clause 98:2:2:[45.2,15.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 126.71/32.24 === Backtracking. Learning clause 99:1:0:[67.3,69.3,48.3,47.3,21.1]:: p31(c44,c44) ->
% 126.71/32.24 === Backtracking. Learning clause 100:2:1:[42.3,56.1]:Top: p2(x0,f11(f4(c45),c43)),p2(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)) ->
% 126.71/32.24 === Conflict found: 97:3:3:[96.2,12.1]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> c34, x1 -> f11(f4(c44),c43), x2 -> f11(f4(f23(c44,f9(f20(c37)))),c43)}
% 126.71/32.24 === Backtracking. Learning clause 101:3:2:[97.2,55.1,97.1,100.2]:TopTop: p2(x0,f11(f4(c44),c43)),p2(x1,x0),p2(x1,f11(f4(c45),c43)) ->
% 126.71/32.24 === Conflict found: 97:3:3:[96.2,12.1]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> c34, x1 -> f11(f4(c42),c43), x2 -> f19(f11(f4(f5(c42)),c43),f9(f20(c37)))}
% 126.71/32.24 === Backtracking. Learning clause 102:2:1:[97.2,64.1]:Top: p2(x0,f11(f4(c42),c43)) -> p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0)
% 126.71/32.24 === Backtracking. Learning clause 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3)
% 126.71/32.24 === Clause set with instances from active satisfied. Growing active. New size: 286
% 126.71/32.24 === Restarting.
% 126.71/32.24 === Conflict found: 78:2:2:[38.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c34, x1 -> c36}
% 126.71/32.24 === Backtracking. Learning clause 104:3:2:[78.2,27.2]:TopTop: p7(x0,x1),p29(x1) -> p29(x0)
% 126.71/32.24 === Conflict found: 97:3:3:[96.2,12.1]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> c44, x1 -> c45, x2 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 105:2:1:[97.1,18.1]:Top: p2(x0,c45) -> p2(x0,c44)
% 126.71/32.24 === Conflict found: 78:2:2:[38.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c35), x1 -> c36}
% 126.71/32.24 === Backtracking. Learning clause 106:1:0:[78.1,22.1]:: -> p7(c36,f8(c35))
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> c34, x1 -> c34, x2 -> c34, x3 -> c46, x4 -> f9(c37)}
% 126.71/32.24 === Backtracking. Learning clause 107:4:3:[103.3,20.1]:TopTopTop: p31(x0,x1),p2(x0,x2),p2(x1,f9(c37)) -> p31(x2,c46)
% 126.71/32.24 === Conflict found: 95:4:3:[42.3,85.1]:TopTopTop: p2(x0,f5(c42)),p2(x0,x1),p2(c44,x2) -> p31(x2,x1) {x0 -> f5(c34), x1 -> c34, x2 -> c45}
% 126.71/32.24 === Backtracking. Learning clause 108:4:3:[95.1,34.2,80.2]:TopTopTop: p2(c44,x0),p2(x1,c42),p2(x2,f5(x1)) -> p31(x0,x2)
% 126.71/32.24 === Backtracking. Learning clause 109:4:4:[70.4,24.1]:TopTopTopTop: p3(f4(x0),x1),p3(f4(f5(x0)),x2),p21(c34,x3) -> p26(x3,x2,x1)
% 126.71/32.24 === Backtracking. Learning clause 110:8:9:[49.3,61.3,49.2,42.3]:TopTopTopTopTopTopTopTopTop: p2(x0,x1),p33(f11(x2,x3),x0),p10(x3,x4),p3(x2,x5),p2(x1,x6),p2(x7,f11(x5,x4)),p2(x7,x8) -> p33(x8,x6)
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> f11(c34,c34), x1 -> c34, x2 -> f11(f4(c44),c43), x3 -> c34, x4 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 111:6:7:[103.2,61.3]:TopTopTopTopTopTopTop: p31(f11(x0,x1),x2),p2(x3,x4),p2(x2,x4),p10(x1,x5),p3(x0,x6) -> p31(f11(x6,x5),x3)
% 126.71/32.24 === Conflict found: 101:3:2:[97.2,55.1,97.1,100.2]:TopTop: p2(x0,f11(f4(c44),c43)),p2(x1,x0),p2(x1,f11(f4(c45),c43)) -> {x0 -> f11(c34,c34), x1 -> f11(c34,c34)}
% 126.71/32.24 === Backtracking. Learning clause 112:3:2:[101.3,61.3,61.3,12.1]:TopTop: p3(x1,f4(c45)),p10(x0,c43),p3(x1,f4(c44)) ->
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> f11(f4(c34),c47), x1 -> c34, x2 -> f11(f4(c46),c47), x3 -> c34, x4 -> f11(f4(c45),c43)}
% 126.71/32.24 === Backtracking. Learning clause 113:6:4:[103.2,66.3]:TopTopTopTop: p31(f11(f4(x0),c47),x1),p2(x2,x3),p2(x1,x3),p31(x0,c42),p31(c46,x0) -> p31(f11(f4(c46),c47),x2)
% 126.71/32.24 === Backtracking. Learning clause 114:5:3:[49.3,66.3]:TopTopTop: p2(x0,x1),p33(f11(f4(x2),c47),x0),p31(x2,c42),p31(c46,x2) -> p33(f11(f4(c46),c47),x1)
% 126.71/32.24 === Conflict found: 110:8:9:[49.3,61.3,49.2,42.3]:TopTopTopTopTopTopTopTopTop: p2(x0,x1),p33(f11(x2,x3),x0),p10(x3,x4),p3(x2,x5),p2(x1,x6),p2(x7,f11(x5,x4)),p2(x7,x8) -> p33(x8,x6) {x0 -> c34, x1 -> f11(f4(c45),c43), x2 -> c34, x3 -> c34, x4 -> c43, x5 -> f4(c34), x6 -> c34, x7 -> f11(f4(f24(c34)),c43), x8 -> f11(f4(c34),c43)}
% 126.71/32.24 === Backtracking. Learning clause 115:6:7:[110.6,61.3]:TopTopTopTopTopTopTop: p2(x0,x1),p33(f11(x2,x3),x0),p10(x3,x4),p3(x2,x5),p2(x1,x6) -> p33(f11(x5,x4),x6)
% 126.71/32.24 === Conflict found: 110:8:9:[49.3,61.3,49.2,42.3]:TopTopTopTopTopTopTopTopTop: p2(x0,x1),p33(f11(x2,x3),x0),p10(x3,x4),p3(x2,x5),p2(x1,x6),p2(x7,f11(x5,x4)),p2(x7,x8) -> p33(x8,x6) {x0 -> c34, x1 -> f11(f4(f24(c34)),c43), x2 -> f4(c34), x3 -> c43, x4 -> c43, x5 -> f4(c34), x6 -> c34, x7 -> f11(f4(f24(c34)),c43), x8 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 116:9:9:[110.6,61.3,42.3]:TopTopTopTopTopTopTopTopTop: p2(x0,f11(x1,x2)),p33(f11(x3,x4),x0),p10(x4,x5),p3(x3,x6),p10(x2,x5),p3(x1,x6),p2(x7,f11(x1,x2)),p2(x7,x8) -> p33(x8,x8)
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> c34, x1 -> c34, x2 -> f24(c34), x3 -> f5(c42), x4 -> f19(f11(f4(c42),c47),f9(f20(c37)))}
% 126.71/32.24 === Backtracking. Learning clause 117:5:4:[103.3,90.2]:TopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x1,f19(f11(f4(c42),c47),f9(f20(c37)))),p2(f11(f4(c46),c47),x3) -> p31(x2,x3)
% 126.71/32.24 === Backtracking. Learning clause 118:5:6:[51.1,61.3]:TopTopTopTopTopTop: p31(x0,f11(x1,x2)),p2(x0,x3),p10(x2,x4),p3(x1,x5) -> p31(x3,f11(x5,x4))
% 126.71/32.24 === Backtracking. Learning clause 119:5:3:[51.1,66.3]:TopTopTop: p31(x0,f11(f4(x1),c47)),p2(x0,x2),p31(x1,c42),p31(c46,x1) -> p31(x2,f11(f4(c46),c47))
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> c34, x1 -> f11(c34,c34), x2 -> c34, x3 -> c44, x4 -> f11(f4(f23(c44,f9(f20(c37)))),c43)}
% 126.71/32.24 === Backtracking. Learning clause 120:6:7:[103.4,61.3]:TopTopTopTopTopTopTop: p31(x0,f11(x1,x2)),p2(x0,x3),p2(x4,f11(x5,x6)),p10(x2,x6),p3(x1,x5) -> p31(x3,x4)
% 126.71/32.24 === Conflict found: 97:3:3:[96.2,12.1]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> f11(f4(c46),c47), x1 -> f19(f11(f4(c42),c47),f9(f20(c37))), x2 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 121:2:1:[97.1,53.1]:Top: p2(x0,f19(f11(f4(c42),c47),f9(f20(c37)))) -> p2(x0,f11(f4(c46),c47))
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> f11(f4(c46),c47), x1 -> c34, x2 -> f19(f11(f4(c42),c47),f9(f20(c37))), x3 -> c34, x4 -> c42}
% 126.71/32.24 === Backtracking. Learning clause 122:4:3:[103.2,53.1]:TopTopTop: p31(f11(f4(c46),c47),x0),p2(x1,x2),p2(x0,x2) -> p31(f19(f11(f4(c42),c47),f9(f20(c37))),x1)
% 126.71/32.24 === Backtracking. Learning clause 123:3:2:[49.3,53.1]:TopTop: p2(x0,x1),p33(f11(f4(c46),c47),x0) -> p33(f19(f11(f4(c42),c47),f9(f20(c37))),x1)
% 126.71/32.24 === Backtracking. Learning clause 124:3:2:[49.3,64.1]:TopTop: p2(x0,x1),p33(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0) -> p33(f11(f4(c42),c43),x1)
% 126.71/32.24 === Conflict found: 80:2:2:[42.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f19(f11(f4(f5(c42)),c43),f9(f20(c37))), x1 -> f11(f4(c42),c43)}
% 126.71/32.24 === Backtracking. Learning clause 125:4:3:[80.1,64.1,103.2]:TopTopTop: p31(f11(f4(c42),c43),x0),p2(x1,x2),p2(x0,x2) -> p31(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x1)
% 126.71/32.24 === Conflict found: 80:2:2:[42.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f19(f11(f4(f5(c42)),c43),f9(f20(c37))), x1 -> f11(f4(c42),c43)}
% 126.71/32.24 === Backtracking. Learning clause 126:1:0:[80.1,64.1]:: -> p2(f11(f4(c42),c43),f19(f11(f4(f5(c42)),c43),f9(f20(c37))))
% 126.71/32.24 === Clause set with instances from active satisfied. Growing active. New size: 352
% 126.71/32.24 === Restarting.
% 126.71/32.24 === Conflict found: 103:5:5:[51.1,97.3]:TopTopTopTopTop: p31(x0,x1),p2(x0,x2),p2(x3,x4),p2(x1,x4) -> p31(x2,x3) {x0 -> c46, x1 -> c42, x2 -> c34, x3 -> c45, x4 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 127:7:6:[103.1,17.1,103.1]:TopTopTopTopTopTop: p2(c46,x0),p2(x1,x2),p2(c42,x2),p2(x0,x3),p2(x4,x5),p2(x1,x5) -> p31(x3,x4)
% 126.71/32.24 === Conflict found: 127:7:6:[103.1,17.1,103.1]:TopTopTopTopTopTop: p2(c46,x0),p2(x1,x2),p2(c42,x2),p2(x0,x3),p2(x4,x5),p2(x1,x5) -> p31(x3,x4) {x0 -> c34, x1 -> c45, x2 -> c34, x3 -> c44, x4 -> c44, x5 -> c34}
% 126.71/32.24 === Backtracking. Learning clause 128:4:2:[127.7,99.1,80.2,80.2,80.2,80.2]:TopTop: p2(x0,c44),p2(x1,c44),p2(x1,c42),p2(x0,c46) ->
% 126.71/32.24 === Conflict found: 92:2:1:[78.2,76.1]:Top: p7(x0,f8(c35)) -> p7(x0,c36) {x0 -> f8(c34)}
% 126.71/32.24 === Backtracking. Learning clause 129:3:2:[92.1,29.2,38.2,78.2]:TopTop: p6(x0,c35),p7(x1,f8(x0)) -> p7(x1,c36)
% 126.71/32.24 === Conflict found: 112:3:2:[101.3,61.3,61.3,12.1]:TopTop: p3(x1,f4(c45)),p10(x0,c43),p3(x1,f4(c44)) -> {x0 -> c34, x1 -> f4(c45)}
% 126.71/32.24 === Backtracking. Learning clause 130:1:1:[112.1,10.1,36.2,42.3,18.1,12.1]:Top: p10(x0,c43) ->
% 126.71/32.24 === Conflict found: 130:1:1:[112.1,10.1,36.2,42.3,18.1,12.1]:Top: p10(x0,c43) -> {x0 -> c43}
% 126.71/32.24
% 126.71/32.24 SZS status Unsatisfiable
% 126.71/32.24
% 126.71/32.24 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 126.71/32.24
% 126.71/32.24 SPASS-SCL-FOL Statistics:
% 126.71/32.24 Number of learned clauses: 56
% 126.71/32.24 Number of propagations: 3090
% 126.71/32.24 Number of decisions: 2080
% 126.71/32.24 Number of resolutions: 83
% 126.71/32.24 Number of condensations: 2
% 126.71/32.24 Number of sub resolutions: 1
% 126.71/32.24 Number of input literals (deduplicated): 80
% 126.71/32.24 Number of grows: 5
% 126.71/32.24 Number of considered ground atoms: 352
% 126.71/32.24
% 126.71/32.24 Needed: 0:0:31.61
% 126.71/32.24
%------------------------------------------------------------------------------