%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN719-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 : n020.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 0.46s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.17 % Problem : SYN719-1 : TPTP v9.2.1. Released v2.5.0.
% 0.09/0.18 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.40 % Computer : n020.cluster.edu
% 0.22/0.40 % Model : x86_64 x86_64
% 0.22/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.40 % Memory : 8042.1875MB
% 0.22/0.40 % OS : Linux 3.10.0-693.el7.x86_64
% 0.22/0.40 % CPULimit : 300
% 0.22/0.40 % WCLimit : 300
% 0.22/0.40 % DateTime : Thu May 7 13:47:51 EDT 2026
% 0.22/0.40 % CPUTime :
% 0.22/0.40 SPASS-SCL-FOL version:
% 0.28/0.51 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.46/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.83 Execution resolution_3 ended with status: unsatisfiable
% 0.46/0.83 Used heuristic: resolution_3
% 0.46/0.83
% 0.46/0.83 Input Clauses:
% 0.46/0.83
% 0.46/0.83 Predicates: p10 p9 p7 p63 p61 p6 p59 p57 p56 p55 p53 p52 p50 p48 p47 p45 p43 p41 p4 p39 p37 p35 p34 p33 p31 p3 p29 p28 p27 p25 p24 p22 p20 p2 p18 p17 p15 p14 p13 p11 p66 p67 p70 p65 p68 p73 p72 p69 p71
% 0.46/0.83 Fol Constants: c78 c77 c79 c80 c81 c82 c88 c85 c74 c75 c76 c84 c83 c90 c86 c94 c93 c91 c92 c87 c89
% 0.46/0.83 Fol Functions: f12 f16 f30 f38 f8 f5 f26 f23 f21 f19 f58 f36 f64 f60 f54 f51 f46 f44 f42 f62 f40 f49 f32
% 0.46/0.83 Problem Properties:
% 0.46/0.83 This is a full first-order problem without equality.
% 0.46/0.83
% 0.46/0.83 After reduction: Problem Properties:
% 0.46/0.83 This is a full first-order problem without equality.
% 0.46/0.83
% 0.46/0.83
% 0.46/0.83 Reduced Input Clauses:
% 0.46/0.83
% 0.46/0.83 Most General Atoms: p6(x1,x2) p57(x1,x2) p55(x1,x2) p53(x1,x2) p47(x1,x2) p4(x1,x2) p35(x1,x2) p33(x1,x2) p27(x1,x2) p24(x1,x2) p2(x1,x2) p17(x1,x2) p13(x1,x2) p28(x2,x3) p73(x3,x1) p10(x2,x3) p65(x1,x3) p11(x2,x3) p66(x3,x1) p15(x0,x3) p67(x3,x2) p68(x2,x3) p29(x2,x3) p69(x1,x3) p70(x3,x1) p48(x2,x3) p71(x1,x3) p72(x1,x3) p9(x2,x3) p18(x2,x3) p63(x2,x3) p56(x2,x3) p59(x2,x3) p52(x2,x3) p50(x2,x3) p45(x2,x3) p43(x2,x3) p3(x2,x3) p41(x2,x3) p61(x2,x3) p39(x2,x3) p34(x2,x3) p37(x2,x3) p7(x2,x3) p31(x2,x3) p25(x2,x3) p20(x2,x3) p14(x2,x3) p22(x2,x3)
% 0.46/0.83
% 0.46/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 53 atoms initially, heuristics mode: resolution_3 ===
% 0.46/0.83
% 0.46/0.83 === Backtracking. Learning clause 127:1:0:[48.1,42.1]:: -> p68(c82,c81)
% 0.46/0.83 === Backtracking. Learning clause 128:3:2:[94.2,44.1]:TopTop: p4(f5(c74,f8(c75,c76)),x0),p10(c77,x1) -> p65(x0,x1)
% 0.46/0.83 === Clause set with instances from active satisfied. Growing active. New size: 117
% 0.46/0.83 === Restarting.
% 0.46/0.83 === Backtracking. Learning clause 129:3:2:[95.2,41.1]:TopTop: p18(c79,x0),p11(f12(c78,c77),x1) -> p66(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 130:3:2:[96.1,42.1]:TopTop: p7(c82,x0),p15(f16(c80,c81),x1) -> p67(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 131:4:4:[101.4,47.1]:TopTopTopTop: p57(x0,f58(c90,x1)),p72(x0,x2),p28(x2,x3) -> p73(x3,x1)
% 0.46/0.83 === Backtracking. Learning clause 132:4:4:[98.4,49.1]:TopTopTopTop: p35(x0,f36(c86,x1)),p69(x0,x2),p29(x2,x3) -> p70(x3,x1)
% 0.46/0.83 === Backtracking. Learning clause 133:2:2:[55.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 134:2:2:[59.2,7.1]:TopTop: p59(x0,x1) -> p59(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 135:2:2:[60.2,8.1]:TopTop: p57(x0,x1) -> p57(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 136:2:2:[61.2,9.1]:TopTop: p56(x0,x1) -> p56(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 137:2:2:[63.2,11.1]:TopTop: p53(x0,x1) -> p53(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 138:2:2:[67.2,15.1]:TopTop: p47(x0,x1) -> p47(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 139:2:2:[69.2,17.1]:TopTop: p43(x0,x1) -> p43(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 140:2:2:[70.2,18.1]:TopTop: p41(x0,x1) -> p41(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 141:2:2:[71.2,19.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 142:2:2:[72.2,20.1]:TopTop: p39(x0,x1) -> p39(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 143:2:2:[73.2,21.1]:TopTop: p37(x0,x1) -> p37(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 144:2:2:[92.2,40.1]:TopTop: p11(x0,x1) -> p11(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 145:3:4:[99.2,43.1]:TopTopTopTop: p34(f38(c85,x0),x1),p29(f30(c88,x2),x3) -> p70(x3,x1)
% 0.46/0.83 === Clause set with instances from active satisfied. Growing active. New size: 182
% 0.46/0.83 === Restarting.
% 0.46/0.83 === Backtracking. Learning clause 146:3:2:[97.1,127.1]:TopTop: p7(c82,x0),p14(c81,x1) -> p68(x0,x1)
% 0.46/0.83 === Conflict found: 144:2:2:[92.2,40.1]:TopTop: p11(x0,x1) -> p11(x1,x0) {x0 -> c78, x1 -> f12(c78,c77)}
% 0.46/0.83 === Backtracking. Learning clause 147:3:2:[144.2,129.2]:TopTop: p11(x0,f12(c78,c77)),p18(c79,x1) -> p66(x0,x1)
% 0.46/0.83 === Backtracking. Learning clause 148:5:5:[96.1,50.2,89.3]:TopTopTopTopTop: p7(x0,x1),p68(x0,x2),p15(x3,f16(c80,x2)),p15(x3,x4) -> p67(x4,x1)
% 0.46/0.83 === Backtracking. Learning clause 149:4:4:[96.1,50.2]:TopTopTopTop: p7(x0,x1),p15(f16(c80,x2),x3),p68(x0,x2) -> p67(x3,x1)
% 0.46/0.83 === Conflict found: 141:2:2:[71.2,19.1]:TopTop: p4(x0,x1) -> p4(x1,x0) {x0 -> c78, x1 -> f5(c74,f8(c75,c76))}
% 0.46/0.83 === Backtracking. Learning clause 150:3:2:[141.2,128.1]:TopTop: p4(x0,f5(c74,f8(c75,c76))),p10(c77,x1) -> p65(x0,x1)
% 0.46/0.83 === Backtracking. Learning clause 151:2:2:[74.2,22.1]:TopTop: p35(x0,x1) -> p35(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 152:2:2:[75.2,23.1]:TopTop: p34(x0,x1) -> p34(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 153:2:2:[78.2,26.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 154:2:2:[79.2,27.1]:TopTop: p29(x0,x1) -> p29(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 155:2:2:[80.2,28.1]:TopTop: p28(x0,x1) -> p28(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 156:2:2:[84.2,32.1]:TopTop: p22(x0,x1) -> p22(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 157:2:2:[88.2,36.1]:TopTop: p17(x0,x1) -> p17(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 158:2:2:[89.2,37.1]:TopTop: p15(x0,x1) -> p15(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 159:2:2:[90.2,38.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 0.46/0.83 === Backtracking. Learning clause 160:3:2:[97.4,46.1]:TopTop: p68(x0,x1),p7(x0,f19(f21(c83,c77),c79)),p14(x1,c81) ->
% 0.46/0.83 === Backtracking. Learning clause 161:2:1:[94.1,19.1,44.1]:Top: p10(c77,x0) -> p65(f5(c74,f8(c75,c76)),x0)
% 0.46/0.83 === Backtracking. Learning clause 162:5:5:[101.4,125.2]:TopTopTopTopTop: p57(x0,f58(c90,f60(f64(c91,x1),f62(c92,x2)))),p72(x0,x3),p28(x3,x4),p71(f54(c93,f30(c88,x4)),x2) -> p70(f30(c88,x4),f49(f51(c94,x1),x2))
% 0.46/0.83 === Backtracking. Learning clause 163:3:3:[51.2,125.2]:TopTopTop: p73(x0,f60(f64(c91,x1),f62(c92,x2))),p71(f54(c93,f30(c88,x0)),x2) -> p70(f30(c88,x0),f49(f51(c94,x1),x2))
% 0.46/0.83 === Backtracking. Learning clause 164:7:6:[52.2,126.4,132.4]:TopTopTopTopTopTop: p67(f16(c80,x0),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,x3),x0)),p35(x4,f36(c86,f38(x3,f40(f42(f44(f46(c87,x1),x2),x3),x0)))),p69(x4,x5),p29(x5,f30(c88,f32(c89,f8(c75,c76)))) -> p68(f19(f21(c83,c77),x1),x2)
% 0.46/0.83 === Backtracking. Learning clause 165:5:4:[52.2,126.4]:TopTopTopTop: p70(f30(c88,f32(c89,f8(c75,c76))),f38(x0,f40(f42(f44(f46(c87,x1),x2),x0),x3))),p67(f16(c80,x3),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,x0),x3)) -> p68(f19(f21(c83,c77),x1),x2)
% 0.46/0.83 === Clause set with instances from active satisfied. Growing active. New size: 231
% 0.46/0.83 === Restarting.
% 0.46/0.83 === Conflict found: 154:2:2:[79.2,27.1]:TopTop: p29(x0,x1) -> p29(x1,x0) {x0 -> c78, x1 -> f30(c88,c78)}
% 0.46/0.83 === Backtracking. Learning clause 166:3:4:[154.2,145.2]:TopTopTopTop: p29(x0,f30(c88,x1)),p34(f38(c85,x2),x3) -> p70(x0,x3)
% 0.46/0.83 === Conflict found: 131:4:4:[101.4,47.1]:TopTopTopTop: p57(x0,f58(c90,x1)),p72(x0,x2),p28(x2,x3) -> p73(x3,x1) {x0 -> f58(c78,c78), x1 -> c78, x2 -> c78, x3 -> c78}
% 0.46/0.83 === Backtracking. Learning clause 167:5:5:[131.1,105.3]:TopTopTopTopTop: p72(f58(x0,x1),x2),p28(x2,x3),p55(x0,c90),p56(x1,x4) -> p73(x3,x4)
% 0.46/0.83 === Backtracking. Learning clause 168:5:5:[98.1,115.3,49.1]:TopTopTopTopTop: p69(f36(x0,x1),x2),p29(x2,x3),p33(x0,c86),p34(x1,x4) -> p70(x3,x4)
% 0.46/0.83 === Backtracking. Learning clause 169:4:5:[75.1,117.3]:TopTopTopTopTop: p34(f38(x0,x1),x2),p25(x0,x3),p37(x1,x4) -> p34(f38(x3,x4),x2)
% 0.46/0.83 === Conflict found: 166:3:4:[154.2,145.2]:TopTopTopTop: p29(x0,f30(c88,x1)),p34(f38(c85,x2),x3) -> p70(x0,x3) {x0 -> c78, x1 -> c78, x2 -> c78, x3 -> f38(c85,c78)}
% 0.46/0.83 === Backtracking. Learning clause 170:2:3:[166.2,23.1]:TopTopTop: p29(x0,f30(c88,x1)) -> p70(x0,f38(c85,x2))
% 0.46/0.83 === Backtracking. Learning clause 171:4:5:[79.1,119.3,154.2,154.1]:TopTopTopTopTop: p27(x0,x1),p28(x2,x3),p29(x4,f30(x0,x2)) -> p29(x4,f30(x1,x3))
% 0.46/0.83 === Conflict found: 148:5:5:[96.1,50.2,89.3]:TopTopTopTopTop: p7(x0,x1),p68(x0,x2),p15(x3,f16(c80,x2)),p15(x3,x4) -> p67(x4,x1) {x0 -> c82, x1 -> c78, x2 -> c81, x3 -> f16(c80,c81), x4 -> f16(c80,c81)}
% 0.46/0.83 === Backtracking. Learning clause 172:3:3:[148.3,37.1]:TopTopTop: p7(x0,x1),p68(x0,x2) -> p67(f16(c80,x2),x1)
% 0.46/0.83 === Conflict found: 159:2:2:[90.2,38.1]:TopTop: p14(x0,x1) -> p14(x1,x0) {x0 -> f23(f26(c84,c85),c78), x1 -> c78}
% 0.46/0.83 === Backtracking. Learning clause 173:1:1:[159.1,45.1]:Top: -> p14(x0,f23(f26(c84,c85),x0))
% 0.46/0.83 === Conflict found: 160:3:2:[97.4,46.1]:TopTop: p68(x0,x1),p7(x0,f19(f21(c83,c77),c79)),p14(x1,c81) -> {x0 -> f19(c78,c78), x1 -> c78}
% 0.46/0.83 === Backtracking. Learning clause 174:4:3:[160.2,103.3]:TopTopTop: p68(f19(x0,x1),x2),p14(x2,c81),p17(x0,f21(c83,c77)),p18(x1,c79) ->
% 0.46/0.83 === Backtracking. Learning clause 175:2:1:[97.2,3.1,46.1]:Top: p68(f19(f21(c83,c77),c79),x0),p14(x0,c81) ->
% 0.46/0.83 === Conflict found: 164:7:6:[52.2,126.4,132.4]:TopTopTopTopTopTop: p67(f16(c80,x0),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,x3),x0)),p35(x4,f36(c86,f38(x3,f40(f42(f44(f46(c87,x1),x2),x3),x0)))),p69(x4,x5),p29(x5,f30(c88,f32(c89,f8(c75,c76)))) -> p68(f19(f21(c83,c77),x1),x2) {x0 -> c78, x1 -> c78, x2 -> c78, x3 -> c78, x4 -> c78, x5 -> f30(c88,f32(c89,f8(c75,c76)))}
% 0.46/0.83 === Backtracking. Learning clause 176:6:5:[164.6,27.1]:TopTopTopTopTop: p67(f16(c80,x0),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,x3),x0)),p35(x4,f36(c86,f38(x3,f40(f42(f44(f46(c87,x1),x2),x3),x0)))),p69(x4,f30(c88,f32(c89,f8(c75,c76)))) -> p68(f19(f21(c83,c77),x1),x2)
% 0.46/0.83 === Conflict found: 145:3:4:[99.2,43.1]:TopTopTopTop: p34(f38(c85,x0),x1),p29(f30(c88,x2),x3) -> p70(x3,x1) {x0 -> c78, x1 -> f38(c78,f40(f42(f44(f46(c87,c78),c78),c78),c78)), x2 -> f32(c89,f8(c75,c76)), x3 -> f30(c88,f32(c89,f8(c75,c76)))}
% 0.46/0.83 === Backtracking. Learning clause 177:5:5:[145.3,165.1,27.1]:TopTopTopTopTop: p34(f38(c85,x0),f38(x1,f40(f42(f44(f46(c87,x2),x3),x1),x4))),p67(f16(c80,x4),c82),p66(f12(c78,c77),x2),p14(x3,f23(f26(c84,x1),x4)) -> p68(f19(f21(c83,c77),x2),x3)
% 0.46/0.83 === Conflict found: 165:5:4:[52.2,126.4]:TopTopTopTop: p70(f30(c88,f32(c89,f8(c75,c76))),f38(x0,f40(f42(f44(f46(c87,x1),x2),x0),x3))),p67(f16(c80,x3),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,x0),x3)) -> p68(f19(f21(c83,c77),x1),x2) {x0 -> c85, x1 -> c78, x2 -> c78, x3 -> c78}
% 0.46/0.83 === Backtracking. Learning clause 178:4:3:[165.1,43.1]:TopTopTop: p67(f16(c80,x0),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,c85),x0)) -> p68(f19(f21(c83,c77),x1),x2)
% 0.46/0.83 === Conflict found: 178:4:3:[165.1,43.1]:TopTopTop: p67(f16(c80,x0),c82),p66(f12(c78,c77),x1),p14(x2,f23(f26(c84,c85),x0)) -> p68(f19(f21(c83,c77),x1),x2) {x0 -> c78, x1 -> c79, x2 -> c78}
% 0.46/0.83 === Backtracking. Learning clause 180:2:1:[41.0,179.1,178.4,175.1,173.1]:Top: p67(f16(c80,x0),c82),p14(x0,c81) ->
% 0.46/0.83 === Conflict found: 180:2:1:[41.0,179.1,178.4,175.1,173.1]:Top: p67(f16(c80,x0),c82),p14(x0,c81) -> {x0 -> c81}
% 0.46/0.83
% 0.46/0.83 SZS status Unsatisfiable
% 0.46/0.83
% 0.46/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.83
% 0.46/0.83 SPASS-SCL-FOL Statistics:
% 0.46/0.83 Number of learned clauses: 53
% 0.46/0.83 Number of propagations: 2811
% 0.46/0.83 Number of decisions: 2022
% 0.46/0.83 Number of resolutions: 64
% 0.46/0.83 Number of condensations: 0
% 0.46/0.83 Number of sub resolutions: 1
% 0.46/0.83 Number of input literals (deduplicated): 129
% 0.46/0.83 Number of grows: 3
% 0.46/0.83 Number of considered ground atoms: 231
% 0.46/0.83
% 0.46/0.83 Needed: 0:00:00.19
% 0.46/0.83
%------------------------------------------------------------------------------