%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN709-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 : n028.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:11 PM UTC 2026
% Result : Unsatisfiable 9.04s 2.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN709-1 : TPTP v9.2.1. Released v2.5.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n028.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 13:47:16 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.19/0.39 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 9.04/2.71 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.04/2.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.04/2.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.04/2.71 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.04/2.71 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.04/2.71 Execution resolution_1 ended with status: unsatisfiable
% 9.04/2.71 Used heuristic: resolution_1
% 9.04/2.71
% 9.04/2.71 Input Clauses:
% 9.04/2.71
% 9.04/2.71 Predicates: p10 p9 p7 p6 p42 p40 p4 p38 p36 p35 p32 p30 p3 p29 p27 p26 p24 p22 p21 p2 p19 p18 p16 p15 p13 p11 p44 p46 p45 p47
% 9.04/2.71 Fol Constants: c48 c49 c50 c58 c56 c59 c60 c51 c52 c53 c54 c61 c57 c55 c64 c66 c62 c63 c65 c67 c68
% 9.04/2.71 Fol Functions: f23 f20 f8 f5 f17 f14 f12 f28 f34 f25 f33 f31 f41 f39 f43 f37
% 9.04/2.71 Problem Properties:
% 9.04/2.71 This is a full first-order problem without equality.
% 9.04/2.71
% 9.04/2.71 After reduction: Problem Properties:
% 9.04/2.71 This is a full first-order problem without equality.
% 9.04/2.71
% 9.04/2.71
% 9.04/2.71 Reduced Input Clauses:
% 9.04/2.71
% 9.04/2.71 Most General Atoms: p6(x1,x2) p4(x1,x2) p35(x1,x2) p30(x1,x2) p26(x1,x2) p22(x1,x2) p2(x1,x2) p18(x1,x2) p15(x1,x2) p13(x1,x2) p19(x2,x3) p47(x1,x3) p16(x2,x3) p44(x1,x3) p10(x2,x3) p45(x1,x3) p11(x2,x3) p46(x1,x3) p9(x2,x3) p3(x2,x3) p40(x2,x3) p38(x2,x3) p42(x2,x3) p29(x2,x3) p7(x2,x3) p32(x2,x3) p27(x2,x3) p21(x2,x3) p36(x2,x3) p24(x2,x3)
% 9.04/2.71
% 9.04/2.71 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 ===
% 9.04/2.71
% 9.04/2.71 === Backtracking. Learning clause 84:3:2:[61.2,27.1]:TopTop: p4(c48,x0),p16(c49,x1) -> p44(x0,x1)
% 9.04/2.71 === Backtracking. Learning clause 85:3:2:[63.2,29.1]:TopTop: p22(f23(c58,c56),x0),p11(f20(c59,c60),x1) -> p46(x0,x1)
% 9.04/2.71 === Backtracking. Learning clause 86:3:2:[62.2,31.1]:TopTop: p11(f12(f14(c54,f17(c61,c49)),c56),x0),p10(c57,x1) -> p45(x0,x1)
% 9.04/2.71 === Backtracking. Learning clause 87:3:4:[60.3,59.1]:TopTopTopTop: p30(x0,x1),p47(x0,f25(f28(c64,x2),f34(c66,x3))) -> p47(x1,f34(x2,x3))
% 9.04/2.71 === Backtracking. Learning clause 88:2:3:[53.2,59.1]:TopTopTop: p19(f25(f28(c64,x0),f34(c66,x1)),x2) -> p19(x2,f34(x0,x1))
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 118
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 89:2:2:[34.2,2.1]:TopTop: p9(x0,x1) -> p9(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 90:2:2:[40.2,8.1]:TopTop: p38(x0,x1) -> p38(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 91:2:2:[41.2,9.1]:TopTop: p36(x0,x1) -> p36(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 92:2:2:[58.2,26.1]:TopTop: p11(x0,x1) -> p11(x1,x0)
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 149
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 93:2:2:[39.2,7.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 9.04/2.71 === Conflict found: 85:3:2:[63.2,29.1]:TopTop: p22(f23(c58,c56),x0),p11(f20(c59,c60),x1) -> p46(x0,x1) {x0 -> f23(c58,c56), x1 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 94:2:1:[85.1,18.1]:Top: p11(f20(c59,c60),x0) -> p46(f23(c58,c56),x0)
% 9.04/2.71 === Backtracking. Learning clause 95:2:2:[53.2,21.1]:TopTop: p19(x0,x1) -> p19(x1,x0)
% 9.04/2.71 === Conflict found: 95:2:2:[53.2,21.1]:TopTop: p19(x0,x1) -> p19(x1,x0) {x0 -> c48, x1 -> f25(f28(c64,c48),f34(c66,c48))}
% 9.04/2.71 === Backtracking. Learning clause 96:2:3:[95.2,88.1]:TopTopTop: p19(x0,f25(f28(c64,x1),f34(c66,x2))) -> p19(x0,f34(x1,x2))
% 9.04/2.71 === Conflict found: 92:2:2:[58.2,26.1]:TopTop: p11(x0,x1) -> p11(x1,x0) {x0 -> c48, x1 -> f12(f14(c54,f17(c61,c49)),c56)}
% 9.04/2.71 === Backtracking. Learning clause 97:3:2:[92.2,86.1]:TopTop: p11(x0,f12(f14(c54,f17(c61,c49)),c56)),p10(c57,x1) -> p45(x0,x1)
% 9.04/2.71 === Backtracking. Learning clause 98:2:4:[53.2,82.1]:TopTopTopTop: p19(f25(f28(c64,x0),f37(f43(c67,x1),x2)),x3) -> p19(x3,f37(f43(c67,x1),f39(f41(c68,f28(c64,x0)),x2)))
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 159
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 99:2:2:[42.2,10.1]:TopTop: p35(x0,x1) -> p35(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 100:2:2:[49.2,17.1]:TopTop: p24(x0,x1) -> p24(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 101:5:4:[63.1,76.3,94.2]:TopTopTopTop: p11(x0,x1),p10(c56,x2),p21(c58,x3),p11(f20(c59,c60),x0) -> p46(f23(x3,x2),x1)
% 9.04/2.71 === Backtracking. Learning clause 102:5:6:[62.1,65.3]:TopTopTopTopTopTop: p45(f12(x0,x1),x2),p10(x2,x3),p10(x1,x4),p9(x0,x5) -> p45(f12(x5,x4),x3)
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 160
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 103:5:6:[63.1,76.3]:TopTopTopTopTopTop: p46(f23(x0,x1),x2),p11(x2,x3),p10(x1,x4),p21(x0,x5) -> p46(f23(x5,x4),x3)
% 9.04/2.71 === Conflict found: 86:3:2:[62.2,31.1]:TopTop: p11(f12(f14(c54,f17(c61,c49)),c56),x0),p10(c57,x1) -> p45(x0,x1) {x0 -> f12(f14(c54,f17(c61,c49)),c56), x1 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 104:2:1:[86.1,26.1]:Top: p10(c57,x0) -> p45(f12(f14(c54,f17(c61,c49)),c56),x0)
% 9.04/2.71 === Backtracking. Learning clause 105:4:4:[60.2,83.2]:TopTopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p19(f25(f28(c64,c65),x2),x3),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,x3)
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 175
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Conflict found: 95:2:2:[53.2,21.1]:TopTop: p19(x0,x1) -> p19(x1,x0) {x0 -> f25(f28(c64,c48),f34(c66,c48)), x1 -> f34(c48,c48)}
% 9.04/2.71 === Backtracking. Learning clause 106:2:3:[95.1,59.1,53.2]:TopTopTop: p19(f34(x0,x1),x2) -> p19(x2,f25(f28(c64,x0),f34(c66,x1)))
% 9.04/2.71 === Conflict found: 105:4:4:[60.2,83.2]:TopTopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p19(f25(f28(c64,c65),x2),x3),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,x3) {x0 -> c48, x1 -> f31(c48,c48), x2 -> c48, x3 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 107:5:5:[105.1,72.3]:TopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p47(f31(f33(c62,c63),x2),x0),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),x1)
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 199
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 108:2:2:[46.2,14.1]:TopTop: p29(x0,x1) -> p29(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 109:2:2:[50.2,18.1]:TopTop: p22(x0,x1) -> p22(x1,x0)
% 9.04/2.71 === Backtracking. Learning clause 110:5:6:[60.3,79.3]:TopTopTopTopTopTop: p30(x0,x1),p47(x0,f25(x2,x3)),p19(x3,x4),p24(x2,x5) -> p47(x1,f25(x5,x4))
% 9.04/2.71 === Backtracking. Learning clause 111:4:5:[53.2,79.3]:TopTopTopTopTop: p19(f25(x0,x1),x2),p19(x1,x3),p24(x0,x4) -> p19(x2,f25(x4,x3))
% 9.04/2.71 === Backtracking. Learning clause 112:4:5:[60.3,106.2]:TopTopTopTopTop: p30(x0,x1),p47(x0,x2),p19(f34(x3,x4),x2) -> p47(x1,f25(f28(c64,x3),f34(c66,x4)))
% 9.04/2.71 === Backtracking. Learning clause 113:3:2:[60.4,64.1]:TopTop: p30(x0,f31(f33(c62,c63),f34(c65,c56))),p47(x0,x1),p19(x1,f25(f28(c64,c65),c60)) ->
% 9.04/2.71 === Conflict found: 105:4:4:[60.2,83.2]:TopTopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p19(f25(f28(c64,c65),x2),x3),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,x3) {x0 -> c48, x1 -> f31(c48,c48), x2 -> f37(f43(c67,c48),c48), x3 -> f37(f43(c67,c48),f39(f41(c68,f28(c64,c65)),c48))}
% 9.04/2.71 === Backtracking. Learning clause 114:3:4:[105.2,82.1]:TopTopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p47(f31(f33(c62,c63),x0),f37(f43(c67,x2),x3)) -> p47(x1,f37(f43(c67,x2),f39(f41(c68,f28(c64,c65)),x3)))
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 232
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Conflict found: 92:2:2:[58.2,26.1]:TopTop: p11(x0,x1) -> p11(x1,x0) {x0 -> c48, x1 -> f20(c59,c60)}
% 9.04/2.71 === Backtracking. Learning clause 115:3:2:[92.2,85.2]:TopTop: p11(x0,f20(c59,c60)),p22(f23(c58,c56),x1) -> p46(x1,x0)
% 9.04/2.71 === Conflict found: 111:4:5:[53.2,79.3]:TopTopTopTopTop: p19(f25(x0,x1),x2),p19(x1,x3),p24(x0,x4) -> p19(x2,f25(x4,x3)) {x0 -> c48, x1 -> c48, x2 -> f25(f28(c64,c65),c48), x3 -> c48, x4 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 116:5:6:[111.4,53.2]:TopTopTopTopTopTop: p19(f25(x0,x1),x2),p19(x1,x3),p24(x0,x4),p19(x2,x5) -> p19(x5,f25(x4,x3))
% 9.04/2.71 === Conflict found: 102:5:6:[62.1,65.3]:TopTopTopTopTopTop: p45(f12(x0,x1),x2),p10(x2,x3),p10(x1,x4),p9(x0,x5) -> p45(f12(x5,x4),x3) {x0 -> c48, x1 -> c48, x2 -> c48, x3 -> c57, x4 -> c56, x5 -> f14(c54,f17(c55,c49))}
% 9.04/2.71 === Backtracking. Learning clause 117:4:3:[102.5,32.1]:TopTopTop: p45(f12(x0,x1),x2),p10(x2,c57),p10(x1,c56),p9(x0,f14(c54,f17(c55,c49))) ->
% 9.04/2.71 === Conflict found: 105:4:4:[60.2,83.2]:TopTopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p19(f25(f28(c64,c65),x2),x3),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,x3) {x0 -> c48, x1 -> c48, x2 -> c48, x3 -> f25(f28(c64,c65),c48)}
% 9.04/2.71 === Backtracking. Learning clause 118:3:3:[105.2,21.1]:TopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,f25(f28(c64,c65),x2))
% 9.04/2.71 === Conflict found: 107:5:5:[105.1,72.3]:TopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p47(f31(f33(c62,c63),x2),x0),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),x1) {x0 -> f37(f43(c67,c48),c48), x1 -> f37(f43(c67,c48),f39(f41(c68,f28(c64,c65)),c48)), x2 -> f34(c66,c48), x3 -> c48, x4 -> f33(c62,c63)}
% 9.04/2.71 === Backtracking. Learning clause 119:4:5:[107.1,82.1]:TopTopTopTopTop: p47(f31(f33(c62,c63),x0),f37(f43(c67,x1),x2)),p19(f25(f28(c64,c65),x0),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),f37(f43(c67,x1),f39(f41(c68,f28(c64,c65)),x2)))
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 250
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 120:2:2:[45.2,13.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 9.04/2.71 === Conflict found: 95:2:2:[53.2,21.1]:TopTop: p19(x0,x1) -> p19(x1,x0) {x0 -> c48, x1 -> f25(f28(c64,c65),c48)}
% 9.04/2.71 === Backtracking. Learning clause 121:4:5:[95.2,111.1]:TopTopTopTopTop: p19(x0,f25(x1,x2)),p19(x2,x3),p24(x1,x4) -> p19(x0,f25(x4,x3))
% 9.04/2.71 === Conflict found: 115:3:2:[92.2,85.2]:TopTop: p11(x0,f20(c59,c60)),p22(f23(c58,c56),x1) -> p46(x1,x0) {x0 -> f20(c48,c48), x1 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 122:6:5:[115.1,80.3,63.2,92.2]:TopTopTopTopTop: p22(f23(c58,c56),x0),p18(x1,c59),p19(x2,c60),p22(x0,x3),p11(x4,f20(x1,x2)) -> p46(x3,x4)
% 9.04/2.71 === Backtracking. Learning clause 123:5:6:[63.3,80.3]:TopTopTopTopTopTop: p22(x0,x1),p46(x0,f20(x2,x3)),p18(x2,x4),p19(x3,x5) -> p46(x1,f20(x4,x5))
% 9.04/2.71 === Backtracking. Learning clause 124:4:4:[44.3,118.1]:TopTopTopTop: p30(x0,f31(f33(c62,c63),f25(f28(c64,c65),x1))),p30(x0,x2),p47(f31(f33(c62,c63),x1),x3) -> p47(x2,f25(f28(c64,c65),x3))
% 9.04/2.71 === Backtracking. Learning clause 125:4:4:[58.3,58.1]:TopTopTopTop: p11(x0,x1),p11(x0,x2),p11(x1,x3) -> p11(x2,x3)
% 9.04/2.71 === Conflict found: 107:5:5:[105.1,72.3]:TopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p47(f31(f33(c62,c63),x2),x0),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),x1) {x0 -> c48, x1 -> f25(f28(c64,c65),c60), x2 -> c48, x3 -> f34(c65,c56), x4 -> f33(c62,c63)}
% 9.04/2.71 === Backtracking. Learning clause 126:7:5:[107.5,64.1,116.5]:TopTopTopTopTop: p47(f31(f33(c62,c63),x0),x1),p19(f25(f28(c64,c65),x0),f34(c65,c56)),p29(f33(c62,c63),f33(c62,c63)),p19(f25(x2,x3),x4),p19(x3,c60),p24(x2,f28(c64,c65)),p19(x4,f25(f28(c64,c65),x1)) ->
% 9.04/2.71 === Conflict found: 118:3:3:[105.2,21.1]:TopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),x0)),x1),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,f25(f28(c64,c65),x2)) {x0 -> f25(f28(c64,c65),c48), x1 -> c48, x2 -> f25(f28(c64,c65),c48)}
% 9.04/2.71 === Backtracking. Learning clause 127:3:3:[118.2,83.2]:TopTopTop: p30(f31(f33(c62,c63),f25(f28(c64,c65),f25(f28(c64,c65),x0))),x1),p47(f31(f33(c62,c63),x0),x2) -> p47(x1,f25(f28(c64,c65),f25(f28(c64,c65),x2)))
% 9.04/2.71 === Conflict found: 107:5:5:[105.1,72.3]:TopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p47(f31(f33(c62,c63),x2),x0),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),x1) {x0 -> f25(f28(c64,c65),c48), x1 -> c48, x2 -> f25(f28(c64,c65),c48), x3 -> c48, x4 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 128:5:5:[107.2,83.2]:TopTopTopTopTop: p19(f25(f28(c64,c65),f25(f28(c64,c65),x0)),x1),p19(f25(f28(c64,c65),f25(f28(c64,c65),x2)),x3),p29(f33(c62,c63),x4),p47(f31(f33(c62,c63),x2),x0) -> p47(f31(x4,x3),x1)
% 9.04/2.71 === Clause set with instances from active satisfied. Growing active. New size: 289
% 9.04/2.71 === Restarting.
% 9.04/2.71 === Backtracking. Learning clause 129:2:2:[44.2,12.1]:TopTop: p30(x0,x1) -> p30(x1,x0)
% 9.04/2.71 === Conflict found: 115:3:2:[92.2,85.2]:TopTop: p11(x0,f20(c59,c60)),p22(f23(c58,c56),x1) -> p46(x1,x0) {x0 -> f20(c59,c60), x1 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 130:2:1:[115.1,26.1]:Top: p22(f23(c58,c56),x0) -> p46(x0,f20(c59,c60))
% 9.04/2.71 === Conflict found: 113:3:2:[60.4,64.1]:TopTop: p30(x0,f31(f33(c62,c63),f34(c65,c56))),p47(x0,x1),p19(x1,f25(f28(c64,c65),c60)) -> {x0 -> f31(c48,c48), x1 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 131:4:3:[113.1,72.3]:TopTopTop: p47(f31(x0,x1),x2),p19(x2,f25(f28(c64,c65),c60)),p19(x1,f34(c65,c56)),p29(x0,f33(c62,c63)) ->
% 9.04/2.71 === Conflict found: 121:4:5:[95.2,111.1]:TopTopTopTopTop: p19(x0,f25(x1,x2)),p19(x2,x3),p24(x1,x4) -> p19(x0,f25(x4,x3)) {x0 -> f34(c48,c48), x1 -> f28(c64,c48), x2 -> f34(c66,c48), x3 -> c48, x4 -> f28(c64,c65)}
% 9.04/2.71 === Backtracking. Learning clause 132:7:9:[121.1,106.2,121.1,121.2,21.1]:TopTopTopTopTopTopTopTopTop: p19(f34(c66,x0),x1),p24(f28(c64,x2),x3),p19(x1,x4),p24(x3,x5),p19(x6,f25(x7,f34(x2,x0))),p24(x7,x8) -> p19(x6,f25(x8,f25(x5,x4)))
% 9.04/2.71 === Conflict found: 121:4:5:[95.2,111.1]:TopTopTopTopTop: p19(x0,f25(x1,x2)),p19(x2,x3),p24(x1,x4) -> p19(x0,f25(x4,x3)) {x0 -> f34(c48,c48), x1 -> f28(c64,c48), x2 -> f34(c66,c48), x3 -> c48, x4 -> f28(c64,c65)}
% 9.04/2.71 === Backtracking. Learning clause 133:6:7:[121.1,106.2,121.1]:TopTopTopTopTopTopTop: p19(f34(c66,x0),x1),p24(f28(c64,x2),x3),p19(f34(x2,x0),x4),p19(x1,x5),p24(x3,x6) -> p19(x4,f25(x6,x5))
% 9.04/2.71 === Conflict found: 107:5:5:[105.1,72.3]:TopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p47(f31(f33(c62,c63),x2),x0),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),x1) {x0 -> f25(c48,c48), x1 -> c48, x2 -> f34(c66,c48), x3 -> f34(c65,c48), x4 -> c48}
% 9.04/2.71 === Backtracking. Learning clause 134:4:4:[107.2,81.2,59.1]:TopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p29(f33(c62,c63),x2),p46(f23(c58,x3),f20(c59,x0)) -> p47(f31(x2,f34(c65,x3)),x1)
% 9.04/2.71 === Conflict found: 107:5:5:[105.1,72.3]:TopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p47(f31(f33(c62,c63),x2),x0),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4) -> p47(f31(x4,x3),x1) {x0 -> c48, x1 -> f25(f28(c64,c65),c48), x2 -> f25(f28(c64,c65),c48), x3 -> c48, x4 -> f33(c62,c63)}
% 9.04/2.71 === Backtracking. Learning clause 135:8:7:[107.2,107.5]:TopTopTopTopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p19(f25(f28(c64,c65),x2),x3),p29(f33(c62,c63),x4),p19(f25(f28(c64,c65),x5),x0),p47(f31(f33(c62,c63),x6),x5),p19(f25(f28(c64,c65),x6),x2),p29(f33(c62,c63),f33(c62,c63)) -> p47(f31(x4,x3),x1)
% 9.04/2.71 === Conflict found: 134:4:4:[107.2,81.2,59.1]:TopTopTopTop: p19(f25(f28(c64,c65),x0),x1),p29(f33(c62,c63),x2),p46(f23(c58,x3),f20(c59,x0)) -> p47(f31(x2,f34(c65,x3)),x1) {x0 -> c60, x1 -> f25(f28(c64,c65),c60), x2 -> f33(c62,c63), x3 -> c56}
% 9.04/2.71
% 9.04/2.71 SZS status Unsatisfiable
% 9.04/2.71
% 9.04/2.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.04/2.71
% 9.04/2.71 SPASS-SCL-FOL Statistics:
% 9.04/2.71 Number of learned clauses: 52
% 9.04/2.71 Number of propagations: 3001
% 9.04/2.71 Number of decisions: 1874
% 9.04/2.71 Number of resolutions: 66
% 9.04/2.71 Number of condensations: 0
% 9.04/2.71 Number of sub resolutions: 0
% 9.04/2.71 Number of input literals (deduplicated): 85
% 9.04/2.71 Number of grows: 9
% 9.04/2.71 Number of considered ground atoms: 289
% 9.04/2.71
% 9.04/2.71 Needed: 0:00:02.17
% 9.04/2.71
%------------------------------------------------------------------------------