%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN689-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 : n011.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 16.52s 4.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SYN689-1 : TPTP v9.2.1. Released v2.5.0.
% 0.09/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.36 % Computer : n011.cluster.edu
% 0.17/0.36 % Model : x86_64 x86_64
% 0.17/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.36 % Memory : 8042.1875MB
% 0.17/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.36 % CPULimit : 300
% 0.17/0.36 % WCLimit : 300
% 0.17/0.36 % DateTime : Thu May 7 13:47:03 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 SPASS-SCL-FOL version:
% 0.27/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 16.52/4.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.52/4.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.52/4.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.52/4.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.52/4.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.52/4.62 Execution resolution_3 ended with status: unsatisfiable
% 16.52/4.62 Used heuristic: resolution_3
% 16.52/4.62
% 16.52/4.62 Input Clauses:
% 16.52/4.62
% 16.52/4.62 Predicates: p27 p23 p10 p9 p3 p21 p2 p18 p12 p22 p24 p26 p25 p28 p29
% 16.52/4.62 Fol Constants: c34 c43 c35 c41 c42 c46 c45 c36 c44 c30 c31 c32 c33 c39 c40 c37 c38
% 16.52/4.62 Fol Functions: f17 f19 f20 f16 f15 f4 f11 f5 f6 f7 f13 f14 f8
% 16.52/4.62 Problem Properties:
% 16.52/4.62 This is a full first-order problem without equality.
% 16.52/4.62
% 16.52/4.62 After reduction: Problem Properties:
% 16.52/4.62 This is a full first-order problem without equality.
% 16.52/4.62
% 16.52/4.62
% 16.52/4.62 Reduced Input Clauses:
% 16.52/4.62
% 16.52/4.62 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) p25(x1,x0) p26(x1,x0) p2(x2,x3)
% 16.52/4.62
% 16.52/4.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_3 ===
% 16.52/4.62
% 16.52/4.62 === Backtracking. Learning clause 63:2:2:[32.2,5.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 65:2:2:[36.2,9.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 66:2:2:[37.2,10.1]:TopTop: p18(x0,x1) -> p18(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 67:2:1:[34.2,19.1]:Top: p3(f15(f16(c43,c36)),x0) -> p3(x0,c44)
% 16.52/4.62 === 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)))
% 16.52/4.62 === 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)))))))))
% 16.52/4.62 === Clause set with instances from active satisfied. Growing active. New size: 116
% 16.52/4.62 === Restarting.
% 16.52/4.62 === Backtracking. Learning clause 70:3:2:[42.2,12.1]:TopTop: p21(c42,x0),p21(c41,x1) -> p22(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 71:3:2:[47.4,13.1]:TopTop: p10(x0,c46),p24(x1,x0),p10(x1,c43) ->
% 16.52/4.62 === Backtracking. Learning clause 72:3:2:[44.2,18.1]:TopTop: p18(f19(c35),x0),p18(f20(f19(c43)),x1) -> p28(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 73:2:2:[33.2,6.1]:TopTop: p9(x0,x1) -> p9(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 74:4:3:[43.3,31.2]:TopTopTop: p18(x0,x1),p29(f19(f17(x2)),x0),p27(x2) -> p29(f20(f19(x2)),x1)
% 16.52/4.62 === Backtracking. Learning clause 75:4:3:[43.1,31.2]:TopTopTop: p29(x0,f19(f17(x1))),p18(x0,x2),p27(x1) -> p29(x2,f20(f19(x1)))
% 16.52/4.62 === Backtracking. Learning clause 76:4:3:[44.3,31.2]:TopTopTop: p18(x0,x1),p28(f19(f17(x2)),x0),p27(x2) -> p28(f20(f19(x2)),x1)
% 16.52/4.62 === Backtracking. Learning clause 77:4:3:[44.1,31.2]:TopTopTop: p28(x0,f19(f17(x1))),p18(x0,x2),p27(x1) -> p28(x2,f20(f19(x1)))
% 16.52/4.62 === Clause set with instances from active satisfied. Growing active. New size: 184
% 16.52/4.62 === Restarting.
% 16.52/4.62 === Conflict found: 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> c34, x1 -> f15(f16(c43,c36))}
% 16.52/4.62 === Backtracking. Learning clause 78:2:1:[64.2,67.1]:Top: p3(x0,f15(f16(c43,c36))) -> p3(x0,c44)
% 16.52/4.62 === Conflict found: 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f15(f16(c43,c36)), x1 -> c44}
% 16.52/4.62 === Backtracking. Learning clause 79:1:0:[64.1,19.1]:: -> p3(c44,f15(f16(c43,c36)))
% 16.52/4.62 === Backtracking. Learning clause 80:2:1:[30.2,67.1]:Top: p10(f16(c43,c36),x0) -> p3(f15(x0),c44)
% 16.52/4.62 === Backtracking. Learning clause 81:2:2:[38.2,11.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 16.52/4.62 === Backtracking. Learning clause 82:2:1:[34.2,54.1]:Top: p3(c32,x0) -> p3(x0,f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31))))))))
% 16.52/4.62 === Backtracking. Learning clause 83:3:1:[32.2,56.1,21.2]:Top: p10(c35,x0),p27(x0) -> p27(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31)))))
% 16.52/4.62 === Backtracking. Learning clause 84:3:1:[32.2,56.1,20.2]:Top: p10(c35,x0),p23(x0) -> p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31)))))
% 16.52/4.62 === Backtracking. Learning clause 85: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)))))
% 16.52/4.62 === Backtracking. Learning clause 86:3:1:[32.2,55.1,21.2]:Top: p10(c33,x0),p27(x0) -> p27(f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31)))))
% 16.52/4.62 === Backtracking. Learning clause 87:3:1:[32.2,55.1,20.2]:Top: p10(c33,x0),p23(x0) -> p23(f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31)))))
% 16.52/4.62 === Backtracking. Learning clause 88: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)))))
% 16.52/4.62 === Backtracking. Learning clause 89:3:1:[32.2,57.1,21.2]:Top: p10(c39,x0),p27(x0) -> p27(f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 90:3:1:[32.2,57.1,20.2]:Top: p10(c39,x0),p23(x0) -> p23(f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 91: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))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 92: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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 93:3:1:[32.2,58.1,20.2]:Top: p10(c40,x0),p23(x0) -> 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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 94:2:1:[32.2,58.1]:Top: p10(c40,x0) -> p10(x0,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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 95:3:1:[32.2,59.1,21.2]:Top: p10(c37,x0),p27(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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 96: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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 97: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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 98:3:1:[32.2,60.1,21.2]:Top: p10(c38,x0),p27(x0) -> p27(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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 99:3:1:[32.2,60.1,20.2]:Top: p10(c38,x0),p23(x0) -> 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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 100:2:1:[32.2,60.1]:Top: p10(c38,x0) -> p10(x0,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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 101:3:1:[32.2,61.1,21.2]:Top: p10(c36,x0),p27(x0) -> 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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 102:3:1:[32.2,61.1,20.2]:Top: p10(c36,x0),p23(x0) -> 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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 103: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)))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 104: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))))))))))))))))))))))))))))
% 16.52/4.62 === Backtracking. Learning clause 106:1:0:[1.0,105.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))))))))))))))))))))))))))))
% 16.52/4.62 === Clause set with instances from active satisfied. Growing active. New size: 258
% 16.52/4.62 === Restarting.
% 16.52/4.62 === Conflict found: 63:2:2:[32.2,5.1]:TopTop: p10(x0,x1) -> p10(x1,x0) {x0 -> c34, x1 -> f16(c43,c36)}
% 16.52/4.62 === Backtracking. Learning clause 107:2:1:[63.2,80.1]:Top: p10(x0,f16(c43,c36)) -> p3(f15(x0),c44)
% 16.52/4.62 === 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}
% 16.52/4.62 === Backtracking. Learning clause 108:3:2:[68.1,66.2]:TopTop: p27(x0),p18(x1,f19(f17(x0))) -> p18(x1,f20(f19(x0)))
% 16.52/4.62 === Conflict found: 66:2:2:[37.2,10.1]:TopTop: p18(x0,x1) -> p18(x1,x0) {x0 -> c34, x1 -> f20(f19(c43))}
% 16.52/4.62 === Backtracking. Learning clause 109:3:2:[66.2,72.2]:TopTop: p18(x0,f20(f19(c43))),p18(f19(c35),x1) -> p28(x0,x1)
% 16.52/4.62 === Conflict found: 80:2:1:[30.2,67.1]:Top: p10(f16(c43,c36),x0) -> p3(f15(x0),c44) {x0 -> f16(c34,c34)}
% 16.52/4.62 === Backtracking. Learning clause 110:3:2:[80.1,51.3]:TopTop: p10(c43,x0),p10(c36,x1) -> p3(f15(f16(x0,x1)),c44)
% 16.52/4.62 === Backtracking. Learning clause 111:2:1:[44.3,10.1,18.1]:Top: p18(f19(c35),x0) -> p28(f20(f19(c43)),x0)
% 16.52/4.62 === Clause set with instances from active satisfied. Growing active. New size: 316
% 16.52/4.62 === Restarting.
% 16.52/4.62 === Conflict found: 108:3:2:[68.1,66.2]:TopTop: p27(x0),p18(x1,f19(f17(x0))) -> p18(x1,f20(f19(x0))) {x0 -> c43, x1 -> c34}
% 16.52/4.62 === Backtracking. Learning clause 113:3:2:[2.0,112.0,108.3,109.1]:TopTop: p18(x0,f19(f17(c43))),p18(f19(c35),x1) -> p28(x0,x1)
% 16.52/4.62 === Backtracking. Learning clause 114:3:3:[37.2,25.2]:TopTopTop: p18(f19(x0),x1),p10(x0,x2) -> p18(x1,f19(x2))
% 16.52/4.62 === Backtracking. Learning clause 115:4:4:[37.3,114.1]:TopTopTopTop: p18(x0,f19(x1)),p18(x0,x2),p10(x1,x3) -> p18(x2,f19(x3))
% 16.52/4.62 === Conflict found: 109:3:2:[66.2,72.2]:TopTop: p18(x0,f20(f19(c43))),p18(f19(c35),x1) -> p28(x0,x1) {x0 -> c34, x1 -> f19(c35)}
% 16.52/4.62 === Backtracking. Learning clause 117:2:1:[2.0,116.0,109.2,10.1,108.3]:Top: p18(x0,f19(f17(c43))) -> p28(x0,f19(c35))
% 16.52/4.62 === Conflict found: 109:3:2:[66.2,72.2]:TopTop: p18(x0,f20(f19(c43))),p18(f19(c35),x1) -> p28(x0,x1) {x0 -> c34, x1 -> f19(c35)}
% 16.52/4.62 === Backtracking. Learning clause 118:2:1:[109.2,10.1]:Top: p18(x0,f20(f19(c43))) -> p28(x0,f19(c35))
% 16.52/4.62 === Backtracking. Learning clause 119:4:3:[34.1,110.3]:TopTopTop: p3(f15(f16(x0,x1)),x2),p10(c43,x0),p10(c36,x1) -> p3(c44,x2)
% 16.52/4.62 === Conflict found: 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f15(f16(c34,c34)), x1 -> c44}
% 16.52/4.62 === Backtracking. Learning clause 120:3:2:[64.1,110.3]:TopTop: p10(c43,x0),p10(c36,x1) -> p3(c44,f15(f16(x0,x1)))
% 16.52/4.62 === Conflict found: 108:3:2:[68.1,66.2]:TopTop: p27(x0),p18(x1,f19(f17(x0))) -> p18(x1,f20(f19(x0))) {x0 -> c34, x1 -> f19(c35)}
% 16.52/4.62 === Backtracking. Learning clause 121:4:3:[108.3,37.2]:TopTopTop: p27(x0),p18(x1,f19(f17(x0))),p18(x1,x2) -> p18(x2,f20(f19(x0)))
% 16.52/4.62 === Clause set with instances from active satisfied. Growing active. New size: 341
% 16.52/4.62 === Restarting.
% 16.52/4.62 === Backtracking. Learning clause 122:4:4:[44.1,25.2]:TopTopTopTop: p28(x0,f19(x1)),p18(x0,x2),p10(x1,x3) -> p28(x2,f19(x3))
% 16.52/4.62 === Conflict found: 64:2:2:[34.2,7.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> c34, x1 -> f15(f16(c34,c34))}
% 16.52/4.62 === Backtracking. Learning clause 123:4:3:[64.2,119.1]:TopTopTop: p3(x0,f15(f16(x1,x2))),p10(c43,x1),p10(c36,x2) -> p3(c44,x0)
% 16.52/4.62 === Conflict found: 117:2:1:[2.0,116.0,109.2,10.1,108.3]:Top: p18(x0,f19(f17(c43))) -> p28(x0,f19(c35)) {x0 -> f19(c34)}
% 16.52/4.62 === Backtracking. Learning clause 124:5:2:[117.1,25.2,122.1,41.3,10.1]:TopTop: p10(x0,f17(c43)),p10(c35,x1),p27(x0),p27(x1) -> p26(x0,x1)
% 16.52/4.62 === Clause set with instances from active satisfied. Growing active. New size: 349
% 16.52/4.62 === Restarting.
% 16.52/4.62 === Backtracking. Learning clause 125:4:4:[45.3,24.2]:TopTopTopTop: p10(x0,x1),p26(f17(x2),x0),p10(x2,x3) -> p26(f17(x3),x1)
% 16.52/4.62 === Conflict found: 125:4:4:[45.3,24.2]:TopTopTopTop: p10(x0,x1),p26(f17(x2),x0),p10(x2,x3) -> p26(f17(x3),x1) {x0 -> c34, x1 -> c35, x2 -> c43, x3 -> c43}
% 16.52/4.62 === Backtracking. Learning clause 126:5:4:[125.4,15.1,125.4]:TopTopTopTop: p10(x0,c35),p10(x1,c43),p10(x2,x0),p26(f17(x3),x2),p10(x3,x1) ->
% 16.52/4.62 === Conflict found: 124:5:2:[117.1,25.2,122.1,41.3,10.1]:TopTop: p10(x0,f17(c43)),p10(c35,x1),p27(x0),p27(x1) -> p26(x0,x1) {x0 -> f17(c34), x1 -> c34}
% 16.52/4.62 === Backtracking. Learning clause 127:9:5:[124.1,24.2,126.4,32.3]:TopTopTopTopTop: p27(f17(x0)),p27(x1),p10(x0,c43),p10(x2,c35),p10(x3,c43),p10(x1,x2),p10(x0,x3),p10(x4,c35),p10(x4,x1) ->
% 16.52/4.62 === Conflict found: 127:9:5:[124.1,24.2,126.4,32.3]:TopTopTopTopTop: p27(f17(x0)),p27(x1),p10(x0,c43),p10(x2,c35),p10(x3,c43),p10(x1,x2),p10(x0,x3),p10(x4,c35),p10(x4,x1) -> {x0 -> c43, x1 -> c35, x2 -> c35, x3 -> c34, x4 -> c35}
% 16.52/4.62 === Backtracking. Learning clause 130:3:2:[3.0,128.1,32.2,129.2,127.4,5.1,5.1,32.3]:TopTop: p27(f17(c43)),p10(x0,c43),p10(x0,x1) ->
% 16.52/4.62 === Conflict found: 130:3:2:[3.0,128.1,32.2,129.2,127.4,5.1,5.1,32.3]:TopTop: p27(f17(c43)),p10(x0,c43),p10(x0,x1) -> {x0 -> c43, x1 -> c43}
% 16.52/4.62
% 16.52/4.62 SZS status Unsatisfiable
% 16.52/4.62
% 16.52/4.62 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.52/4.62
% 16.52/4.62 SPASS-SCL-FOL Statistics:
% 16.52/4.62 Number of learned clauses: 63
% 16.52/4.62 Number of propagations: 3968
% 16.52/4.62 Number of decisions: 3090
% 16.52/4.62 Number of resolutions: 91
% 16.52/4.62 Number of condensations: 0
% 16.52/4.62 Number of sub resolutions: 5
% 16.52/4.62 Number of input literals (deduplicated): 60
% 16.52/4.62 Number of grows: 6
% 16.52/4.62 Number of considered ground atoms: 349
% 16.52/4.62
% 16.52/4.62 Needed: 0:00:04.03
% 16.52/4.62
%------------------------------------------------------------------------------