%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN710-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 : n003.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 15.65s 3.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN710-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 : n003.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:46:57 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]
% 15.65/3.64 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.65/3.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.65/3.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.65/3.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.65/3.64 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.65/3.64 Execution resolution_2 ended with status: unsatisfiable
% 15.65/3.64 Used heuristic: resolution_2
% 15.65/3.64
% 15.65/3.64 Input Clauses:
% 15.65/3.64
% 15.65/3.64 Predicates: p10 p8 p7 p6 p4 p31 p3 p29 p28 p26 p24 p23 p21 p2 p19 p17 p15 p14 p12 p33 p34 p37 p35 p36
% 15.65/3.64 Fol Constants: c38 c39 c43 c45 c44 c40 c41 c42 c46 c47 c50 c53 c51 c55 c48 c49 c54 c52
% 15.65/3.64 Fol Functions: f5 f11 f9 f30 f18 f32 f16 f13 f27 f25 f20 f22
% 15.65/3.64 Problem Properties:
% 15.65/3.64 This is a full first-order problem without equality.
% 15.65/3.64
% 15.65/3.64 After reduction: Problem Properties:
% 15.65/3.64 This is a full first-order problem without equality.
% 15.65/3.64
% 15.65/3.64
% 15.65/3.64 Reduced Input Clauses:
% 15.65/3.64
% 15.65/3.64 Most General Atoms: p10(x1,x2) p6(x1,x2) p31(x1,x2) p29(x1,x2) p28(x1,x2) p26(x1,x2) p23(x1,x2) p21(x1,x2) p2(x1,x2) p19(x1,x2) p14(x1,x2) p12(x1,x2) p8(x2,x3) p33(x1,x3) p37(x3,x2) p36(x2,x3) p24(x2,x3) p35(x1,x3) p34(x3,x2) p7(x2,x3) p15(x2,x3) p3(x2,x3) p17(x2,x3) p4(x2,x3)
% 15.65/3.64
% 15.65/3.64 === Starting SPASS-SCL-FOL A Little Less Naive, considering 73 atoms initially, heuristics mode: resolution_2 ===
% 15.65/3.64
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 73
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 73
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 73
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 88:1:2:[52.1,3.1]:TopTop: -> p35(f30(c53,x0),f25(f27(c54,x0),x1))
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 73
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 137
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 137
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 137
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 137
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 137
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 201
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 201
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 201
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 201
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 89:3:3:[80.1,72.1]:TopTopTop: p33(f18(c51,x0),x1) -> p33(f18(c51,x0),x2),p33(f18(c51,f20(f22(c52,x1),x2)),x1)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 201
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 265
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 265
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 265
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 265
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 265
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 329
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 329
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 90:1:2:[53.1,17.1]:TopTop: -> p33(f18(c51,x0),f13(f16(c48,x0),x1))
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 329
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 91:1:2:[27.1,90.1]:TopTop: -> p36(f13(f16(c48,x0),x1),x0)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 329
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 92:3:3:[27.1,80.3]:TopTopTop: p33(f11(c46,x0),x1),p33(f18(c51,x2),x0) -> p36(x1,x2)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 330
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 93:3:2:[54.3,20.1]:TopTop: p7(c38,x0),p8(c39,x1) -> p33(x0,x1)
% 15.65/3.64 === Backtracking. Learning clause 94:2:0:[81.1,20.1]:: p33(f11(c46,c39),c39) -> p33(f32(c55,f5(c41,c42)),c39)
% 15.65/3.64 === Backtracking. Learning clause 95:1:0:[81.1,59.2,85.2,21.1]:: -> p33(f32(c55,f5(c41,c42)),c45)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 394
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 396
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 96:2:1:[87.2,22.1]:Top: p35(f30(c53,c43),f25(f27(c54,c44),x0)) -> p35(f30(c53,c43),x0)
% 15.65/3.64 === Backtracking. Learning clause 97:2:1:[32.3,22.1]:Top: p7(x0,c43),p7(x0,c44) ->
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 398
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 98:3:2:[58.1,23.1]:TopTop: p4(f5(c41,c42),x0),p3(c40,x1) -> p34(x1,x0)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 404
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 99:3:2:[54.3,24.1]:TopTop: p7(f11(c46,c39),x0),p8(f9(c47,c43),x1) -> p33(x0,x1)
% 15.65/3.64 === Backtracking. Learning clause 100:2:1:[80.1,24.1,27.1]:Top: p33(f18(c51,x0),c39) -> p36(f9(c47,c43),x0)
% 15.65/3.64 === Backtracking. Learning clause 101:2:0:[81.2,24.1]:: p33(c38,f9(c47,c43)) -> p33(f32(c55,f5(c41,c42)),f9(c47,c43))
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 412
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 102:3:0:[82.4,25.1]:: p33(c43,f9(c47,c43)),p33(c43,c50) -> p33(f11(c46,f9(c47,c43)),c50)
% 15.65/3.64 === Backtracking. Learning clause 103:3:2:[54.4,25.1]:TopTop: p7(x0,f11(c46,c50)),p8(x1,f9(c47,c43)),p33(x0,x1) ->
% 15.65/3.64 === Conflict found: 93:3:2:[54.3,20.1]:TopTop: p7(c38,x0),p8(c39,x1) -> p33(x0,x1) {x0 -> f11(c46,c50), x1 -> f9(c47,c43)}
% 15.65/3.64 === Backtracking. Learning clause 104:2:0:[93.3,25.1]:: p7(c38,f11(c46,c50)),p8(c39,f9(c47,c43)) ->
% 15.65/3.64 === Backtracking. Learning clause 105:1:0:[73.2,25.1]:: p33(f18(c51,f20(f22(c52,c50),f9(c47,c43))),f9(c47,c43)) ->
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 476
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 479
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 106:3:2:[54.3,50.1]:TopTop: p7(f11(c46,f13(f16(c48,c49),c50)),x0),p8(f9(c47,c43),x1) -> p33(x0,x1)
% 15.65/3.64 === Conflict found: 106:3:2:[54.3,50.1]:TopTop: p7(f11(c46,f13(f16(c48,c49),c50)),x0),p8(f9(c47,c43),x1) -> p33(x0,x1) {x0 -> f11(c46,c50), x1 -> f9(c47,c43)}
% 15.65/3.64 === Backtracking. Learning clause 107:1:0:[106.3,25.1,2.1]:: p7(f11(c46,f13(f16(c48,c49),c50)),f11(c46,c50)) ->
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 481
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 108:3:4:[57.2,88.1]:TopTopTopTop: p29(f30(c53,x0),x1),p24(f25(f27(c54,x0),x2),x3) -> p35(x1,x3)
% 15.65/3.64 === Backtracking. Learning clause 109:1:2:[26.1,88.1]:TopTop: -> p37(f25(f27(c54,x0),x1),x0)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 482
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 110:3:4:[56.1,91.1]:TopTopTopTop: p8(f13(f16(c48,x0),x1),x2),p15(x0,x3) -> p36(x2,x3)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 486
% 15.65/3.64 === Restarting.
% 15.65/3.64 === Backtracking. Learning clause 111:3:2:[54.3,95.1]:TopTop: p7(f32(c55,f5(c41,c42)),x0),p8(c45,x1) -> p33(x0,x1)
% 15.65/3.64 === Conflict found: 111:3:2:[54.3,95.1]:TopTop: p7(f32(c55,f5(c41,c42)),x0),p8(c45,x1) -> p33(x0,x1) {x0 -> f11(c46,c50), x1 -> f9(c47,c43)}
% 15.65/3.64 === Backtracking. Learning clause 112:2:0:[111.3,25.1]:: p7(f32(c55,f5(c41,c42)),f11(c46,c50)),p8(c45,f9(c47,c43)) ->
% 15.65/3.64 === Backtracking. Learning clause 113:1:0:[49.1,95.1]:: -> p33(c38,c45)
% 15.65/3.64 === Clause set with instances from active satisfied. Growing active. New size: 550
% 15.65/3.64
% 15.65/3.64 SZS status Unsatisfiable
% 15.65/3.64
% 15.65/3.64 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.65/3.64
% 15.65/3.64 SPASS-SCL-FOL Statistics:
% 15.65/3.64 Number of learned clauses: 26
% 15.65/3.64 Number of propagations: 5892
% 15.65/3.64 Number of decisions: 2845
% 15.65/3.64 Number of resolutions: 35
% 15.65/3.64 Number of condensations: 4
% 15.65/3.64 Number of sub resolutions: 0
% 15.65/3.64 Number of input literals (deduplicated): 73
% 15.65/3.64 Number of grows: 35
% 15.65/3.64 Number of considered ground atoms: 550
% 15.65/3.64
% 15.65/3.64 Needed: 0:00:03.10
% 15.65/3.64
%------------------------------------------------------------------------------