%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : MSC015-1.010 : TPTP v9.2.1. Released v3.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:28:56 PM UTC 2026
% Result : Unsatisfiable 7.29s 2.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MSC015-1.010 : TPTP v9.2.1. Released v3.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 : n011.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 12:42:33 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 7.29/2.01 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/2.01 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/2.01 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/2.01 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/2.01 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/2.01 Execution resolution_1 ended with status: unsatisfiable
% 7.29/2.01 Used heuristic: resolution_1
% 7.29/2.01
% 7.29/2.01 Input Clauses:
% 7.29/2.01
% 7.29/2.01 Predicates: p
% 7.29/2.01 Fol Constants: s0 s1
% 7.29/2.01 Fol Functions:
% 7.29/2.01 Problem Properties:
% 7.29/2.01 This is a Bernays Schoenfinkel problem.
% 7.29/2.01
% 7.29/2.01 After reduction: Problem Properties:
% 7.29/2.01 This is a Bernays Schoenfinkel problem.
% 7.29/2.01
% 7.29/2.01
% 7.29/2.01 Reduced Input Clauses:
% 7.29/2.01
% 7.29/2.01 Most General Atoms: p(x0,x1,x2,x3,x4,x5,x6,x7,x8,s0) p(x0,x1,x2,x3,x4,x5,x6,x7,x8,s1)
% 7.29/2.01
% 7.29/2.01 === Starting SPASS-SCL-FOL A Little Less Naive, considering 2 atoms initially, heuristics mode: resolution_1 ===
% 7.29/2.01
% 7.29/2.01 === Backtracking. Learning clause 13:1:0:[2.2,12.1]:: p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s0) ->
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 3
% 7.29/2.01 === Restarting.
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 59
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 123
% 7.29/2.01 === Backtracking. Learning clause 14:2:6:[3.1,2.2,2.1,5.1]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s0,s0) -> p(x0,x1,x2,x3,x4,x5,s1,s0,s0,s0)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 187
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 251
% 7.29/2.01 === Backtracking. Learning clause 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 315
% 7.29/2.01 === Backtracking. Learning clause 16:2:8:[3.1,2.2]:TopTopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,x7,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,x7,s1,s0)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 379
% 7.29/2.01 === Backtracking. Learning clause 17:2:8:[2.1,16.2]:TopTopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,x7,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,x7,s1,s1)
% 7.29/2.01 === Backtracking. Learning clause 18:2:2:[9.2,17.1,15.2,4.1,17.1,15.1,6.1,17.2,4.2,17.2,6.2,15.2,17.1,4.1,14.1,17.1,17.2,4.2]:TopTop: p(x0,x1,s0,s1,s1,s0,s0,s0,s1,s1) -> p(x0,x1,s1,s0,s0,s1,s1,s0,s1,s1)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 443
% 7.29/2.01 === Backtracking. Learning clause 19:2:4:[4.1,17.2,17.1,7.2,2.2,3.2]:TopTopTopTop: p(x0,x1,x2,x3,s0,s1,s1,s1,s0,s1) -> p(x0,x1,x2,x3,s1,s0,s0,s1,s1,s1)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 507
% 7.29/2.01 === Backtracking. Learning clause 20:2:5:[4.2,17.1,17.2,6.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s0,s0,s0)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 571
% 7.29/2.01 === Backtracking. Learning clause 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s1, x5 -> s1, x6 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 22:2:2:[21.2,8.1,5.2,21.2,6.2,21.1,5.1,20.1,21.1,5.1,17.1,4.1,2.1,19.1,15.1,6.1,21.1,15.1,9.1,21.1,15.1,6.1,17.1,4.1,14.1]:TopTop: p(x0,x1,s0,s0,s1,s0,s1,s1,s1,s1) -> p(x0,x1,s1,s0,s0,s1,s1,s0,s0,s0)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s1, x2 -> s1, x3 -> s1, x4 -> s0, x5 -> s1, x6 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 23:2:0:[21.1,20.2,15.1,7.1,5.2,21.2,8.2,21.1,15.2,15.1,6.1,21.2,21.1,15.1,11.1,21.1,6.2,15.1,6.1,15.2,21.2,7.2,21.1,21.2,15.1,22.2,15.2,21.2,7.2,7.1,15.2,21.1,15.1,6.1,21.1,15.1,21.2,20.2,8.1,21.1,15.1,5.2,21.2,10.2,15.2,21.2,20.2,14.2,4.2,17.2,7.2,15.2,21.2,6.1,21.1]:: p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s0) -> p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s1)
% 7.29/2.01 === Backtracking. Learning clause 24:2:5:[4.2,16.1,17.2,6.2]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s1,s1,s1) -> p(x0,x1,x2,x3,x4,s1,s0,s1,s1,s0)
% 7.29/2.01 === Backtracking. Learning clause 25:2:3:[2.1,4.2,19.1,15.1,17.2,6.1,5.2,2.2,24.2,15.2,21.1,15.1,8.1,21.1,5.1,20.1,21.1,5.1,17.1,4.1,2.1,19.1,15.1,6.1,21.1]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s1,s1,s1) -> p(x0,x1,x2,s1,s1,s1,s0,s1,s1,s1)
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 26:2:3:[15.1,21.2,24.1,2.1,5.1,17.1,4.1,2.1,19.1,15.1,6.1,21.1,15.1,8.1,21.1,5.1,20.1,21.1,5.1,17.1,4.1,2.1,19.1]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s1,s0,s0,s1,s1,s1)
% 7.29/2.01 === Conflict found: 14:2:6:[3.1,2.2,2.1,5.1]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s0,s0) -> p(x0,x1,x2,x3,x4,x5,s1,s0,s0,s0) {x0 -> s0, x1 -> s1, x2 -> s1, x3 -> s0, x4 -> s0, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 27:2:2:[14.1,4.2,21.1,17.2,9.2,24.1]:TopTop: p(x0,x1,s0,s1,s1,s1,s1,s1,s1,s1) -> p(x0,x1,s1,s0,s0,s1,s0,s1,s1,s0)
% 7.29/2.01 === Backtracking. Learning clause 28:2:2:[9.1,15.2,17.1]:TopTop: p(x0,x1,s0,s1,s1,s1,s0,s1,s1,s1) -> p(x0,x1,s1,s0,s0,s0,s0,s0,s1,s1)
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 29:2:3:[15.1,21.2,24.1,2.1,5.1,17.1,4.1,2.1,19.1,15.1,6.1,21.1,15.1,8.1,21.1,5.1,20.1,21.1,5.1,17.1,4.1,2.1]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s0,s1,s1,s1,s0,s1)
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 30:2:3:[15.1,21.2,24.1,2.1,5.1,17.1,4.1,2.1,19.1,15.1,6.1,21.1,15.1,8.1,21.1,5.1]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s0,s0,s1,s0,s0,s0)
% 7.29/2.01 === Conflict found: 28:2:2:[9.1,15.2,17.1]:TopTop: p(x0,x1,s0,s1,s1,s1,s0,s1,s1,s1) -> p(x0,x1,s1,s0,s0,s0,s0,s0,s1,s1) {x0 -> s0, x1 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 31:2:2:[28.1,25.2,4.1,14.1,21.1]:TopTop: p(x0,x1,s0,s0,s0,s0,s0,s1,s1,s1) -> p(x0,x1,s1,s0,s0,s0,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s1, x3 -> s1, x4 -> s1, x5 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 32:2:1:[15.2,10.1,25.2,21.1,31.1,21.2,9.2,15.2]:Top: p(x0,s0,s0,s1,s1,s1,s0,s1,s1,s1) -> p(x0,s1,s1,s0,s0,s0,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 17:2:8:[2.1,16.2]:TopTopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,x7,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,x7,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s1, x3 -> s0, x4 -> s1, x5 -> s1, x6 -> s1, x7 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 33:2:5:[17.1,5.2,4.1,21.2,6.2,16.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s1,s1,s1) -> p(x0,x1,x2,x3,x4,s1,s1,s1,s1,s0)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s1, x6 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 34:2:1:[21.1,6.2,32.1,15.2]:Top: p(x0,s0,s0,s1,s1,s0,s0,s1,s1,s1) -> p(x0,s1,s1,s0,s0,s0,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s0, x6 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 35:1:0:[21.1,1.1,15.1,24.1,2.1,5.1]:: -> p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s0)
% 7.29/2.01 === Conflict found: 19:2:4:[4.1,17.2,17.1,7.2,2.2,3.2]:TopTopTopTop: p(x0,x1,x2,x3,s0,s1,s1,s1,s0,s1) -> p(x0,x1,x2,x3,s1,s0,s0,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 36:2:1:[19.2,34.1,2.2,4.2,17.2,5.2,21.2,20.2]:Top: p(x0,s0,s0,s1,s0,s0,s1,s0,s0,s0) -> p(x0,s1,s1,s0,s0,s0,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s0, x6 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 37:1:0:[21.1,1.1,15.1,24.1,2.1]:: -> p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s1)
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s1, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 38:2:1:[15.1,19.2,6.1,2.2,4.2,17.2,21.1,15.1,8.1,21.1,5.1,36.1]:Top: p(x0,s0,s0,s0,s0,s1,s1,s0,s0,s0) -> p(x0,s1,s1,s0,s0,s0,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s0, x6 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 39:1:0:[21.1,1.1]:: -> p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s1)
% 7.29/2.01 === Conflict found: 38:2:1:[15.1,19.2,6.1,2.2,4.2,17.2,21.1,15.1,8.1,21.1,5.1,36.1]:Top: p(x0,s0,s0,s0,s0,s1,s1,s0,s0,s0) -> p(x0,s1,s1,s0,s0,s0,s1,s1,s1,s1) {x0 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 40:1:0:[38.1,35.1]:: -> p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 16:2:8:[3.1,2.2]:TopTopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,x7,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,x7,s1,s0) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s0, x5 -> s0, x6 -> s1, x7 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 41:2:3:[16.1,30.2]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s0,s0,s1,s0,s1,s0)
% 7.29/2.01 === Conflict found: 17:2:8:[2.1,16.2]:TopTopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,x7,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,x7,s1,s1) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s0, x6 -> s0, x7 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 42:2:4:[17.1,7.2,4.1,16.1,2.2]:TopTopTopTop: p(x0,x1,x2,x3,s0,s1,s1,s1,s1,s0) -> p(x0,x1,x2,x3,s1,s0,s0,s1,s1,s0)
% 7.29/2.01 === Backtracking. Learning clause 43:2:4:[7.1,15.2,17.1]:TopTopTopTop: p(x0,x1,x2,x3,s0,s1,s0,s1,s1,s1) -> p(x0,x1,x2,x3,s1,s0,s0,s0,s1,s1)
% 7.29/2.01 === Backtracking. Learning clause 44:2:7:[4.1,17.2]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s0,s0)
% 7.29/2.01 === Backtracking. Learning clause 45:2:1:[2.2,10.1]:Top: p(x0,s0,s1,s1,s1,s1,s1,s1,s1,s0) -> p(x0,s1,s0,s0,s0,s0,s0,s0,s0,s0)
% 7.29/2.01 === Conflict found: 20:2:5:[4.2,17.1,17.2,6.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s0,s0,s0) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 46:2:5:[20.1,14.2,2.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s0,s1,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s0,s0,s1)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 635
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s1, x1 -> s0, x2 -> s1, x3 -> s0, x4 -> s1, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 47:2:5:[15.1,21.2,6.1,21.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s0,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s1,s1,s1)
% 7.29/2.01 === Conflict found: 33:2:5:[17.1,5.2,4.1,21.2,6.2,16.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s1,s1,s1) -> p(x0,x1,x2,x3,x4,s1,s1,s1,s1,s0) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 48:2:4:[33.1,21.2,42.1]:TopTopTopTop: p(x0,x1,x2,x3,s0,s0,s1,s0,s0,s0) -> p(x0,x1,x2,x3,s1,s0,s0,s1,s1,s0)
% 7.29/2.01 === Backtracking. Learning clause 49:2:1:[10.1,15.2,30.1,25.2,48.1]:Top: p(x0,s0,s1,s0,s0,s0,s0,s1,s1,s1) -> p(x0,s1,s0,s1,s1,s0,s0,s1,s1,s0)
% 7.29/2.01 === Backtracking. Learning clause 50:2:3:[8.2,44.1,15.2]:TopTopTop: p(x0,x1,x2,s0,s1,s1,s0,s1,s1,s1) -> p(x0,x1,x2,s1,s0,s0,s0,s1,s0,s0)
% 7.29/2.01 === Backtracking. Learning clause 51:2:1:[9.2,21.1,15.2,49.1,25.2]:Top: p(x0,s0,s0,s0,s0,s0,s0,s1,s1,s1) -> p(x0,s1,s0,s1,s1,s0,s0,s1,s1,s0)
% 7.29/2.01 === Conflict found: 16:2:8:[3.1,2.2]:TopTopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,x7,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,x7,s1,s0) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s1, x6 -> s1, x7 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 52:2:6:[16.1,5.2,2.1]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s0,s1,s1)
% 7.29/2.01 === Backtracking. Learning clause 53:2:2:[6.1,31.2]:TopTop: p(x0,x1,s0,s0,s0,s0,s0,s1,s1,s1) -> p(x0,x1,s1,s0,s0,s1,s0,s0,s0,s0)
% 7.29/2.01 === Conflict found: 44:2:7:[4.1,17.2]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s0,s0) {x0 -> s1, x1 -> s0, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s1, x6 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 54:2:5:[44.1,6.2]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s1,s1,s1) -> p(x0,x1,x2,x3,x4,s1,s0,s1,s0,s0)
% 7.29/2.01 === Conflict found: 51:2:1:[9.2,21.1,15.2,49.1,25.2]:Top: p(x0,s0,s0,s0,s0,s0,s0,s1,s1,s1) -> p(x0,s1,s0,s1,s1,s0,s0,s1,s1,s0) {x0 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 55:1:0:[51.1,39.1]:: -> p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s0)
% 7.29/2.01 === Conflict found: 47:2:5:[15.1,21.2,6.1,21.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s0,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s1,s1,s1) {x0 -> s0, x1 -> s1, x2 -> s1, x3 -> s1, x4 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 56:2:0:[47.1,8.2,15.1,15.2,7.1,47.1,15.1,47.2,11.1,7.2,21.2,41.1,22.2,15.2,21.2,7.2,15.2,47.2]:: p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s0) -> p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s0)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s0, x4 -> s1, x5 -> s1, x6 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 57:2:3:[21.1,14.2,8.1,44.1,16.1]:TopTopTop: p(x0,x1,x2,s0,s1,s1,s0,s1,s0,s0) -> p(x0,x1,x2,s1,s0,s0,s0,s1,s1,s0)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 699
% 7.29/2.01 === Conflict found: 44:2:7:[4.1,17.2]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s0,s0) {x0 -> s1, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s1, x5 -> s1, x6 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 58:2:6:[44.1,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s0,s0)
% 7.29/2.01 === Conflict found: 14:2:6:[3.1,2.2,2.1,5.1]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s0,s0) -> p(x0,x1,x2,x3,x4,x5,s1,s0,s0,s0) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s0, x4 -> s1, x5 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 59:2:5:[14.1,54.2,21.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s1,s1,s1,s1) -> p(x0,x1,x2,x3,x4,s1,s1,s1,s1,s1)
% 7.29/2.01 === Backtracking. Learning clause 60:2:1:[10.2,47.1,15.2,25.2,15.1,7.1,21.1,15.1,21.2,9.2,15.2,59.1,25.2]:Top: p(x0,s0,s0,s0,s0,s0,s0,s1,s1,s1) -> p(x0,s1,s0,s0,s1,s1,s1,s1,s1,s1)
% 7.29/2.01 === Conflict found: 47:2:5:[15.1,21.2,6.1,21.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s0,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s1,s1,s1) {x0 -> s1, x1 -> s0, x2 -> s0, x3 -> s0, x4 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 61:2:3:[47.1,7.2,15.1,59.2,8.1,47.1,15.2,5.1,21.2]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s0,s1,s1,s0,s0,s0)
% 7.29/2.01 === Backtracking. Learning clause 62:2:1:[8.1,60.2]:Top: p(x0,s0,s0,s0,s0,s0,s0,s1,s1,s1) -> p(x0,s1,s0,s1,s0,s0,s0,s0,s0,s0)
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s1, x1 -> s1, x2 -> s0, x3 -> s0, x4 -> s0, x5 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 63:2:1:[15.1,47.2,7.1,21.1,45.2,33.2,15.2,15.1]:Top: p(x0,s0,s1,s1,s1,s0,s0,s1,s1,s1) -> p(x0,s1,s0,s0,s1,s0,s1,s1,s1,s1)
% 7.29/2.01 === Clause set with instances from active satisfied. Growing active. New size: 763
% 7.29/2.01 === Conflict found: 15:2:6:[2.1,3.2,4.1,2.1,3.1,2.1,2.2,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s1,s1) {x0 -> s1, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 64:2:3:[15.1,26.2,6.1]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s1,s1,s0,s0,s0,s0)
% 7.29/2.01 === Conflict found: 21:2:7:[4.1,17.2,17.1]:TopTopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,x6,s0,s0,s0) -> p(x0,x1,x2,x3,x4,x5,x6,s1,s1,s1) {x0 -> s1, x1 -> s0, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s1, x6 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 65:2:2:[21.1,14.2,9.1,21.1]:TopTop: p(x0,x1,s0,s1,s1,s1,s0,s1,s0,s0) -> p(x0,x1,s1,s0,s0,s0,s0,s1,s1,s1)
% 7.29/2.01 === Backtracking. Learning clause 66:2:6:[2.1,58.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s0,s1)
% 7.29/2.01 === Backtracking. Learning clause 67:2:4:[4.1,43.2]:TopTopTopTop: p(x0,x1,x2,x3,s0,s1,s0,s1,s1,s1) -> p(x0,x1,x2,x3,s1,s0,s0,s1,s0,s0)
% 7.29/2.01 === Conflict found: 47:2:5:[15.1,21.2,6.1,21.1]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s0,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s0,s1,s1,s1) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> s1, x4 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 68:2:4:[47.2,5.1,7.2,59.2,21.2]:TopTopTopTop: p(x0,x1,x2,x3,s0,s0,s1,s0,s0,s0) -> p(x0,x1,x2,x3,s1,s1,s1,s0,s0,s0)
% 7.29/2.01 === Conflict found: 14:2:6:[3.1,2.2,2.1,5.1]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s0,s0) -> p(x0,x1,x2,x3,x4,x5,s1,s0,s0,s0) {x0 -> s1, x1 -> s0, x2 -> s0, x3 -> s1, x4 -> s1, x5 -> s0}
% 7.29/2.01 === Backtracking. Learning clause 69:2:4:[14.1,67.2,16.1]:TopTopTopTop: p(x0,x1,x2,x3,s0,s1,s0,s1,s1,s1) -> p(x0,x1,x2,x3,s1,s0,s1,s0,s1,s0)
% 7.29/2.01 === Conflict found: 58:2:6:[44.1,5.2]:TopTopTopTopTopTop: p(x0,x1,x2,x3,x4,x5,s0,s1,s1,s1) -> p(x0,x1,x2,x3,x4,x5,s1,s1,s0,s0) {x0 -> s1, x1 -> s0, x2 -> s1, x3 -> s0, x4 -> s0, x5 -> s1}
% 7.29/2.01 === Backtracking. Learning clause 70:2:5:[58.1,47.2]:TopTopTopTopTop: p(x0,x1,x2,x3,x4,s0,s0,s0,s0,s0) -> p(x0,x1,x2,x3,x4,s1,s1,s1,s0,s0)
% 7.29/2.01 === Conflict found: 64:2:3:[15.1,26.2,6.1]:TopTopTop: p(x0,x1,x2,s0,s0,s0,s0,s0,s0,s0) -> p(x0,x1,x2,s1,s1,s1,s0,s0,s0,s0) {x0 -> s1, x1 -> s1, x2 -> s1}
% 7.29/2.01
% 7.29/2.01 SZS status Unsatisfiable
% 7.29/2.01
% 7.29/2.01 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/2.01
% 7.29/2.01 SPASS-SCL-FOL Statistics:
% 7.29/2.01 Number of learned clauses: 58
% 7.29/2.01 Number of propagations: 12429
% 7.29/2.01 Number of decisions: 628
% 7.29/2.01 Number of resolutions: 384
% 7.29/2.01 Number of condensations: 0
% 7.29/2.01 Number of sub resolutions: 0
% 7.29/2.01 Number of input literals (deduplicated): 22
% 7.29/2.01 Number of grows: 13
% 7.29/2.01 Number of considered ground atoms: 763
% 7.29/2.01
% 7.29/2.01 Needed: 0:00:01.47
% 7.29/2.01
%------------------------------------------------------------------------------