%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN659-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 : n031.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:07 PM UTC 2026
% Result : Unsatisfiable 5.18s 1.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.15 % Problem : SYN659-1 : TPTP v9.2.1. Released v2.5.0.
% 0.11/0.16 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.38 % Computer : n031.cluster.edu
% 0.19/0.38 % Model : x86_64 x86_64
% 0.19/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.38 % Memory : 8042.1875MB
% 0.19/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.38 % CPULimit : 300
% 0.19/0.38 % WCLimit : 300
% 0.19/0.38 % DateTime : Thu May 7 13:48:56 EDT 2026
% 0.19/0.38 % CPUTime :
% 0.19/0.38 SPASS-SCL-FOL version:
% 0.28/0.48 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.18/1.81 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/1.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/1.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/1.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/1.81 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/1.81 Execution resolution_1 ended with status: unsatisfiable
% 5.18/1.81 Used heuristic: resolution_1
% 5.18/1.81
% 5.18/1.81 Input Clauses:
% 5.18/1.81
% 5.18/1.81 Predicates: p22 p10 p7 p6 p3 p20 p2 p19 p14 p12 p23 p24 p26 p25
% 5.18/1.81 Fol Constants: c27 c41 c38 c31 c32 c28 c29 c36 c33 c37 c34 c35 c40 c39 c30
% 5.18/1.81 Fol Functions: f16 f8 f17 f18 f5 f4 f9 f13 f15 f21 f11
% 5.18/1.81 Problem Properties:
% 5.18/1.81 This is a full first-order problem without equality.
% 5.18/1.81
% 5.18/1.81 After reduction: Problem Properties:
% 5.18/1.81 This is a full first-order problem without equality.
% 5.18/1.81
% 5.18/1.81
% 5.18/1.81 Reduced Input Clauses:
% 5.18/1.81
% 5.18/1.81 Most General Atoms: p22(x1) p6(x1,x2) p20(x1,x2) p14(x1,x2) p26(x3,x1) p12(x2,x3) p24(x1,x3) p10(x2,x3) p25(x1,x3) p7(x2,x3) p3(x2,x3) p19(x4,x5) p23(x5,x3,x1) p2(x1,x5)
% 5.18/1.81
% 5.18/1.81 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_1 ===
% 5.18/1.81
% 5.18/1.81 === Backtracking. Learning clause 52:2:1:[35.2,11.1]:Top: p2(c41,x0) -> p2(x0,c38)
% 5.18/1.81 === Backtracking. Learning clause 53:2:1:[30.2,12.1]:Top: p10(f16(c31),x0) -> p10(x0,c32)
% 5.18/1.81 === Backtracking. Learning clause 54:2:1:[30.2,16.1]:Top: p10(f16(c36),x0) -> p10(x0,c37)
% 5.18/1.81 === Backtracking. Learning clause 55:2:1:[31.2,13.1]:Top: p7(f8(c28),x0) -> p7(x0,c29)
% 5.18/1.81 === Backtracking. Learning clause 56:2:1:[35.2,15.1]:Top: p2(f17(c31),x0) -> p2(x0,c33)
% 5.18/1.81 === Backtracking. Learning clause 57:2:1:[35.2,14.1]:Top: p2(f17(c36),x0) -> p2(x0,c38)
% 5.18/1.81 === Backtracking. Learning clause 58:2:1:[37.3,17.1]:Top: p14(x0,f18(c34)),p14(x0,c35) ->
% 5.18/1.81 === Backtracking. Learning clause 59:2:2:[30.2,2.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 5.18/1.81 === Backtracking. Learning clause 60:2:2:[31.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 5.18/1.81 === Backtracking. Learning clause 61:2:2:[33.2,5.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 5.18/1.81 === Backtracking. Learning clause 62:2:2:[35.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 5.18/1.81 === Backtracking. Learning clause 63:2:2:[37.2,9.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 5.18/1.81 === Clause set with instances from active satisfied. Growing active. New size: 125
% 5.18/1.81 === Restarting.
% 5.18/1.81 === Conflict found: 59:2:2:[30.2,2.1]:TopTop: p10(x0,x1) -> p10(x1,x0) {x0 -> c27, x1 -> f16(c36)}
% 5.18/1.81 === Backtracking. Learning clause 64:2:1:[59.2,54.1]:Top: p10(x0,f16(c36)) -> p10(x0,c37)
% 5.18/1.81 === Backtracking. Learning clause 65:5:6:[41.4,49.2]:TopTopTopTopTopTop: p14(x0,f15(c29,f13(x1,x2))),p24(x0,x3),p12(x3,f13(x4,x5)),p2(f11(f4(x2),x1),f9(c30)) -> p10(x1,x4)
% 5.18/1.81 === Backtracking. Learning clause 66:2:0:[49.2,27.1]:: p2(f11(f4(c41),c40),f9(c30)) -> p10(c40,c32)
% 5.18/1.81 === Clause set with instances from active satisfied. Growing active. New size: 164
% 5.18/1.81 === Restarting.
% 5.18/1.81 === Conflict found: 64:2:1:[59.2,54.1]:Top: p10(x0,f16(c36)) -> p10(x0,c37) {x0 -> f16(c27)}
% 5.18/1.81 === Backtracking. Learning clause 67:2:1:[64.1,20.2]:Top: p12(x0,c36) -> p10(f16(x0),c37)
% 5.18/1.81 === Backtracking. Learning clause 68:2:1:[30.1,20.2,12.1]:Top: p12(c31,x0) -> p10(f16(x0),c32)
% 5.18/1.81 === Backtracking. Learning clause 69:3:1:[30.1,67.2,68.2]:Top: p12(x0,c36),p12(c31,x0) -> p10(c37,c32)
% 5.18/1.81 === Backtracking. Learning clause 70:2:1:[38.2,29.1]:Top: p12(f13(f16(c39),f17(c39)),x0) -> p12(x0,f13(c40,c41))
% 5.18/1.81 === Backtracking. Learning clause 71:3:2:[41.3,29.1]:TopTop: p14(x0,x1),p24(x0,f13(f16(c39),f17(c39))) -> p24(x1,f13(c40,c41))
% 5.18/1.81 === Backtracking. Learning clause 72:2:2:[50.2,28.1]:TopTop: p24(f15(c29,f13(x0,x1)),f13(c32,c33)) -> p2(x1,c38)
% 5.18/1.81 === Backtracking. Learning clause 73:3:2:[41.2,28.1]:TopTop: p14(f15(c29,f13(c37,c38)),x0),p12(f13(c32,c33),x1) -> p24(x0,x1)
% 5.18/1.81 === Backtracking. Learning clause 74:3:2:[41.2,27.1]:TopTop: p14(f15(c29,f13(c40,c41)),x0),p12(f13(c32,c33),x1) -> p24(x0,x1)
% 5.18/1.81 === Backtracking. Learning clause 75:3:3:[41.1,9.1,72.1]:TopTopTop: p24(f15(c29,f13(x0,x1)),x2),p12(x2,f13(c32,c33)) -> p2(x1,c38)
% 5.18/1.81 === Clause set with instances from active satisfied. Growing active. New size: 195
% 5.18/1.81 === Restarting.
% 5.18/1.81 === Conflict found: 52:2:1:[35.2,11.1]:Top: p2(c41,x0) -> p2(x0,c38) {x0 -> c27}
% 5.18/1.81 === Backtracking. Learning clause 76:2:1:[52.1,62.2]:Top: p2(x0,c41) -> p2(x0,c38)
% 5.18/1.81 === Conflict found: 59:2:2:[30.2,2.1]:TopTop: p10(x0,x1) -> p10(x1,x0) {x0 -> f16(c31), x1 -> c32}
% 5.18/1.81 === Backtracking. Learning clause 77:2:1:[59.1,12.1,30.2]:Top: p10(c32,x0) -> p10(x0,f16(c31))
% 5.18/1.81 === Conflict found: 59:2:2:[30.2,2.1]:TopTop: p10(x0,x1) -> p10(x1,x0) {x0 -> f16(c36), x1 -> c37}
% 5.18/1.81 === Backtracking. Learning clause 78:2:1:[59.1,16.1,30.2]:Top: p10(c37,x0) -> p10(x0,f16(c36))
% 5.18/1.81 === Conflict found: 60:2:2:[31.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c28), x1 -> c29}
% 5.18/1.81 === Backtracking. Learning clause 79:1:0:[60.1,13.1]:: -> p7(c29,f8(c28))
% 5.18/1.81 === Backtracking. Learning clause 80:4:3:[35.3,56.1,35.3]:TopTopTop: p2(x0,x1),p2(x2,x0),p2(x2,f17(c31)) -> p2(x1,c33)
% 5.18/1.81 === Conflict found: 62:2:2:[35.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f17(c31), x1 -> c33}
% 5.18/1.81 === Backtracking. Learning clause 81:1:0:[62.1,15.1]:: -> p2(c33,f17(c31))
% 5.18/1.81 === Conflict found: 62:2:2:[35.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f17(c36), x1 -> c38}
% 5.18/1.81 === Backtracking. Learning clause 82:2:1:[62.1,14.1,35.2]:Top: p2(c38,x0) -> p2(x0,f17(c36))
% 5.18/1.81 === Conflict found: 63:2:2:[37.2,9.1]:TopTop: p14(x0,x1) -> p14(x1,x0) {x0 -> c35, x1 -> f18(c34)}
% 5.18/1.81 === Backtracking. Learning clause 83:1:0:[63.2,17.1]:: p14(c35,f18(c34)) ->
% 5.18/1.81 === Conflict found: 63:2:2:[37.2,9.1]:TopTop: p14(x0,x1) -> p14(x1,x0) {x0 -> c27, x1 -> f15(c29,f13(c37,c38))}
% 5.18/1.81 === Backtracking. Learning clause 84:3:2:[63.2,73.1]:TopTop: p14(x0,f15(c29,f13(c37,c38))),p12(f13(c32,c33),x1) -> p24(x0,x1)
% 5.18/1.81 === Backtracking. Learning clause 85:3:3:[41.1,9.1]:TopTopTop: p24(x0,x1),p12(x1,x2) -> p24(x0,x2)
% 5.18/1.81 === Conflict found: 85:3:3:[41.1,9.1]:TopTopTop: p24(x0,x1),p12(x1,x2) -> p24(x0,x2) {x0 -> f15(c29,f13(c27,c27)), x1 -> f13(c27,c27), x2 -> f13(c40,c41)}
% 5.18/1.81 === Backtracking. Learning clause 86:5:6:[85.3,47.1,85.3]:TopTopTopTopTopTop: p12(x0,f13(x1,x2)),p24(f15(c29,f13(x3,x4)),x5),p12(x5,x0) -> p10(x3,x1),p25(f21(c27,x3),x1)
% 5.18/1.81 === Conflict found: 85:3:3:[41.1,9.1]:TopTopTop: p24(x0,x1),p12(x1,x2) -> p24(x0,x2) {x0 -> f15(c29,f13(c37,c38)), x1 -> f13(c32,c33), x2 -> c27}
% 5.18/1.81 === Backtracking. Learning clause 87:2:1:[85.1,28.1]:Top: p12(f13(c32,c33),x0) -> p24(f15(c29,f13(c37,c38)),x0)
% 5.18/1.81 === Clause set with instances from active satisfied. Growing active. New size: 221
% 5.18/1.81 === Restarting.
% 5.18/1.81 === Conflict found: 69:3:1:[30.1,67.2,68.2]:Top: p12(x0,c36),p12(c31,x0) -> p10(c37,c32) {x0 -> c27}
% 5.18/1.81 === Backtracking. Learning clause 88:4:2:[69.2,38.3]:TopTop: p12(x0,c36),p12(x1,c31),p12(x1,x0) -> p10(c37,c32)
% 5.18/1.81 === Backtracking. Learning clause 89:3:2:[30.2,68.2,59.2]:TopTop: p12(c31,x0),p10(x1,f16(x0)) -> p10(x1,c32)
% 5.18/1.81 === Backtracking. Learning clause 90:2:1:[31.2,79.1]:Top: p7(c29,x0) -> p7(x0,f8(c28))
% 5.18/1.81 === Backtracking. Learning clause 91:3:2:[35.2,81.1,35.2]:TopTop: p2(c33,x0),p2(x0,x1) -> p2(x1,f17(c31))
% 5.18/1.81 === Backtracking. Learning clause 92:3:3:[35.2,62.2,62.2]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0)
% 5.18/1.81 === Conflict found: 92:3:3:[35.2,62.2,62.2]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> c27, x1 -> c38, x2 -> c41}
% 5.18/1.81 === Backtracking. Learning clause 93:2:1:[92.2,11.1,62.1]:Top: p2(x0,c38) -> p2(x0,c41)
% 5.18/1.81 === Conflict found: 92:3:3:[35.2,62.2,62.2]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> c27, x1 -> f17(c36), x2 -> c38}
% 5.18/1.81 === Backtracking. Learning clause 94:3:2:[92.2,82.2]:TopTop: p2(x0,f17(c36)),p2(c38,x1) -> p2(x1,x0)
% 5.18/1.81 === Backtracking. Learning clause 95:3:2:[31.1,21.2,60.2,60.1,90.2]:TopTop: p6(c28,x0),p7(c29,x1) -> p7(x1,f8(x0))
% 5.18/1.81 === Conflict found: 92:3:3:[35.2,62.2,62.2]:TopTopTop: p2(x0,x1),p2(x2,x1) -> p2(x2,x0) {x0 -> c33, x1 -> f17(c31), x2 -> f17(c27)}
% 5.18/1.81 === Backtracking. Learning clause 96:3:2:[92.2,25.2,92.1,81.1]:TopTop: p12(x0,c31),p2(x1,c33) -> p2(x1,f17(x0))
% 5.18/1.81 === Backtracking. Learning clause 97:3:3:[42.1,6.1]:TopTopTop: p25(x0,x1),p10(x1,x2) -> p25(x0,x2)
% 5.18/1.81 === Backtracking. Learning clause 98:2:2:[34.2,6.1]:TopTop: p20(x0,x1) -> p20(x1,x0)
% 5.18/1.81 === Backtracking. Learning clause 99:2:2:[38.2,10.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 5.18/1.81 === Conflict found: 99:2:2:[38.2,10.1]:TopTop: p12(x0,x1) -> p12(x1,x0) {x0 -> c27, x1 -> f13(f16(c39),f17(c39))}
% 5.18/1.81 === Backtracking. Learning clause 100:2:1:[99.2,70.1]:Top: p12(x0,f13(f16(c39),f17(c39))) -> p12(x0,f13(c40,c41))
% 5.18/1.81 === Backtracking. Learning clause 101:5:5:[41.4,75.1]:TopTopTopTopTop: p14(x0,f15(c29,f13(x1,x2))),p24(x0,x3),p12(x3,x4),p12(x4,f13(c32,c33)) -> p2(x2,c38)
% 5.18/1.81 === Conflict found: 86:5:6:[85.3,47.1,85.3]:TopTopTopTopTopTop: p12(x0,f13(x1,x2)),p24(f15(c29,f13(x3,x4)),x5),p12(x5,x0) -> p10(x3,x1),p25(f21(c27,x3),x1) {x0 -> f13(c32,c33), x1 -> c32, x2 -> c33, x3 -> c37, x4 -> c38, x5 -> c27}
% 5.18/1.81 === Backtracking. Learning clause 102:4:3:[86.2,87.2,10.1]:TopTopTop: p12(x0,f13(x1,x2)),p12(f13(c32,c33),x0) -> p10(c37,x1),p25(f21(c27,c37),x1)
% 5.18/1.81 === Conflict found: 85:3:3:[41.1,9.1]:TopTopTop: p24(x0,x1),p12(x1,x2) -> p24(x0,x2) {x0 -> f15(c29,f13(c27,c27)), x1 -> f13(c27,c27), x2 -> f13(c40,c41)}
% 5.18/1.81 === Backtracking. Learning clause 103:4:4:[85.3,75.1]:TopTopTopTop: p24(f15(c29,f13(x0,x1)),x2),p12(x2,x3),p12(x3,f13(c32,c33)) -> p2(x1,c38)
% 5.18/1.81 === Conflict found: 86:5:6:[85.3,47.1,85.3]:TopTopTopTopTopTop: p12(x0,f13(x1,x2)),p24(f15(c29,f13(x3,x4)),x5),p12(x5,x0) -> p10(x3,x1),p25(f21(c27,x3),x1) {x0 -> c27, x1 -> c32, x2 -> c33, x3 -> c40, x4 -> c41, x5 -> f13(c32,c33)}
% 5.18/1.81 === Backtracking. Learning clause 104:4:3:[86.2,27.1]:TopTopTop: p12(x0,f13(x1,x2)),p12(f13(c32,c33),x0) -> p10(c40,x1),p25(f21(c27,c40),x1)
% 5.18/1.81 === Conflict found: 85:3:3:[41.1,9.1]:TopTopTop: p24(x0,x1),p12(x1,x2) -> p24(x0,x2) {x0 -> f15(c29,f13(f16(c39),f17(c39))), x1 -> c27, x2 -> f13(c32,c33)}
% 5.18/1.81 === Backtracking. Learning clause 105:4:3:[85.3,39.1,41.4]:TopTopTop: p12(x0,f13(c32,c33)),p14(x1,f15(c29,f13(f16(c39),f17(c39)))),p24(x1,x2),p12(x2,x0) ->
% 5.18/1.81 === Clause set with instances from active satisfied. Growing active. New size: 252
% 5.18/1.81 === Restarting.
% 5.18/1.81 === Conflict found: 102:4:3:[86.2,87.2,10.1]:TopTopTop: p12(x0,f13(x1,x2)),p12(f13(c32,c33),x0) -> p10(c37,x1),p25(f21(c27,c37),x1) {x0 -> f13(c32,c33), x1 -> c32, x2 -> c33}
% 5.18/1.81 === Backtracking. Learning clause 106:2:0:[102.1,10.1]:: -> p10(c37,c32),p25(f21(c27,c37),c32)
% 5.18/1.81 === Conflict found: 74:3:2:[41.2,27.1]:TopTop: p14(f15(c29,f13(c40,c41)),x0),p12(f13(c32,c33),x1) -> p24(x0,x1) {x0 -> c27, x1 -> f13(c32,c33)}
% 5.18/1.81 === Backtracking. Learning clause 107:2:1:[74.2,10.1,63.2]:Top: p14(x0,f15(c29,f13(c40,c41))) -> p24(x0,f13(c32,c33))
% 5.18/1.81 === Backtracking. Learning clause 108:8:9:[41.1,45.3,86.2]:TopTopTopTopTopTopTopTopTop: p24(f15(x0,x1),x2),p12(x2,x3),p12(x1,f13(x4,x5)),p7(x0,c29),p12(x6,f13(x7,x8)),p12(x3,x6) -> p10(x4,x7),p25(f21(c27,x4),x7)
% 5.18/1.81 === Backtracking. Learning clause 109:5:6:[41.1,45.3]:TopTopTopTopTopTop: p24(f15(x0,x1),x2),p12(x2,x3),p12(x1,x4),p7(x0,x5) -> p24(f15(x5,x4),x3)
% 5.18/1.81 === Backtracking. Learning clause 110:4:5:[37.2,45.3]:TopTopTopTopTop: p14(f15(x0,x1),x2),p12(x1,x3),p7(x0,x4) -> p14(x2,f15(x4,x3))
% 5.18/1.81 === Conflict found: 107:2:1:[74.2,10.1,63.2]:Top: p14(x0,f15(c29,f13(c40,c41))) -> p24(x0,f13(c32,c33)) {x0 -> c27}
% 5.18/1.81 === Backtracking. Learning clause 111:4:3:[107.1,110.4]:TopTopTop: p14(f15(x0,x1),x2),p12(x1,f13(c40,c41)),p7(x0,c29) -> p24(x2,f13(c32,c33))
% 5.18/1.81 === Conflict found: 101:5:5:[41.4,75.1]:TopTopTopTopTop: p14(x0,f15(c29,f13(x1,x2))),p24(x0,x3),p12(x3,x4),p12(x4,f13(c32,c33)) -> p2(x2,c38) {x0 -> c27, x1 -> c27, x2 -> c27, x3 -> f13(c32,c33), x4 -> f13(c32,c33)}
% 5.18/1.81 === Backtracking. Learning clause 112:7:7:[101.3,10.1,110.4,111.4]:TopTopTopTopTopTopTop: p14(f15(x0,x1),x2),p12(x1,f13(x3,x4)),p7(x0,c29),p14(f15(x5,x6),x2),p12(x6,f13(c40,c41)),p7(x5,c29) -> p2(x4,c38)
% 5.18/1.81 === Conflict found: 73:3:2:[41.2,28.1]:TopTop: p14(f15(c29,f13(c37,c38)),x0),p12(f13(c32,c33),x1) -> p24(x0,x1) {x0 -> c27, x1 -> f13(c32,c33)}
% 5.18/1.81 === Backtracking. Learning clause 113:2:1:[73.2,10.1,63.2]:Top: p14(x0,f15(c29,f13(c37,c38))) -> p24(x0,f13(c32,c33))
% 5.18/1.81 === Conflict found: 102:4:3:[86.2,87.2,10.1]:TopTopTop: p12(x0,f13(x1,x2)),p12(f13(c32,c33),x0) -> p10(c37,x1),p25(f21(c27,c37),x1) {x0 -> f13(f16(c39),f17(c39)), x1 -> c40, x2 -> c41}
% 5.18/1.81 === Backtracking. Learning clause 114:3:0:[102.1,29.1]:: p12(f13(c32,c33),f13(f16(c39),f17(c39))) -> p10(c37,c40),p25(f21(c27,c37),c40)
% 5.18/1.81 === Conflict found: 99:2:2:[38.2,10.1]:TopTop: p12(x0,x1) -> p12(x1,x0) {x0 -> f13(f16(c39),f17(c39)), x1 -> f13(c40,c41)}
% 5.18/1.81 === Backtracking. Learning clause 115:2:1:[99.1,29.1,85.2]:Top: p24(x0,f13(c40,c41)) -> p24(x0,f13(f16(c39),f17(c39)))
% 5.18/1.81 === Backtracking. Learning clause 116:6:7:[41.4,47.1,10.1,110.4]:TopTopTopTopTopTopTop: p24(x0,f13(x1,x2)),p14(f15(x3,x4),x0),p12(x4,f13(x5,x6)),p7(x3,c29) -> p10(x5,x1),p25(f21(c27,x5),x1)
% 5.18/1.81 === Backtracking. Learning clause 117:7:10:[50.1,85.3,109.5]:TopTopTopTopTopTopTopTopTopTop: p24(f15(c29,f13(x0,x1)),x2),p12(x2,f13(x3,x4)),p24(f15(x5,x6),x7),p12(x7,f13(x3,x4)),p12(x6,f13(x8,x9)),p7(x5,c29) -> p2(x1,x9)
% 5.18/1.81 === Backtracking. Learning clause 118:2:0:[49.2,28.1]:: p2(f11(f4(c38),c37),f9(c30)) -> p10(c37,c32)
% 5.18/1.81 === Conflict found: 109:5:6:[41.1,45.3]:TopTopTopTopTopTop: p24(f15(x0,x1),x2),p12(x2,x3),p12(x1,x4),p7(x0,x5) -> p24(f15(x5,x4),x3) {x0 -> c29, x1 -> f13(c40,c41), x2 -> f13(c32,c33), x3 -> f13(c32,c33), x4 -> f13(f16(c39),f17(c39)), x5 -> c29}
% 5.18/1.81 === Backtracking. Learning clause 119:3:0:[109.5,39.1,27.1]:: p12(f13(c32,c33),f13(c32,c33)),p12(f13(c40,c41),f13(f16(c39),f17(c39))),p7(c29,c29) ->
% 5.18/1.81 === Conflict found: 99:2:2:[38.2,10.1]:TopTop: p12(x0,x1) -> p12(x1,x0) {x0 -> f13(f16(c39),f17(c39)), x1 -> f13(c40,c41)}
% 5.18/1.81
% 5.18/1.81 SZS status Unsatisfiable
% 5.18/1.81
% 5.18/1.81 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/1.81
% 5.18/1.81 SPASS-SCL-FOL Statistics:
% 5.18/1.81 Number of learned clauses: 68
% 5.18/1.81 Number of propagations: 3199
% 5.18/1.81 Number of decisions: 1617
% 5.18/1.81 Number of resolutions: 101
% 5.18/1.81 Number of condensations: 0
% 5.18/1.81 Number of sub resolutions: 0
% 5.18/1.81 Number of input literals (deduplicated): 51
% 5.18/1.81 Number of grows: 5
% 5.18/1.81 Number of considered ground atoms: 252
% 5.18/1.81
% 5.18/1.81 Needed: 0:00:01.19
% 5.18/1.81
%------------------------------------------------------------------------------