%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN693-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 : n023.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:10 PM UTC 2026
% Result : Unsatisfiable 38.46s 8.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN693-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n023.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:48:09 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 38.46/8.28 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.46/8.28 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.46/8.28 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.46/8.28 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.46/8.28 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.46/8.28 Execution resolution_3 ended with status: unsatisfiable
% 38.46/8.28 Used heuristic: resolution_3
% 38.46/8.28
% 38.46/8.28 Input Clauses:
% 38.46/8.28
% 38.46/8.28 Predicates: p25 p29 p30 p28 p10 p7 p6 p3 p21 p2 p17 p14 p12 p31 p32 p26 p33 p27
% 38.46/8.28 Fol Constants: c34 c36 c41 c38 c39 c40 c44 c46 c42 c35 c45 c43 c37
% 38.46/8.28 Fol Functions: f18 f16 f5 f8 f22 f20 f9 f23 f4 f24 f11 f13 f19 f15
% 38.46/8.28 Problem Properties:
% 38.46/8.28 This is a full first-order problem without equality.
% 38.46/8.28
% 38.46/8.28 After reduction: Problem Properties:
% 38.46/8.28 This is a full first-order problem without equality.
% 38.46/8.28
% 38.46/8.28
% 38.46/8.28 Reduced Input Clauses:
% 38.46/8.28
% 38.46/8.28 Most General Atoms: p25(x1) p30(x1) p29(x1) p28(x1) p6(x1,x2) p17(x1,x2) p14(x1,x2) p33(x3,x1) p12(x2,x3) p27(x1,x3) p31(x3,x1) p10(x2,x3) p32(x1,x3) p3(x2,x3) p7(x2,x3) p21(x4,x5) p26(x5,x3,x1) p2(x1,x5)
% 38.46/8.28
% 38.46/8.28 === Starting SPASS-SCL-FOL A Little Less Naive, considering 61 atoms initially, heuristics mode: resolution_3 ===
% 38.46/8.28
% 38.46/8.28 === Backtracking. Learning clause 70:2:1:[40.2,16.1]:Top: p2(c44,x0) -> p2(x0,c46)
% 38.46/8.28 === Backtracking. Learning clause 71:2:1:[36.2,19.1]:Top: p7(f8(c35),x0) -> p7(x0,c36)
% 38.46/8.28 === Backtracking. Learning clause 72:2:2:[36.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 73:2:2:[38.2,10.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 75:2:2:[41.2,13.1]:TopTop: p17(x0,x1) -> p17(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 76:2:2:[42.2,14.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 77:3:2:[47.2,44.1]:TopTop: p2(f11(f4(c42),c45),x0),p2(f11(f4(f5(c42)),c45),x1) -> p33(x1,x0)
% 38.46/8.28 === Clause set with instances from active satisfied. Growing active. New size: 126
% 38.46/8.28 === Restarting.
% 38.46/8.28 === Backtracking. Learning clause 78:3:2:[50.2,20.1]:TopTop: p17(f22(c34,c45),x0),p10(c43,x1) -> p32(x0,x1)
% 38.46/8.28 === Backtracking. Learning clause 79:2:2:[43.2,15.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 80:2:1:[40.3,53.1]:Top: p2(x0,f11(f4(c46),c43)),p2(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)) ->
% 38.46/8.28 === Backtracking. Learning clause 81:2:1:[40.1,51.1,74.1]:Top: p2(f11(f4(c42),c45),x0) -> p2(x0,f11(f4(f23(c42,f9(f20(c37)))),c45))
% 38.46/8.28 === Backtracking. Learning clause 82:3:2:[47.3,52.1]:TopTop: p2(x0,x1),p33(f11(f4(f23(c44,f9(f20(c37)))),c43),x0) -> p33(f11(f4(c44),c43),x1)
% 38.46/8.28 === Backtracking. Learning clause 83:3:2:[47.1,52.1]:TopTop: p33(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)),p2(x0,x1) -> p33(x1,f11(f4(c44),c43))
% 38.46/8.28 === Backtracking. Learning clause 84:3:2:[49.3,52.1]:TopTop: p2(x0,x1),p31(f11(f4(f23(c44,f9(f20(c37)))),c43),x0) -> p31(f11(f4(c44),c43),x1)
% 38.46/8.28 === Backtracking. Learning clause 85:3:2:[49.1,52.1]:TopTop: p31(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)),p2(x0,x1) -> p31(x1,f11(f4(c44),c43))
% 38.46/8.28 === Clause set with instances from active satisfied. Growing active. New size: 190
% 38.46/8.28 === Restarting.
% 38.46/8.28 === Backtracking. Learning clause 86:2:2:[35.2,7.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 38.46/8.28 === Conflict found: 70:2:1:[40.2,16.1]:Top: p2(c44,x0) -> p2(x0,c46) {x0 -> c34}
% 38.46/8.28 === Backtracking. Learning clause 87:2:1:[70.1,74.2]:Top: p2(x0,c44) -> p2(x0,c46)
% 38.46/8.28 === Backtracking. Learning clause 88:3:2:[49.2,18.1]:TopTop: p2(f5(c42),x0),p2(c44,x1) -> p31(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 89:3:2:[49.2,21.1]:TopTop: p2(c46,x0),p2(f23(c44,f9(f20(c37))),x1) -> p31(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 90:2:0:[58.3,53.1]:: p10(c43,c43),p3(f4(c46),f4(f23(c44,f9(f20(c37))))) ->
% 38.46/8.28 === Backtracking. Learning clause 91:2:1:[40.2,61.1]:Top: p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0) -> p2(x0,f11(f4(c42),c43))
% 38.46/8.28 === Backtracking. Learning clause 92:3:2:[47.1,61.1]:TopTop: p33(x0,f19(f11(f4(f5(c42)),c43),f9(f20(c37)))),p2(x0,x1) -> p33(x1,f11(f4(c42),c43))
% 38.46/8.28 === Backtracking. Learning clause 93:3:2:[49.1,61.1]:TopTop: p31(x0,f19(f11(f4(f5(c42)),c43),f9(f20(c37)))),p2(x0,x1) -> p31(x1,f11(f4(c42),c43))
% 38.46/8.28 === Backtracking. Learning clause 94:3:2:[49.3,61.1]:TopTop: p2(x0,x1),p31(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0) -> p31(f11(f4(c42),c43),x1)
% 38.46/8.28 === Backtracking. Learning clause 95:3:2:[47.3,61.1]:TopTop: p2(x0,x1),p33(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0) -> p33(f11(f4(c42),c43),x1)
% 38.46/8.28 === Clause set with instances from active satisfied. Growing active. New size: 257
% 38.46/8.28 === Restarting.
% 38.46/8.28 === Conflict found: 72:2:2:[36.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c34, x1 -> f8(c35)}
% 38.46/8.28 === Backtracking. Learning clause 96:2:1:[72.2,71.1]:Top: p7(x0,f8(c35)) -> p7(x0,c36)
% 38.46/8.28 === Conflict found: 72:2:2:[36.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c35), x1 -> c36}
% 38.46/8.28 === Backtracking. Learning clause 97:1:0:[72.1,19.1]:: -> p7(c36,f8(c35))
% 38.46/8.28 === Conflict found: 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c34, x1 -> f5(c42)}
% 38.46/8.28 === Backtracking. Learning clause 98:3:2:[74.2,88.1]:TopTop: p2(x0,f5(c42)),p2(c44,x1) -> p31(x1,x0)
% 38.46/8.28 === Backtracking. Learning clause 99:2:1:[36.1,27.2,19.1]:Top: p6(c35,x0) -> p7(f8(x0),c36)
% 38.46/8.28 === Conflict found: 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c34, x1 -> f23(c44,f9(f20(c37)))}
% 38.46/8.28 === Backtracking. Learning clause 100:3:2:[74.2,89.2]:TopTop: p2(x0,f23(c44,f9(f20(c37)))),p2(c46,x1) -> p31(x0,x1)
% 38.46/8.28 === Backtracking. Learning clause 101:5:4:[40.3,77.2,40.3]:TopTopTopTop: p2(x0,x1),p2(f11(f4(c42),c45),x2),p2(x3,x0),p2(x3,f11(f4(f5(c42)),c45)) -> p33(x1,x2)
% 38.46/8.28 === Conflict found: 78:3:2:[50.2,20.1]:TopTop: p17(f22(c34,c45),x0),p10(c43,x1) -> p32(x0,x1) {x0 -> f22(c34,c34), x1 -> c43}
% 38.46/8.28 === Backtracking. Learning clause 102:4:3:[78.1,59.3]:TopTopTop: p10(c43,x0),p10(c45,x1),p21(c34,x2) -> p32(f22(x2,x1),x0)
% 38.46/8.28 === Backtracking. Learning clause 103:4:5:[41.1,59.3,75.2,75.1]:TopTopTopTopTop: p10(x0,x1),p21(x2,x3),p17(x4,f22(x2,x0)) -> p17(x4,f22(x3,x1))
% 38.46/8.28 === Backtracking. Learning clause 104:4:5:[40.1,58.3]:TopTopTopTopTop: p2(f11(x0,x1),x2),p10(x1,x3),p3(x0,x4) -> p2(f11(x4,x3),x2)
% 38.46/8.28 === Backtracking. Learning clause 105:6:7:[40.3,104.1,40.3]:TopTopTopTopTopTopTop: p2(x0,x1),p10(x2,x3),p3(x4,x5),p2(x6,x0),p2(x6,f11(x4,x2)) -> p2(f11(x5,x3),x1)
% 38.46/8.28 === Conflict found: 105:6:7:[40.3,104.1,40.3]:TopTopTopTopTopTopTop: p2(x0,x1),p10(x2,x3),p3(x4,x5),p2(x6,x0),p2(x6,f11(x4,x2)) -> p2(f11(x5,x3),x1) {x0 -> c46, x1 -> c34, x2 -> c34, x3 -> c34, x4 -> c34, x5 -> c34, x6 -> f11(f4(f5(c42)),c45)}
% 38.46/8.28 === Backtracking. Learning clause 106:7:8:[105.5,58.3]:TopTopTopTopTopTopTopTop: p2(x0,x1),p10(x2,x3),p3(x4,x5),p2(f11(x6,x7),x0),p10(x7,x2),p3(x6,x4) -> p2(f11(x5,x3),x1)
% 38.46/8.28 === Backtracking. Learning clause 107:4:3:[49.1,81.2]:TopTopTop: p31(x0,x1),p2(x0,x2),p2(f11(f4(c42),c45),x1) -> p31(x2,f11(f4(f23(c42,f9(f20(c37)))),c45))
% 38.46/8.28 === Backtracking. Learning clause 108:2:1:[49.3,12.1,21.1]:Top: p2(c46,x0) -> p31(f23(c44,f9(f20(c37))),x0)
% 38.46/8.28 === Backtracking. Learning clause 109:3:2:[47.1,51.1]:TopTop: p33(x0,f11(f4(c42),c45)),p2(x0,x1) -> p33(x1,f11(f4(f23(c42,f9(f20(c37)))),c45))
% 38.46/8.28 === Backtracking. Learning clause 110:3:2:[49.3,51.1]:TopTop: p2(x0,x1),p31(f11(f4(c42),c45),x0) -> p31(f11(f4(f23(c42,f9(f20(c37)))),c45),x1)
% 38.46/8.28 === Backtracking. Learning clause 111:3:2:[47.3,51.1]:TopTop: p2(x0,x1),p33(f11(f4(c42),c45),x0) -> p33(f11(f4(f23(c42,f9(f20(c37)))),c45),x1)
% 38.46/8.28 === Conflict found: 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f11(f4(f23(c44,f9(f20(c37)))),c43), x1 -> f11(f4(c44),c43)}
% 38.46/8.28 === Backtracking. Learning clause 112:1:0:[74.1,52.1]:: -> p2(f11(f4(c44),c43),f11(f4(f23(c44,f9(f20(c37)))),c43))
% 38.46/8.28 === Conflict found: 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f19(f11(f4(f5(c42)),c43),f9(f20(c37))), x1 -> f11(f4(c42),c43)}
% 38.46/8.28 === Backtracking. Learning clause 113:1:0:[74.1,61.1]:: -> p2(f11(f4(c42),c43),f19(f11(f4(f5(c42)),c43),f9(f20(c37))))
% 38.46/8.28 === Clause set with instances from active satisfied. Growing active. New size: 321
% 38.46/8.28 === Restarting.
% 38.46/8.28 === Conflict found: 72:2:2:[36.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c34), x1 -> c36}
% 38.46/8.28 === Backtracking. Learning clause 114:2:1:[72.1,99.2]:Top: p6(c35,x0) -> p7(c36,f8(x0))
% 38.46/8.28 === Backtracking. Learning clause 115:3:1:[38.3,90.2]:Top: p3(x0,f4(c46)),p3(x0,f4(f23(c44,f9(f20(c37))))),p10(c43,c43) ->
% 38.46/8.28 === Backtracking. Learning clause 116:5:6:[47.3,58.3]:TopTopTopTopTopTop: p2(x0,x1),p33(f11(x2,x3),x0),p10(x3,x4),p3(x2,x5) -> p33(f11(x5,x4),x1)
% 38.46/8.28 === Conflict found: 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c34, x1 -> f19(f11(f4(f5(c42)),c43),f9(f20(c37)))}
% 38.46/8.28 === Backtracking. Learning clause 117:2:1:[74.2,91.1]:Top: p2(x0,f19(f11(f4(f5(c42)),c43),f9(f20(c37)))) -> p2(x0,f11(f4(c42),c43))
% 38.46/8.28 === Conflict found: 91:2:1:[40.2,61.1]:Top: p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0) -> p2(x0,f11(f4(c42),c43)) {x0 -> f19(c34,c34)}
% 38.46/8.28 === Backtracking. Learning clause 118:5:4:[91.1,57.3,49.1]:TopTopTopTop: p2(f11(f4(f5(c42)),c43),x0),p2(f9(f20(c37)),x1),p31(x2,f19(x0,x1)),p2(x2,x3) -> p31(x3,f11(f4(c42),c43))
% 38.46/8.28 === Conflict found: 106:7:8:[105.5,58.3]:TopTopTopTopTopTopTopTop: p2(x0,x1),p10(x2,x3),p3(x4,x5),p2(f11(x6,x7),x0),p10(x7,x2),p3(x6,x4) -> p2(f11(x5,x3),x1) {x0 -> f11(f4(f23(c44,f9(f20(c37)))),c43), x1 -> f11(f4(f23(c44,f9(f20(c37)))),c43), x2 -> c43, x3 -> c43, x4 -> c34, x5 -> f4(c46), x6 -> f4(c44), x7 -> c43}
% 38.46/8.28 === Backtracking. Learning clause 119:4:2:[106.1,12.1,53.1,112.1]:TopTop: p10(x0,c43),p3(x1,f4(c46)),p10(c43,x0),p3(f4(c44),x1) ->
% 38.46/8.28 === Clause set with instances from active satisfied. Growing active. New size: 381
% 38.46/8.28 === Restarting.
% 38.46/8.28 === Conflict found: 119:4:2:[106.1,12.1,53.1,112.1]:TopTop: p10(x0,c43),p3(x1,f4(c46)),p10(c43,x0),p3(f4(c44),x1) -> {x0 -> c43, x1 -> c34}
% 38.46/8.28 === Backtracking. Learning clause 120:4:2:[119.4,73.2]:TopTop: p10(x0,c43),p3(x1,f4(c46)),p10(c43,x0),p3(x1,f4(c44)) ->
% 38.46/8.28 === Conflict found: 119:4:2:[106.1,12.1,53.1,112.1]:TopTop: p10(x0,c43),p3(x1,f4(c46)),p10(c43,x0),p3(f4(c44),x1) -> {x0 -> c43, x1 -> f4(c34)}
% 38.46/8.28 === Backtracking. Learning clause 121:3:2:[119.4,34.2,34.2,74.2,87.2]:TopTop: p10(x0,c43),p10(c43,x0),p2(x1,c44) ->
% 38.46/8.28 === Conflict found: 74:2:2:[40.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c44, x1 -> f5(c42)}
% 38.46/8.28 === Backtracking. Learning clause 122:3:2:[74.2,121.3]:TopTop: p2(c44,x0),p10(x1,c43),p10(c43,x1) ->
% 38.46/8.28 === Conflict found: 122:3:2:[74.2,121.3]:TopTop: p2(c44,x0),p10(x1,c43),p10(c43,x1) -> {x0 -> c46, x1 -> c43}
% 38.46/8.28
% 38.46/8.28 SZS status Unsatisfiable
% 38.46/8.28
% 38.46/8.28 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.46/8.28
% 38.46/8.28 SPASS-SCL-FOL Statistics:
% 38.46/8.28 Number of learned clauses: 53
% 38.46/8.28 Number of propagations: 2817
% 38.46/8.28 Number of decisions: 2093
% 38.46/8.28 Number of resolutions: 68
% 38.46/8.28 Number of condensations: 0
% 38.46/8.28 Number of sub resolutions: 0
% 38.46/8.28 Number of input literals (deduplicated): 74
% 38.46/8.28 Number of grows: 5
% 38.46/8.28 Number of considered ground atoms: 381
% 38.46/8.28
% 38.46/8.28 Needed: 0:00:07.68
% 38.46/8.28
%------------------------------------------------------------------------------