%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYN711-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 : n007.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 17.48s 4.93s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.16 % Problem : SYN711-1 : TPTP v9.2.1. Released v2.5.0. % 0.10/0.17 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.22/0.40 % Computer : n007.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:46:24 EDT 2026 % 0.22/0.40 % CPUTime : % 0.22/0.40 SPASS-SCL-FOL version: % 0.26/0.50 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 17.48/4.93 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.48/4.93 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.48/4.93 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.48/4.93 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.48/4.93 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.48/4.93 Execution resolution_3 ended with status: unsatisfiable % 17.48/4.93 Used heuristic: resolution_3 % 17.48/4.93 % 17.48/4.93 Input Clauses: % 17.48/4.93 % 17.48/4.93 Predicates: p39 p45 p17 p9 p6 p5 p33 p3 p28 p26 p24 p22 p2 p19 p44 p40 p42 p41 p43 % 17.48/4.93 Fol Constants: c46 c56 c47 c58 c55 c57 c52 c48 c62 c49 c50 c53 c1 c54 c51 c59 c61 c60 c63 % 17.48/4.93 Fol Functions: f34 f7 f4 f16 f12 f11 f10 f8 f15 f18 f23 f13 f38 f35 f37 f30 f27 f31 f25 f20 f36 f32 f14 f21 % 17.48/4.93 Problem Properties: % 17.48/4.93 This is a full first-order problem without equality. % 17.48/4.93 % 17.48/4.93 After reduction: Problem Properties: % 17.48/4.93 This is a full first-order problem without equality. % 17.48/4.93 % 17.48/4.93 % 17.48/4.93 Reduced Input Clauses: % 17.48/4.93 % 17.48/4.93 Most General Atoms: p39(x1) p45(x1) p17(x1,x2) p28(x1,x2) p22(x1,x2) p2(x1,x2) p19(x1,x2) p3(x1,x3) p40(x2,x3) p33(x1,x3) p44(x2,x3) p6(x2,x3) p43(x1,x3) p42(x1,x3) p41(x1,x3) p9(x2,x3) p26(x2,x3) p24(x4,x5) p5(x6,x7) % 17.48/4.93 % 17.48/4.93 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_3 === % 17.48/4.93 % 17.48/4.93 === Backtracking. Learning clause 90:2:2:[44.2,8.1]:TopTop: p9(x0,x1) -> p9(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 91:2:2:[45.2,9.1]:TopTop: p6(x0,x1) -> p6(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 92:2:2:[46.2,10.1]:TopTop: p5(x0,x1) -> p5(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 93:2:1:[47.1,25.1]:Top: p42(f16(f7(c46)),x0) -> p42(f16(c62),x0) % 17.48/4.93 === Backtracking. Learning clause 94:2:1:[47.2,25.1]:Top: p42(x0,f16(c62)) -> p42(x0,f16(f7(c46))) % 17.48/4.93 === Backtracking. Learning clause 95:1:0:[26.1,29.1]:: -> p42(f8(f10(f11(f12(c49)))),f7(c46)) % 17.48/4.93 === Clause set with instances from active satisfied. Growing active. New size: 123 % 17.48/4.93 === Restarting. % 17.48/4.93 === Backtracking. Learning clause 96:2:2:[48.2,11.1]:TopTop: p33(x0,x1) -> p33(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 97:2:2:[49.2,12.1]:TopTop: p3(x0,x1) -> p3(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 98:3:2:[61.1,24.1]:TopTop: p6(f7(c47),x0),p3(f4(c48),x1) -> p40(x0,x1) % 17.48/4.93 === Backtracking. Learning clause 99:2:1:[45.1,56.1,91.1]:Top: p6(f7(c56),x0) -> p6(x0,f37(f35(f7(c50),f7(c46)),f7(c55))) % 17.48/4.93 === Backtracking. Learning clause 100:2:1:[46.2,57.1]:Top: p5(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)),x0) -> p5(x0,c56) % 17.48/4.93 === Backtracking. Learning clause 101:2:0:[28.2,57.1]:: p45(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55))) -> p45(c56) % 17.48/4.93 === Backtracking. Learning clause 102:2:1:[46.2,58.1]:Top: p5(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54)),x0) -> p5(x0,c58) % 17.48/4.93 === Backtracking. Learning clause 104:1:0:[4.0,103.1,28.2,58.1]:: p45(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54))) -> % 17.48/4.93 === Backtracking. Learning clause 105:2:0:[27.2,58.1]:: p39(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54))) -> p39(c58) % 17.48/4.93 === Backtracking. Learning clause 106:2:1:[46.2,59.1]:Top: p5(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54)),x0) -> p5(x0,c55) % 17.48/4.93 === Backtracking. Learning clause 108:1:0:[5.0,107.1,28.2,59.1]:: p45(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54))) -> % 17.48/4.93 === Backtracking. Learning clause 109:2:0:[27.2,59.1]:: p39(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54))) -> p39(c55) % 17.48/4.93 === Backtracking. Learning clause 110:2:1:[46.2,60.1]:Top: p5(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56)),x0) -> p5(x0,c57) % 17.48/4.93 === Backtracking. Learning clause 112:1:0:[6.0,111.1,28.2,60.1]:: p45(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56))) -> % 17.48/4.93 === Backtracking. Learning clause 113:2:0:[27.2,60.1]:: p39(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56))) -> p39(c57) % 17.48/4.93 === Clause set with instances from active satisfied. Growing active. New size: 189 % 17.48/4.93 === Restarting. % 17.48/4.93 === Backtracking. Learning clause 114:3:2:[64.3,25.1]:TopTop: p6(f16(c62),x0),p6(f16(f7(c46)),x1) -> p42(x0,x1) % 17.48/4.93 === Backtracking. Learning clause 115:2:2:[43.2,7.1]:TopTop: p17(x0,x1) -> p17(x1,x0) % 17.48/4.93 === Clause set with instances from active satisfied. Growing active. New size: 253 % 17.48/4.93 === Restarting. % 17.48/4.93 === Backtracking. Learning clause 116:2:2:[52.2,15.1]:TopTop: p24(x0,x1) -> p24(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 117:2:2:[55.2,18.1]:TopTop: p19(x0,x1) -> p19(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 118:3:2:[63.1,74.1]:TopTop: p6(x0,x1),p43(f7(c55),x0) -> p43(f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59))),x1) % 17.48/4.93 === Backtracking. Learning clause 119:3:2:[63.2,74.1]:TopTop: p6(x0,x1),p43(x0,f7(c55)) -> p43(x1,f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59)))) % 17.48/4.93 === Backtracking. Learning clause 120:2:1:[45.1,74.1,91.1]:Top: p6(f7(c55),x0) -> p6(x0,f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59)))) % 17.48/4.93 === Clause set with instances from active satisfied. Growing active. New size: 321 % 17.48/4.93 === Restarting. % 17.48/4.93 === Backtracking. Learning clause 121:2:2:[53.2,16.1]:TopTop: p22(x0,x1) -> p22(x1,x0) % 17.48/4.93 === Backtracking. Learning clause 122:3:2:[64.3,75.1]:TopTop: p6(f16(c59),x0),p6(f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49)))))))))),x1) -> p42(x0,x1) % 17.48/4.93 === Backtracking. Learning clause 123:2:1:[47.1,75.1]:Top: p42(f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49)))))))))),x0) -> p42(f16(c59),x0) % 17.48/4.93 === Backtracking. Learning clause 124:2:1:[45.1,79.1,91.1]:Top: p6(f7(c57),x0) -> p6(x0,f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f36(f10(f11(f12(c49))),c60)))) % 17.48/4.93 % 17.48/4.93 SZS status Unsatisfiable % 17.48/4.93 % 17.48/4.93 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.48/4.93 % 17.48/4.93 SPASS-SCL-FOL Statistics: % 17.48/4.93 Number of learned clauses: 32 % 17.48/4.93 Number of propagations: 2722 % 17.48/4.93 Number of decisions: 1808 % 17.48/4.93 Number of resolutions: 39 % 17.48/4.93 Number of condensations: 0 % 17.48/4.93 Number of sub resolutions: 3 % 17.48/4.93 Number of input literals (deduplicated): 87 % 17.48/4.93 Number of grows: 4 % 17.48/4.93 Number of considered ground atoms: 321 % 17.48/4.93 % 17.48/4.93 Needed: 0:00:04.27 % 17.48/4.93 %------------------------------------------------------------------------------