%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN688-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 : n018.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 19.91s 4.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.15 % Problem : SYN688-1 : TPTP v9.2.1. Released v2.5.0.
% 0.10/0.16 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.38 % Computer : n018.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:47:17 EDT 2026
% 0.19/0.38 % CPUTime :
% 0.19/0.38 SPASS-SCL-FOL version:
% 0.31/0.47 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 19.91/4.53 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.91/4.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.91/4.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.91/4.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.91/4.53 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.91/4.53 Execution resolution_1 ended with status: unsatisfiable
% 19.91/4.53 Used heuristic: resolution_1
% 19.91/4.53
% 19.91/4.53 Input Clauses:
% 19.91/4.53
% 19.91/4.53 Predicates: p27 p23 p10 p9 p3 p21 p2 p18 p12 p22 p24 p26 p25 p28 p29
% 19.91/4.53 Fol Constants: c34 c43 c35 c41 c42 c46 c45 c36 c44 c30 c31 c32 c33 c39 c40 c37 c38
% 19.91/4.53 Fol Functions: f17 f19 f20 f16 f15 f4 f11 f5 f6 f7 f13 f14 f8
% 19.91/4.53 Problem Properties:
% 19.91/4.53 This is a full first-order problem without equality.
% 19.91/4.53
% 19.91/4.53 After reduction: Problem Properties:
% 19.91/4.53 This is a full first-order problem without equality.
% 19.91/4.53
% 19.91/4.53
% 19.91/4.53 Reduced Input Clauses:
% 19.91/4.53
% 19.91/4.53 Most General Atoms: p23(x1) p27(x1) p9(x1,x2) p3(x1,x2) p12(x1,x2) p21(x2,x3) p22(x3,x1) p18(x2,x3) p29(x3,x1) p28(x3,x1) p10(x2,x3) p24(x3,x1) p26(x1,x0) p25(x1,x0) p2(x2,x3)
% 19.91/4.53
% 19.91/4.53 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_1 ===
% 19.91/4.53
% 19.91/4.53 === Backtracking. Learning clause 63:2:2:[32.2,5.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 19.91/4.53 === Backtracking. Learning clause 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 19.91/4.53 === Backtracking. Learning clause 65:2:2:[36.2,9.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 19.91/4.53 === Backtracking. Learning clause 66:2:2:[37.2,10.1]:TopTop: p18(x0,x1) -> p18(x1,x0)
% 19.91/4.53 === Backtracking. Learning clause 67:2:1:[34.2,19.1]:Top: p3(f15(f16(c43,c36)),x0) -> p3(x0,c44)
% 19.91/4.53 === Backtracking. Learning clause 68:3:2:[37.1,31.2,66.1]:TopTop: p18(f19(f17(x0)),x1),p27(x0) -> p18(x1,f20(f19(x0)))
% 19.91/4.53 === Backtracking. Learning clause 69:2:1:[34.2,39.1]:Top: p3(c30,x0) -> p3(x0,f4(f5(f6(f6(f6(f6(f6(f7(c31)))))))))
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 115
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Conflict found: 63:2:2:[32.2,5.1]:TopTop: p10(x0,x1) -> p10(x1,x0) {x0 -> c34, x1 -> f17(c34)}
% 19.91/4.53 === Backtracking. Learning clause 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0)
% 19.91/4.53 === Backtracking. Learning clause 71:5:3:[44.2,49.4,10.1,44.2,66.2]:TopTopTop: p27(x0),p25(x0,x0),p18(x1,x2),p18(x1,f19(x0)) -> p28(x2,x1)
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 183
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Backtracking. Learning clause 72:3:2:[42.2,12.1]:TopTop: p21(c42,x0),p21(c41,x1) -> p22(x1,x0)
% 19.91/4.53 === Backtracking. Learning clause 73:7:5:[44.4,40.3,10.1,44.4]:TopTopTopTopTop: p18(x0,f19(x1)),p27(x2),p27(x1),p18(x3,x0),p28(x4,x3),p18(x4,f19(x2)) -> p25(x2,x1)
% 19.91/4.53 === Backtracking. Learning clause 74:2:1:[34.2,54.1]:Top: p3(c32,x0) -> p3(x0,f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31))))))))
% 19.91/4.53 === Backtracking. Learning clause 75:2:0:[20.2,56.1]:: p23(c35) -> p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31)))))
% 19.91/4.53 === Backtracking. Learning clause 77:1:0:[3.0,76.0,21.2,56.1]:: -> p27(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31)))))
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c33, x1 -> f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31))))}
% 19.91/4.53 === Backtracking. Learning clause 78:2:0:[70.1,55.1]:: p23(f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31))))) -> p23(c33)
% 19.91/4.53 === Backtracking. Learning clause 79:3:1:[32.2,58.1,21.2]:Top: p10(c40,x0),p27(x0) -> p27(f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Backtracking. Learning clause 80:3:1:[32.2,59.1,20.2]:Top: p10(c37,x0),p23(x0) -> p23(f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Backtracking. Learning clause 81:2:1:[32.2,59.1]:Top: p10(c37,x0) -> p10(x0,f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c36, x1 -> f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31))))))))))))))))))))))))))}
% 19.91/4.53 === Backtracking. Learning clause 82:2:0:[70.1,61.1]:: p23(f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31))))))))))))))))))))))))))) -> p23(c36)
% 19.91/4.53 === Backtracking. Learning clause 83:2:0:[20.2,62.1]:: p23(c34) -> p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c31))))))))))))))))))))))))))))
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 198
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Backtracking. Learning clause 84:5:4:[46.4,16.1,46.4,63.2]:TopTopTopTop: p10(x0,f17(c43)),p10(x1,x2),p25(x3,x1),p10(x3,x0),p10(c34,x2) ->
% 19.91/4.53 === Conflict found: 68:3:2:[37.1,31.2,66.1]:TopTop: p18(f19(f17(x0)),x1),p27(x0) -> p18(x1,f20(f19(x0))) {x0 -> c34, x1 -> f19(c34)}
% 19.91/4.53 === Backtracking. Learning clause 85:7:6:[68.1,25.2,43.1,43.2,66.2]:TopTopTopTopTopTop: p27(x0),p10(f17(x0),x1),p29(x2,f19(x1)),p18(x2,x3),p18(x3,x4),p18(x5,f20(f19(x0))) -> p29(x4,x5)
% 19.91/4.53 === Conflict found: 68:3:2:[37.1,31.2,66.1]:TopTop: p18(f19(f17(x0)),x1),p27(x0) -> p18(x1,f20(f19(x0))) {x0 -> c34, x1 -> f19(c34)}
% 19.91/4.53 === Backtracking. Learning clause 86:5:4:[68.1,25.2,43.1]:TopTopTopTop: p27(x0),p10(f17(x0),x1),p29(x2,f19(x1)),p18(x2,x3) -> p29(x3,f20(f19(x0)))
% 19.91/4.53 === Conflict found: 68:3:2:[37.1,31.2,66.1]:TopTop: p18(f19(f17(x0)),x1),p27(x0) -> p18(x1,f20(f19(x0))) {x0 -> c34, x1 -> f19(c34)}
% 19.91/4.53 === Backtracking. Learning clause 87:3:2:[68.1,25.2]:TopTop: p27(x0),p10(f17(x0),x1) -> p18(f19(x1),f20(f19(x0)))
% 19.91/4.53 === Backtracking. Learning clause 88:4:4:[44.1,25.2]:TopTopTopTop: p28(x0,f19(x1)),p18(x0,x2),p10(x1,x3) -> p28(x2,f19(x3))
% 19.91/4.53 === Backtracking. Learning clause 89:6:5:[37.3,44.1,87.3]:TopTopTopTopTop: p18(f19(x0),x1),p28(x2,f20(f19(x3))),p18(x2,x4),p27(x3),p10(f17(x3),x0) -> p28(x4,x1)
% 19.91/4.53 === Backtracking. Learning clause 90:6:5:[37.3,43.3,87.3]:TopTopTopTopTop: p18(f19(x0),x1),p18(x2,x3),p29(f20(f19(x4)),x2),p27(x4),p10(f17(x4),x0) -> p29(x1,x3)
% 19.91/4.53 === Conflict found: 88:4:4:[44.1,25.2]:TopTopTopTop: p28(x0,f19(x1)),p18(x0,x2),p10(x1,x3) -> p28(x2,f19(x3)) {x0 -> f20(f19(c43)), x1 -> c34, x2 -> c34, x3 -> f17(c34)}
% 19.91/4.53 === Backtracking. Learning clause 91:5:4:[88.1,18.1,88.1]:TopTopTopTop: p18(f20(f19(c43)),x0),p10(c34,x1),p18(x0,x2),p10(x1,x3) -> p28(x2,f19(x3))
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c35, x1 -> f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31))))}
% 19.91/4.53 === Backtracking. Learning clause 92:2:0:[70.1,56.1]:: p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31))))) -> p23(c35)
% 19.91/4.53 === Backtracking. Learning clause 93:2:0:[20.2,55.1]:: p23(c33) -> p23(f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31)))))
% 19.91/4.53 === Backtracking. Learning clause 94:2:0:[21.2,55.1]:: p27(c33) -> p27(f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31)))))
% 19.91/4.53 === Backtracking. Learning clause 95:3:1:[21.2,81.2]:Top: p27(x0),p10(c37,x0) -> p27(f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Backtracking. Learning clause 96:2:0:[20.2,58.1]:: p23(c40) -> p23(f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c38, x1 -> f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f7(f7(f7(f7(f6(f7(f7(f7(f7(f7(f7(f7(c31))))))))))))))))))))))))))}
% 19.91/4.53 === Backtracking. Learning clause 97:2:0:[70.1,60.1]:: p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f7(f7(f7(f7(f6(f7(f7(f7(f7(f7(f7(f7(c31))))))))))))))))))))))))))) -> p23(c38)
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 222
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Conflict found: 68:3:2:[37.1,31.2,66.1]:TopTop: p18(f19(f17(x0)),x1),p27(x0) -> p18(x1,f20(f19(x0))) {x0 -> c34, x1 -> c34}
% 19.91/4.53 === Backtracking. Learning clause 98:3:2:[68.1,66.2]:TopTop: p27(x0),p18(x1,f19(f17(x0))) -> p18(x1,f20(f19(x0)))
% 19.91/4.53 === Conflict found: 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f15(f16(c43,c36)), x1 -> c44}
% 19.91/4.53 === Backtracking. Learning clause 99:2:1:[64.1,19.1,34.2]:Top: p3(c44,x0) -> p3(x0,f15(f16(c43,c36)))
% 19.91/4.53 === Backtracking. Learning clause 100:3:3:[37.2,26.2,66.2]:TopTopTop: p18(x0,x1),p18(x2,f20(x0)) -> p18(x2,f20(x1))
% 19.91/4.53 === Backtracking. Learning clause 101:2:1:[32.2,55.1]:Top: p10(c33,x0) -> p10(x0,f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31)))))
% 19.91/4.53 === Backtracking. Learning clause 102:2:0:[21.2,57.1]:: p27(c39) -> p27(f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31))))))))))))
% 19.91/4.53 === Backtracking. Learning clause 103:2:0:[21.2,58.1]:: p27(c40) -> p27(f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Backtracking. Learning clause 104:2:0:[21.2,61.1]:: p27(c36) -> p27(f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c34, x1 -> f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c31)))))))))))))))))))))))))))}
% 19.91/4.53 === Backtracking. Learning clause 105:2:0:[70.1,62.1]:: p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c31)))))))))))))))))))))))))))) -> p23(c34)
% 19.91/4.53 === Backtracking. Learning clause 107:1:0:[1.0,106.0,21.2,62.1]:: -> p27(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c31))))))))))))))))))))))))))))
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 229
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Conflict found: 73:7:5:[44.4,40.3,10.1,44.4]:TopTopTopTopTop: p18(x0,f19(x1)),p27(x2),p27(x1),p18(x3,x0),p28(x4,x3),p18(x4,f19(x2)) -> p25(x2,x1) {x0 -> c34, x1 -> f17(c34), x2 -> c34, x3 -> c34, x4 -> f19(c34)}
% 19.91/4.53 === Backtracking. Learning clause 108:6:4:[73.6,10.1]:TopTopTopTop: p18(x0,f19(x1)),p27(x2),p27(x1),p18(x3,x0),p28(f19(x2),x3) -> p25(x2,x1)
% 19.91/4.53 === Conflict found: 66:2:2:[37.2,10.1]:TopTop: p18(x0,x1) -> p18(x1,x0) {x0 -> f19(c34), x1 -> f20(c34)}
% 19.91/4.53 === Backtracking. Learning clause 109:3:3:[66.2,37.1]:TopTopTop: p18(x0,x1),p18(x1,x2) -> p18(x0,x2)
% 19.91/4.53 === Conflict found: 66:2:2:[37.2,10.1]:TopTop: p18(x0,x1) -> p18(x1,x0) {x0 -> c34, x1 -> f20(f19(c43))}
% 19.91/4.53 === Backtracking. Learning clause 110:5:4:[66.2,91.1]:TopTopTopTop: p18(x0,f20(f19(c43))),p10(c34,x1),p18(x0,x2),p10(x1,x3) -> p28(x2,f19(x3))
% 19.91/4.53 === Conflict found: 109:3:3:[66.2,37.1]:TopTopTop: p18(x0,x1),p18(x1,x2) -> p18(x0,x2) {x0 -> f20(f19(c43)), x1 -> f20(c34), x2 -> c34}
% 19.91/4.53 === Backtracking. Learning clause 111:6:5:[109.1,26.2,91.1]:TopTopTopTopTop: p18(f20(x0),x1),p18(f19(c43),x0),p10(c34,x2),p18(x1,x3),p10(x2,x4) -> p28(x3,f19(x4))
% 19.91/4.53 === Backtracking. Learning clause 112:2:2:[33.2,6.1]:TopTop: p9(x0,x1) -> p9(x1,x0)
% 19.91/4.53 === Backtracking. Learning clause 113:4:3:[43.3,31.2]:TopTopTop: p18(x0,x1),p29(f19(f17(x2)),x0),p27(x2) -> p29(f20(f19(x2)),x1)
% 19.91/4.53 === Backtracking. Learning clause 114:4:3:[44.3,31.2]:TopTopTop: p18(x0,x1),p28(f19(f17(x2)),x0),p27(x2) -> p28(f20(f19(x2)),x1)
% 19.91/4.53 === Backtracking. Learning clause 115:4:3:[44.1,31.2]:TopTopTop: p28(x0,f19(f17(x1))),p18(x0,x2),p27(x1) -> p28(x2,f20(f19(x1)))
% 19.91/4.53 === Backtracking. Learning clause 116:3:2:[34.1,74.2]:TopTop: p3(x0,x1),p3(c32,x0) -> p3(f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31))))))),x1)
% 19.91/4.53 === Backtracking. Learning clause 117:2:0:[20.2,57.1]:: p23(c39) -> p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31))))))))))))
% 19.91/4.53 === Backtracking. Learning clause 118:2:0:[20.2,61.1]:: p23(c36) -> p23(f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 246
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Backtracking. Learning clause 119:5:3:[44.2,49.4,66.2,10.1]:TopTopTop: p27(x0),p27(x1),p25(x1,x0),p18(x2,f19(x0)) -> p28(f19(x1),x2)
% 19.91/4.53 === Conflict found: 109:3:3:[66.2,37.1]:TopTopTop: p18(x0,x1),p18(x1,x2) -> p18(x0,x2) {x0 -> f19(f17(c43)), x1 -> f20(f19(c43)), x2 -> c34}
% 19.91/4.53 === Backtracking. Learning clause 120:3:2:[109.1,31.2,66.2,66.1]:TopTop: p27(x0),p18(x1,f20(f19(x0))) -> p18(x1,f19(f17(x0)))
% 19.91/4.53 === Backtracking. Learning clause 121:2:2:[38.2,11.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c37, x1 -> f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31))))))))))))))))))))))))))}
% 19.91/4.53 === Backtracking. Learning clause 122:2:0:[70.1,59.1]:: p23(f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31))))))))))))))))))))))))))) -> p23(c37)
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 248
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Conflict found: 110:5:4:[66.2,91.1]:TopTopTopTop: p18(x0,f20(f19(c43))),p10(c34,x1),p18(x0,x2),p10(x1,x3) -> p28(x2,f19(x3)) {x0 -> f19(c34), x1 -> c35, x2 -> f19(c34), x3 -> c34}
% 19.91/4.53 === Backtracking. Learning clause 124:7:4:[2.0,123.2,110.1,87.3,40.3,10.1,32.3]:TopTopTopTop: p10(c34,x0),p10(x0,x1),p27(x2),p27(x1),p10(x3,f17(c43)),p10(x3,x2) -> p25(x2,x1)
% 19.91/4.53 === Conflict found: 124:7:4:[2.0,123.2,110.1,87.3,40.3,10.1,32.3]:TopTopTopTop: p10(c34,x0),p10(x0,x1),p27(x2),p27(x1),p10(x3,f17(c43)),p10(x3,x2) -> p25(x2,x1) {x0 -> c34, x1 -> c34, x2 -> f17(c34), x3 -> f17(c34)}
% 19.91/4.53 === Backtracking. Learning clause 125:6:3:[124.5,24.2,5.1]:TopTopTop: p10(c34,x0),p10(x0,x1),p27(f17(x2)),p27(x1),p10(x2,c43) -> p25(f17(x2),x1)
% 19.91/4.53 === Conflict found: 84:5:4:[46.4,16.1,46.4,63.2]:TopTopTopTop: p10(x0,f17(c43)),p10(x1,x2),p25(x3,x1),p10(x3,x0),p10(c34,x2) -> {x0 -> f17(c34), x1 -> c34, x2 -> c43, x3 -> f17(c34)}
% 19.91/4.53 === Backtracking. Learning clause 126:7:4:[84.1,24.2,5.1,125.6]:TopTopTopTop: p10(x0,x1),p10(c34,x1),p10(c34,x3),p10(x3,x0),p27(f17(x2)),p27(x0),p10(x2,c43) ->
% 19.91/4.53 === Conflict found: 89:6:5:[37.3,44.1,87.3]:TopTopTopTopTop: p18(f19(x0),x1),p28(x2,f20(f19(x3))),p18(x2,x4),p27(x3),p10(f17(x3),x0) -> p28(x4,x1) {x0 -> f17(c34), x1 -> f19(f17(c34)), x2 -> f19(c34), x3 -> c34, x4 -> f19(c34)}
% 19.91/4.53 === Backtracking. Learning clause 127:5:4:[89.1,10.1]:TopTopTopTop: p28(x0,f20(f19(x1))),p18(x0,x2),p27(x1),p10(f17(x1),x3) -> p28(x2,f19(x3))
% 19.91/4.53 === Backtracking. Learning clause 128:4:3:[37.3,43.1,31.2,10.1]:TopTopTop: p29(x0,f20(f19(x1))),p18(x0,x2),p27(x1) -> p29(x2,f19(f17(x1)))
% 19.91/4.53 === Conflict found: 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31))))))), x1 -> c34}
% 19.91/4.53 === Backtracking. Learning clause 129:3:2:[64.1,116.3]:TopTop: p3(x0,x1),p3(c32,x0) -> p3(x1,f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31))))))))
% 19.91/4.53 === Backtracking. Learning clause 130:2:1:[32.2,56.1]:Top: p10(c35,x0) -> p10(x0,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31)))))
% 19.91/4.53 === Backtracking. Learning clause 131:2:1:[32.2,57.1]:Top: p10(c39,x0) -> p10(x0,f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31))))))))))))
% 19.91/4.53 === Conflict found: 70:3:2:[63.2,20.2]:TopTop: p10(x0,x1),p23(x1) -> p23(x0) {x0 -> c40, x1 -> f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31))))))))))))))))))))))))))}
% 19.91/4.53 === Backtracking. Learning clause 132:2:0:[70.1,58.1]:: p23(f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31))))))))))))))))))))))))))) -> p23(c40)
% 19.91/4.53 === Backtracking. Learning clause 133:2:1:[32.2,61.1]:Top: p10(c36,x0) -> p10(x0,f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31)))))))))))))))))))))))))))
% 19.91/4.53 === Clause set with instances from active satisfied. Growing active. New size: 265
% 19.91/4.53 === Restarting.
% 19.91/4.53 === Conflict found: 126:7:4:[84.1,24.2,5.1,125.6]:TopTopTopTop: p10(x0,x1),p10(c34,x1),p10(c34,x3),p10(x3,x0),p27(f17(x2)),p27(x0),p10(x2,c43) -> {x0 -> c34, x1 -> c45, x2 -> c43, x3 -> c34}
% 19.91/4.53 === Backtracking. Learning clause 134:6:3:[126.7,5.1]:TopTopTop: p10(x0,x1),p10(c34,x1),p10(c34,x2),p10(x2,x0),p27(f17(c43)),p27(x0) ->
% 19.91/4.53 === Conflict found: 134:6:3:[126.7,5.1]:TopTopTop: p10(x0,x1),p10(c34,x1),p10(c34,x2),p10(x2,x0),p27(f17(c43)),p27(x0) -> {x0 -> c34, x1 -> c34, x2 -> c34}
% 19.91/4.53
% 19.91/4.53 SZS status Unsatisfiable
% 19.91/4.53
% 19.91/4.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.91/4.53
% 19.91/4.53 SPASS-SCL-FOL Statistics:
% 19.91/4.53 Number of learned clauses: 69
% 19.91/4.53 Number of propagations: 4849
% 19.91/4.53 Number of decisions: 3963
% 19.91/4.53 Number of resolutions: 105
% 19.91/4.53 Number of condensations: 0
% 19.91/4.53 Number of sub resolutions: 3
% 19.91/4.53 Number of input literals (deduplicated): 60
% 19.91/4.53 Number of grows: 8
% 19.91/4.53 Number of considered ground atoms: 265
% 19.91/4.53
% 19.91/4.53 Needed: 0:00:03.91
% 19.91/4.53
%------------------------------------------------------------------------------