%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN673-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 : n021.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:08 PM UTC 2026
% Result : Unsatisfiable 46.21s 12.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN673-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 : n021.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:58 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 SPASS-SCL-FOL version:
% 0.19/0.38 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 46.21/12.03 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.21/12.03 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.21/12.03 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.21/12.03 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.21/12.03 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.21/12.03 Execution resolution_2 ended with status: unsatisfiable
% 46.21/12.03 Used heuristic: resolution_2
% 46.21/12.03
% 46.21/12.03 Input Clauses:
% 46.21/12.03
% 46.21/12.03 Predicates: p10 p9 p7 p6 p4 p3 p25 p23 p20 p2 p18 p16 p15 p13 p11 p29 p27 p28
% 46.21/12.03 Fol Constants: c35 c41 c33 c34 c30 c38 c32 c31 c40 c37 c42 c39 c36 c43
% 46.21/12.03 Fol Functions: f19 f14 f8 f5 f12 f21 f24 f17 f26 f22
% 46.21/12.03 Problem Properties:
% 46.21/12.03 This is a full first-order problem without equality.
% 46.21/12.03
% 46.21/12.03 After reduction: Problem Properties:
% 46.21/12.03 This is a full first-order problem without equality.
% 46.21/12.03
% 46.21/12.03
% 46.21/12.03 Reduced Input Clauses:
% 46.21/12.03
% 46.21/12.03 Most General Atoms: p6(x1,x2) p4(x1,x2) p20(x1,x2) p2(x1,x2) p15(x1,x2) p10(x1,x3) p29(x2,x3) p11(x0,x3) p27(x3,x2) p16(x2,x3) p28(x1,x3) p3(x2,x3) p13(x2,x3) p9(x2,x3) p18(x2,x3) p25(x2,x3) p7(x2,x3) p23(x2,x3)
% 46.21/12.03
% 46.21/12.03 === Starting SPASS-SCL-FOL A Little Less Naive, considering 59 atoms initially, heuristics mode: resolution_2 ===
% 46.21/12.03
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 70
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 56:2:0:[53.1,1.1]:: p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31) -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
% 46.21/12.03 === Backtracking. Learning clause 57:2:0:[52.1,1.1]:: -> p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39),p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 70
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 70
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 70
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 134
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 134
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 134
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 58:2:1:[37.1,52.2,53.2]:Top: p10(x0,f14(f19(c35,c37),c39)) -> p29(f5(c33,f8(c34,c30)),x0)
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 134
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 134
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 198
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 198
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 198
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 198
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 205
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 59:1:0:[20.1,12.1]:: -> p28(f21(c30,c40),c31)
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 269
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 269
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 60:5:5:[33.3,40.3]:TopTopTopTopTop: p16(x0,x1),p16(x0,x2),p20(x3,x4),p28(x3,x1) -> p28(x4,x2)
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 269
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 269
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Conflict found: 58:2:1:[37.1,52.2,53.2]:Top: p10(x0,f14(f19(c35,c37),c39)) -> p29(f5(c33,f8(c34,c30)),x0) {x0 -> f14(f19(c35,c37),c39)}
% 46.21/12.03 === Backtracking. Learning clause 61:1:0:[58.1,1.1]:: -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 280
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 62:2:0:[53.1,16.1]:: p28(f21(c30,f26(c43,f14(f19(c35,f14(f19(c35,c37),c39)),c41))),c31) -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),c41))
% 46.21/12.03 === Conflict found: 58:2:1:[37.1,52.2,53.2]:Top: p10(x0,f14(f19(c35,c37),c39)) -> p29(f5(c33,f8(c34,c30)),x0) {x0 -> f14(f19(c35,f14(f19(c35,c37),c39)),c41)}
% 46.21/12.03 === Backtracking. Learning clause 63:1:0:[58.1,16.1]:: -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),c41))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 344
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 350
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 64:3:2:[38.4,17.1]:TopTop: p29(x0,x1),p4(x0,f5(c33,f8(c34,c30))),p10(x1,c38) ->
% 46.21/12.03 === Backtracking. Learning clause 65:2:0:[52.3,17.1]:: p10(c38,f14(f19(c35,c37),c39)) -> p29(f24(c42,f26(c43,c38)),c39)
% 46.21/12.03 === Conflict found: 58:2:1:[37.1,52.2,53.2]:Top: p10(x0,f14(f19(c35,c37),c39)) -> p29(f5(c33,f8(c34,c30)),x0) {x0 -> c38}
% 46.21/12.03 === Backtracking. Learning clause 66:1:0:[58.2,17.1]:: p10(c38,f14(f19(c35,c37),c39)) ->
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 353
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 67:3:2:[39.1,21.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,c37),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 68:2:1:[55.2,21.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,c37),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Backtracking. Learning clause 69:1:0:[18.1,21.1]:: -> p29(f5(c33,f8(c34,c30)),c37)
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 357
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 70:3:2:[38.3,41.1]:TopTop: p29(x0,c38),p4(x0,x1) -> p29(x1,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)))
% 46.21/12.03 === Backtracking. Learning clause 71:2:1:[22.1,41.1]:Top: p10(c38,x0) -> p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),x0)
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 362
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Conflict found: 60:5:5:[33.3,40.3]:TopTopTopTopTop: p16(x0,x1),p16(x0,x2),p20(x3,x4),p28(x3,x1) -> p28(x4,x2) {x0 -> c35, x1 -> c31, x2 -> c35, x3 -> f21(c30,c40), x4 -> c35}
% 46.21/12.03 === Backtracking. Learning clause 72:3:2:[60.4,59.1,12.1]:TopTop: p16(x0,c31),p20(f21(c30,c40),x1) -> p28(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 73:3:2:[40.2,59.1]:TopTop: p20(f21(c30,c40),x0),p16(c31,x1) -> p28(x0,x1)
% 46.21/12.03 === Backtracking. Learning clause 74:2:1:[55.1,59.1]:Top: p27(f12(c32,x0),f5(c33,f8(c34,c30))) -> p27(f12(c32,f14(f19(c35,x0),f17(c36,c40))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Conflict found: 68:2:1:[55.2,21.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,c37),f17(c36,x0))),f5(c33,f8(c34,c30))) {x0 -> c40}
% 46.21/12.03 === Backtracking. Learning clause 75:1:0:[68.1,59.1]:: -> p27(f12(c32,f14(f19(c35,c37),f17(c36,c40))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 426
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 427
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 76:3:2:[38.1,61.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p10(f14(f19(c35,c37),c39),x1) -> p29(x0,x1)
% 46.21/12.03 === Conflict found: 64:3:2:[38.4,17.1]:TopTop: p29(x0,x1),p4(x0,f5(c33,f8(c34,c30))),p10(x1,c38) -> {x0 -> f5(c33,f8(c34,c30)), x1 -> f14(f19(c35,c37),c39)}
% 46.21/12.03 === Backtracking. Learning clause 77:2:0:[64.1,61.1]:: p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))),p10(f14(f19(c35,c37),c39),c38) ->
% 46.21/12.03 === Backtracking. Learning clause 78:1:0:[19.1,61.1]:: -> p27(f12(c32,f14(f19(c35,c37),c39)),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 427
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 79:3:2:[38.1,63.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p10(f14(f19(c35,f14(f19(c35,c37),c39)),c41),x1) -> p29(x0,x1)
% 46.21/12.03 === Conflict found: 64:3:2:[38.4,17.1]:TopTop: p29(x0,x1),p4(x0,f5(c33,f8(c34,c30))),p10(x1,c38) -> {x0 -> f5(c33,f8(c34,c30)), x1 -> f14(f19(c35,f14(f19(c35,c37),c39)),c41)}
% 46.21/12.03 === Backtracking. Learning clause 80:2:0:[64.1,63.1]:: p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))),p10(f14(f19(c35,f14(f19(c35,c37),c39)),c41),c38) ->
% 46.21/12.03 === Backtracking. Learning clause 81:1:0:[19.1,63.1]:: -> p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 427
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 82:2:1:[22.3,66.1]:Top: p10(x0,c38),p10(x0,f14(f19(c35,c37),c39)) ->
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 429
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 83:3:2:[38.1,69.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p10(c37,x1) -> p29(x0,x1)
% 46.21/12.03 === Conflict found: 64:3:2:[38.4,17.1]:TopTop: p29(x0,x1),p4(x0,f5(c33,f8(c34,c30))),p10(x1,c38) -> {x0 -> f5(c33,f8(c34,c30)), x1 -> c37}
% 46.21/12.03 === Backtracking. Learning clause 84:2:0:[64.1,69.1]:: p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))),p10(c37,c38) ->
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 493
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 495
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 85:3:2:[39.1,75.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,f14(f19(c35,c37),f17(c36,c40))),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 86:2:1:[55.2,75.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Conflict found: 74:2:1:[55.1,59.1]:Top: p27(f12(c32,x0),f5(c33,f8(c34,c30))) -> p27(f12(c32,f14(f19(c35,x0),f17(c36,c40))),f5(c33,f8(c34,c30))) {x0 -> f14(f19(c35,c37),f17(c36,c40))}
% 46.21/12.03 === Backtracking. Learning clause 87:1:0:[74.1,75.1]:: -> p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 497
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 88:3:2:[39.1,78.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,f14(f19(c35,c37),c39)),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 89:2:1:[55.2,78.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Conflict found: 74:2:1:[55.1,59.1]:Top: p27(f12(c32,x0),f5(c33,f8(c34,c30))) -> p27(f12(c32,f14(f19(c35,x0),f17(c36,c40))),f5(c33,f8(c34,c30))) {x0 -> f14(f19(c35,c37),c39)}
% 46.21/12.03 === Backtracking. Learning clause 90:1:0:[74.1,78.1]:: -> p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 499
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 91:3:2:[39.1,81.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 92:2:1:[55.2,81.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Conflict found: 74:2:1:[55.1,59.1]:Top: p27(f12(c32,x0),f5(c33,f8(c34,c30))) -> p27(f12(c32,f14(f19(c35,x0),f17(c36,c40))),f5(c33,f8(c34,c30))) {x0 -> f14(f19(c35,f14(f19(c35,c37),c39)),c41)}
% 46.21/12.03 === Backtracking. Learning clause 93:1:0:[74.1,81.1]:: -> p27(f12(c32,f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),f17(c36,c40))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 503
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 94:3:2:[39.1,87.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40))),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 95:2:1:[55.2,87.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40))),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Backtracking. Learning clause 96:1:0:[18.1,87.1]:: -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 567
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 569
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 97:3:2:[39.1,90.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 98:2:1:[55.2,90.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Backtracking. Learning clause 99:1:0:[18.1,90.1]:: -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 571
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 100:3:2:[39.1,93.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p11(f12(c32,f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),f17(c36,c40))),x1) -> p27(x1,x0)
% 46.21/12.03 === Backtracking. Learning clause 101:2:1:[55.2,93.1]:Top: p28(f21(c30,x0),c31) -> p27(f12(c32,f14(f19(c35,f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),f17(c36,c40))),f17(c36,x0))),f5(c33,f8(c34,c30)))
% 46.21/12.03 === Backtracking. Learning clause 102:1:0:[18.1,93.1]:: -> p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,f14(f19(c35,c37),c39)),c41)),f17(c36,c40)))
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 573
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 103:3:2:[38.1,96.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p10(f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40)),x1) -> p29(x0,x1)
% 46.21/12.03 === Conflict found: 64:3:2:[38.4,17.1]:TopTop: p29(x0,x1),p4(x0,f5(c33,f8(c34,c30))),p10(x1,c38) -> {x0 -> f5(c33,f8(c34,c30)), x1 -> f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40))}
% 46.21/12.03 === Backtracking. Learning clause 104:2:0:[64.1,96.1]:: p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))),p10(f14(f19(c35,f14(f19(c35,c37),f17(c36,c40))),f17(c36,c40)),c38) ->
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 574
% 46.21/12.03 === Restarting.
% 46.21/12.03 === Backtracking. Learning clause 105:3:2:[38.1,99.1]:TopTop: p4(f5(c33,f8(c34,c30)),x0),p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),x1) -> p29(x0,x1)
% 46.21/12.03 === Conflict found: 64:3:2:[38.4,17.1]:TopTop: p29(x0,x1),p4(x0,f5(c33,f8(c34,c30))),p10(x1,c38) -> {x0 -> f5(c33,f8(c34,c30)), x1 -> f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))}
% 46.21/12.03 === Backtracking. Learning clause 106:2:0:[64.1,99.1]:: p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))),p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),c38) ->
% 46.21/12.03 === Clause set with instances from active satisfied. Growing active. New size: 638
% 46.21/12.03
% 46.21/12.03 SZS status Unsatisfiable
% 46.21/12.03
% 46.21/12.03 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.21/12.03
% 46.21/12.03 SPASS-SCL-FOL Statistics:
% 46.21/12.03 Number of learned clauses: 51
% 46.21/12.03 Number of propagations: 7507
% 46.21/12.03 Number of decisions: 3521
% 46.21/12.03 Number of resolutions: 57
% 46.21/12.03 Number of condensations: 0
% 46.21/12.03 Number of sub resolutions: 0
% 46.21/12.03 Number of input literals (deduplicated): 59
% 46.21/12.03 Number of grows: 40
% 46.21/12.03 Number of considered ground atoms: 638
% 46.21/12.03
% 46.21/12.03 Needed: 0:0:11.47
% 46.21/12.03
%------------------------------------------------------------------------------