%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN692-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 : n001.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 20.01s 4.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN692-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 : n001.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:04 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]
% 20.01/4.59 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.01/4.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.01/4.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.01/4.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.01/4.59 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.01/4.59 Execution resolution_3 ended with status: unsatisfiable
% 20.01/4.59 Used heuristic: resolution_3
% 20.01/4.59
% 20.01/4.59 Input Clauses:
% 20.01/4.59
% 20.01/4.59 Predicates: p25 p29 p30 p28 p10 p7 p6 p3 p21 p2 p17 p14 p12 p31 p26 p33 p27 p32
% 20.01/4.59 Fol Constants: c34 c36 c41 c38 c39 c40 c44 c45 c42 c35 c37 c43
% 20.01/4.59 Fol Functions: f18 f16 f5 f8 f20 f9 f23 f4 f24 f11 f13 f19 f22 f15
% 20.01/4.59 Problem Properties:
% 20.01/4.59 This is a full first-order problem without equality.
% 20.01/4.59
% 20.01/4.59 After reduction: Problem Properties:
% 20.01/4.59 This is a full first-order problem without equality.
% 20.01/4.59
% 20.01/4.59
% 20.01/4.59 Reduced Input Clauses:
% 20.01/4.59
% 20.01/4.59 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)
% 20.01/4.59
% 20.01/4.59 === Starting SPASS-SCL-FOL A Little Less Naive, considering 57 atoms initially, heuristics mode: resolution_3 ===
% 20.01/4.59
% 20.01/4.59 === Backtracking. Learning clause 69:2:1:[39.2,16.1]:Top: p2(c44,x0) -> p2(x0,c45)
% 20.01/4.59 === Backtracking. Learning clause 70:2:1:[35.2,19.1]:Top: p7(f8(c35),x0) -> p7(x0,c36)
% 20.01/4.59 === Backtracking. Learning clause 71:2:2:[35.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 72:2:2:[37.2,10.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 73:2:2:[39.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 74:2:2:[40.2,13.1]:TopTop: p17(x0,x1) -> p17(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 75:2:2:[41.2,14.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 20.01/4.59 === Clause set with instances from active satisfied. Growing active. New size: 122
% 20.01/4.59 === Restarting.
% 20.01/4.59 === Backtracking. Learning clause 76:2:2:[42.2,15.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 77:3:2:[48.2,43.1]:TopTop: p2(f11(f4(c42),c43),x0),p2(f11(f4(f5(c42)),c43),x1) -> p31(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 78:2:1:[39.3,52.1]:Top: p2(x0,f11(f4(c45),c43)),p2(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)) ->
% 20.01/4.59 === Backtracking. Learning clause 79:3:2:[46.3,50.1]:TopTop: p2(x0,x1),p33(f11(f4(c42),c43),x0) -> p33(f11(f4(f23(c42,f9(f20(c37)))),c43),x1)
% 20.01/4.59 === Backtracking. Learning clause 80:3:2:[46.1,50.1]:TopTop: p33(x0,f11(f4(c42),c43)),p2(x0,x1) -> p33(x1,f11(f4(f23(c42,f9(f20(c37)))),c43))
% 20.01/4.59 === Backtracking. Learning clause 81:2:1:[39.1,50.1,73.1]:Top: p2(f11(f4(c42),c43),x0) -> p2(x0,f11(f4(f23(c42,f9(f20(c37)))),c43))
% 20.01/4.59 === Backtracking. Learning clause 82:3:2:[48.3,51.1]:TopTop: p2(x0,x1),p31(f11(f4(f23(c44,f9(f20(c37)))),c43),x0) -> p31(f11(f4(c44),c43),x1)
% 20.01/4.59 === Backtracking. Learning clause 83:3:2:[48.1,51.1]:TopTop: p31(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)),p2(x0,x1) -> p31(x1,f11(f4(c44),c43))
% 20.01/4.59 === Backtracking. Learning clause 84:3:2:[46.3,51.1]:TopTop: p2(x0,x1),p33(f11(f4(f23(c44,f9(f20(c37)))),c43),x0) -> p33(f11(f4(c44),c43),x1)
% 20.01/4.59 === Backtracking. Learning clause 85:3:2:[46.1,51.1]:TopTop: p33(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)),p2(x0,x1) -> p33(x1,f11(f4(c44),c43))
% 20.01/4.59 === Clause set with instances from active satisfied. Growing active. New size: 187
% 20.01/4.59 === Restarting.
% 20.01/4.59 === Conflict found: 69:2:1:[39.2,16.1]:Top: p2(c44,x0) -> p2(x0,c45) {x0 -> c34}
% 20.01/4.59 === Backtracking. Learning clause 86:2:1:[69.1,73.2]:Top: p2(x0,c44) -> p2(x0,c45)
% 20.01/4.59 === Conflict found: 71:2:2:[35.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c34, x1 -> f8(c35)}
% 20.01/4.59 === Backtracking. Learning clause 87:2:1:[71.2,70.1]:Top: p7(x0,f8(c35)) -> p7(x0,c36)
% 20.01/4.59 === Backtracking. Learning clause 88:3:2:[48.2,18.1]:TopTop: p2(f5(c42),x0),p2(c44,x1) -> p31(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 89:2:1:[35.1,26.2,19.1]:Top: p6(c35,x0) -> p7(f8(x0),c36)
% 20.01/4.59 === Backtracking. Learning clause 90:3:2:[48.2,20.1]:TopTop: p2(c45,x0),p2(f23(c44,f9(f20(c37))),x1) -> p31(x1,x0)
% 20.01/4.59 === Backtracking. Learning clause 91:4:3:[46.4,61.1]:TopTopTop: p2(x0,f11(f4(c42),x1)),p33(x2,x0),p2(x2,f11(f4(f5(c42)),x1)) -> p32(f22(c34,x1),c43)
% 20.01/4.59 === Backtracking. Learning clause 92:2:0:[57.3,52.1]:: p10(c43,c43),p3(f4(c45),f4(f23(c44,f9(f20(c37))))) ->
% 20.01/4.59 === Conflict found: 77:3:2:[48.2,43.1]:TopTop: p2(f11(f4(c42),c43),x0),p2(f11(f4(f5(c42)),c43),x1) -> p31(x1,x0) {x0 -> f11(f4(f23(c42,f9(f20(c37)))),c43), x1 -> c34}
% 20.01/4.59 === Backtracking. Learning clause 93:2:1:[77.1,50.1]:Top: p2(f11(f4(f5(c42)),c43),x0) -> p31(x0,f11(f4(f23(c42,f9(f20(c37)))),c43))
% 20.01/4.59 === Backtracking. Learning clause 94:3:2:[48.3,50.1]:TopTop: p2(x0,x1),p31(f11(f4(c42),c43),x0) -> p31(f11(f4(f23(c42,f9(f20(c37)))),c43),x1)
% 20.01/4.59 === Backtracking. Learning clause 95:2:1:[39.2,60.1]:Top: p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),x0) -> p2(x0,f11(f4(c42),c43))
% 20.01/4.59 === Clause set with instances from active satisfied. Growing active. New size: 260
% 20.01/4.59 === Restarting.
% 20.01/4.59 === Backtracking. Learning clause 96:2:2:[34.2,7.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 20.01/4.59 === Conflict found: 71:2:2:[35.2,8.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c34), x1 -> c36}
% 20.01/4.59 === Backtracking. Learning clause 97:2:1:[71.1,89.2]:Top: p6(c35,x0) -> p7(c36,f8(x0))
% 20.01/4.59 === Conflict found: 73:2:2:[39.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c34, x1 -> f5(c42)}
% 20.01/4.59 === Backtracking. Learning clause 98:3:2:[73.2,88.1]:TopTop: p2(x0,f5(c42)),p2(c44,x1) -> p31(x1,x0)
% 20.01/4.59 === Conflict found: 73:2:2:[39.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c34, x1 -> f23(c44,f9(f20(c37)))}
% 20.01/4.59 === Backtracking. Learning clause 99:3:2:[73.2,90.2]:TopTop: p2(x0,f23(c44,f9(f20(c37)))),p2(c45,x1) -> p31(x0,x1)
% 20.01/4.59 === Backtracking. Learning clause 100:4:2:[39.2,62.3,73.2]:TopTop: p31(c44,x0),p31(x0,f5(c42)),p2(x1,f11(f4(x0),c43)) -> p2(x1,f11(f4(c44),c43))
% 20.01/4.59 === Backtracking. Learning clause 101:4:3:[48.1,81.2]:TopTopTop: p31(x0,x1),p2(x0,x2),p2(f11(f4(c42),c43),x1) -> p31(x2,f11(f4(f23(c42,f9(f20(c37)))),c43))
% 20.01/4.59 === Backtracking. Learning clause 102:2:1:[48.3,12.1,20.1]:Top: p2(c45,x0) -> p31(f23(c44,f9(f20(c37))),x0)
% 20.01/4.59 === Conflict found: 73:2:2:[39.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f11(f4(f23(c44,f9(f20(c37)))),c43), x1 -> f11(f4(c44),c43)}
% 20.01/4.59 === Backtracking. Learning clause 103:1:0:[73.1,51.1]:: -> p2(f11(f4(c44),c43),f11(f4(f23(c44,f9(f20(c37)))),c43))
% 20.01/4.59 === Conflict found: 73:2:2:[39.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)}
% 20.01/4.59 === Backtracking. Learning clause 104:1:0:[73.1,60.1]:: -> p2(f11(f4(c42),c43),f19(f11(f4(f5(c42)),c43),f9(f20(c37))))
% 20.01/4.59 === Conflict found: 81:2:1:[39.1,50.1,73.1]:Top: p2(f11(f4(c42),c43),x0) -> p2(x0,f11(f4(f23(c42,f9(f20(c37)))),c43)) {x0 -> f11(f4(f24(f23(c42,f9(f20(c37))))),c43)}
% 20.01/4.59 === Backtracking. Learning clause 105:3:0:[81.2,64.3]:: p2(f11(f4(c42),c43),f11(f4(f24(f23(c42,f9(f20(c37))))),c43)),p31(f23(c42,f9(f20(c37))),c44),p31(f23(c42,f9(f20(c37))),f5(c42)) ->
% 20.01/4.59 === Clause set with instances from active satisfied. Growing active. New size: 309
% 20.01/4.59 === Restarting.
% 20.01/4.59 === Backtracking. Learning clause 106:3:1:[37.3,92.2]:Top: p3(x0,f4(c45)),p3(x0,f4(f23(c44,f9(f20(c37))))),p10(c43,c43) ->
% 20.01/4.59 === Conflict found: 91:4:3:[46.4,61.1]:TopTopTop: p2(x0,f11(f4(c42),x1)),p33(x2,x0),p2(x2,f11(f4(f5(c42)),x1)) -> p32(f22(c34,x1),c43) {x0 -> c34, x1 -> c34, x2 -> f11(c34,c34)}
% 20.01/4.59 === Backtracking. Learning clause 107:5:4:[91.3,57.3]:TopTopTopTop: p2(x0,f11(f4(c42),x1)),p33(f11(x2,x3),x0),p10(x3,x1),p3(x2,f4(f5(c42))) -> p32(f22(c34,x1),c43)
% 20.01/4.59 === Conflict found: 91:4:3:[46.4,61.1]:TopTopTop: p2(x0,f11(f4(c42),x1)),p33(x2,x0),p2(x2,f11(f4(f5(c42)),x1)) -> p32(f22(c34,x1),c43) {x0 -> f11(c34,c34), x1 -> c34, x2 -> c34}
% 20.01/4.59 === Backtracking. Learning clause 108:5:4:[91.1,57.3]:TopTopTopTop: p33(x0,f11(x1,x2)),p2(x0,f11(f4(f5(c42)),x3)),p10(x2,x3),p3(x1,f4(c42)) -> p32(f22(c34,x3),c43)
% 20.01/4.59 === Backtracking. Learning clause 109:4:2:[39.2,62.3]:TopTop: p2(f11(f4(x0),c43),x1),p31(c44,x0),p31(x0,f5(c42)) -> p2(x1,f11(f4(c44),c43))
% 20.01/4.59 === Conflict found: 100:4:2:[39.2,62.3,73.2]:TopTop: p31(c44,x0),p31(x0,f5(c42)),p2(x1,f11(f4(x0),c43)) -> p2(x1,f11(f4(c44),c43)) {x0 -> f23(c42,f9(f20(c37))), x1 -> f5(c42)}
% 20.01/4.59 === Backtracking. Learning clause 110:4:1:[100.3,81.2]:Top: p31(c44,f23(c42,f9(f20(c37)))),p31(f23(c42,f9(f20(c37))),f5(c42)),p2(f11(f4(c42),c43),x0) -> p2(x0,f11(f4(c44),c43))
% 20.01/4.59 === Conflict found: 73:2:2:[39.2,12.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c34, x1 -> f19(f11(f4(f5(c42)),c43),f9(f20(c37)))}
% 20.01/4.59 === Backtracking. Learning clause 111:2:1:[73.2,95.1]:Top: p2(x0,f19(f11(f4(f5(c42)),c43),f9(f20(c37)))) -> p2(x0,f11(f4(c42),c43))
% 20.01/4.59 === Conflict found: 78:2:1:[39.3,52.1]:Top: p2(x0,f11(f4(c45),c43)),p2(x0,f11(f4(f23(c44,f9(f20(c37)))),c43)) -> {x0 -> f11(f4(c44),c43)}
% 20.01/4.59 === Backtracking. Learning clause 112:1:0:[78.2,103.1]:: p2(f11(f4(c44),c43),f11(f4(c45),c43)) ->
% 20.01/4.59 === Clause set with instances from active satisfied. Growing active. New size: 335
% 20.01/4.59 === Restarting.
% 20.01/4.59 === Conflict found: 107:5:4:[91.3,57.3]:TopTopTopTop: p2(x0,f11(f4(c42),x1)),p33(f11(x2,x3),x0),p10(x3,x1),p3(x2,f4(f5(c42))) -> p32(f22(c34,x1),c43) {x0 -> f11(c34,c34), x1 -> c34, x2 -> c34, x3 -> c34}
% 20.01/4.59 === Backtracking. Learning clause 113:6:5:[107.1,57.3]:TopTopTopTopTop: p33(f11(x0,x1),f11(x2,x3)),p10(x1,x4),p3(x0,f4(f5(c42))),p10(x3,x4),p3(x2,f4(c42)) -> p32(f22(c34,x4),c43)
% 20.01/4.59 === Conflict found: 110:4:1:[100.3,81.2]:Top: p31(c44,f23(c42,f9(f20(c37)))),p31(f23(c42,f9(f20(c37))),f5(c42)),p2(f11(f4(c42),c43),x0) -> p2(x0,f11(f4(c44),c43)) {x0 -> f11(c34,c34)}
% 20.01/4.59 === Backtracking. Learning clause 114:6:3:[110.2,48.4]:TopTopTop: p31(c44,f23(c42,f9(f20(c37)))),p2(f11(f4(c42),c43),x0),p2(x1,f5(c42)),p31(x2,x1),p2(x2,f23(c42,f9(f20(c37)))) -> p2(x0,f11(f4(c44),c43))
% 20.01/4.59
% 20.01/4.59 SZS status Unsatisfiable
% 20.01/4.59
% 20.01/4.59 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.01/4.59
% 20.01/4.59 SPASS-SCL-FOL Statistics:
% 20.01/4.59 Number of learned clauses: 46
% 20.01/4.59 Number of propagations: 2368
% 20.01/4.59 Number of decisions: 1952
% 20.01/4.59 Number of resolutions: 54
% 20.01/4.59 Number of condensations: 0
% 20.01/4.59 Number of sub resolutions: 0
% 20.01/4.59 Number of input literals (deduplicated): 73
% 20.01/4.59 Number of grows: 5
% 20.01/4.59 Number of considered ground atoms: 335
% 20.01/4.59
% 20.01/4.59 Needed: 0:00:04.03
% 20.01/4.60
%------------------------------------------------------------------------------