%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SWB030+2 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:35:48 PM UTC 2026
% Result : Unsatisfiable 0.42s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : SWB030+2 : TPTP v9.2.1. Released v5.2.0.
% 0.13/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.36 % Computer : n026.cluster.edu
% 0.18/0.36 % Model : x86_64 x86_64
% 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.36 % Memory : 8042.1875MB
% 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.36 % CPULimit : 300
% 0.18/0.36 % WCLimit : 300
% 0.18/0.36 % DateTime : Thu May 7 13:20:39 EDT 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 SPASS-SCL-FOL version:
% 0.14/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.63 Execution resolution_2 ended with status: unsatisfiable
% 0.42/0.63 Used heuristic: resolution_2
% 0.42/0.63
% 0.42/0.63 Input Clauses:
% 0.42/0.63
% 0.42/0.63 Predicates: iext icext ic ren1 ren2 ren3
% 0.42/0.63 Fol Constants: uri_rdf_type uri_owl_hasSelf uri_owl_onProperty uri_owl_complementOf uri_ex_c uri_owl_Class uri_owl_Restriction dat_str_true uri_xsd_boolean skc1
% 0.42/0.63 Fol Functions: literal_typed
% 0.42/0.63 Problem Properties:
% 0.42/0.63 This is a full first-order problem without equality.
% 0.42/0.63
% 0.42/0.63 After reduction: Problem Properties:
% 0.42/0.63 This is a full first-order problem without equality.
% 0.42/0.63
% 0.42/0.63
% 0.42/0.63 Reduced Input Clauses:
% 0.42/0.63
% 0.42/0.63 Most General Atoms: iext(uri_rdf_type,x1,x0) iext(x2,x1,x1) iext(uri_owl_hasSelf,x0,x1) iext(uri_owl_onProperty,x0,x2) ren1(x0,x3,x2) icext(x2,x1) ren3(x0,x1) ic(x1) ren2(x0,x2,x1) iext(uri_owl_complementOf,x0,x1)
% 0.42/0.63
% 0.42/0.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 45 atoms initially, heuristics mode: resolution_2 ===
% 0.42/0.63
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 46
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 21:1:0:[1.1,16.1]:: -> icext(uri_owl_Class,uri_ex_c)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 47
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 22:1:0:[15.1,17.1]:: -> ren3(uri_ex_c,skc1)
% 0.42/0.63 === Backtracking. Learning clause 23:3:2:[2.2,5.2]:TopTop: icext(x0,x0),icext(x1,x0) -> ren1(x1,x0,uri_rdf_type)
% 0.42/0.63 === Backtracking. Learning clause 24:1:1:[1.1,6.2,23.1]:Top: -> ren1(x0,x0,uri_rdf_type)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 48
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 25:1:0:[1.1,18.1]:: -> icext(uri_owl_Restriction,skc1)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 50
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 26:2:2:[7.2,19.1]:TopTop: iext(uri_owl_hasSelf,skc1,x0) -> ren1(skc1,x1,uri_rdf_type)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.42/0.63 === Backtracking. Learning clause 27:3:3:[1.2,11.1]:TopTopTop: iext(uri_rdf_type,x0,x1) -> icext(x2,x0),ren2(x2,x0,x1)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Conflict found: 26:2:2:[7.2,19.1]:TopTop: iext(uri_owl_hasSelf,skc1,x0) -> ren1(skc1,x1,uri_rdf_type) {x0 -> literal_typed(dat_str_true,uri_xsd_boolean), x1 -> uri_rdf_type}
% 0.42/0.63 === Backtracking. Learning clause 28:1:1:[26.1,20.1]:Top: -> ren1(skc1,x0,uri_rdf_type)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 119
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 29:2:1:[8.2,21.1]:Top: ren2(uri_owl_Class,uri_ex_c,x0),icext(x0,uri_ex_c) ->
% 0.42/0.63 === Backtracking. Learning clause 30:2:1:[3.2,21.1]:Top: ren1(uri_owl_Class,uri_ex_c,x0) -> iext(x0,uri_ex_c,uri_ex_c)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 119
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 31:1:1:[14.1,22.1]:Top: -> ren2(uri_ex_c,x0,skc1)
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 119
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Conflict found: 29:2:1:[8.2,21.1]:Top: ren2(uri_owl_Class,uri_ex_c,x0),icext(x0,uri_ex_c) -> {x0 -> uri_owl_Class}
% 0.42/0.63 === Backtracking. Learning clause 32:1:0:[29.2,21.1]:: ren2(uri_owl_Class,uri_ex_c,uri_owl_Class) ->
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 183
% 0.42/0.63 === Backtracking. Learning clause 33:3:3:[14.2,8.1]:TopTopTop: ren3(x0,x1),icext(x0,x2),icext(x1,x2) ->
% 0.42/0.63 === Conflict found: 33:3:3:[14.2,8.1]:TopTopTop: ren3(x0,x1),icext(x0,x2),icext(x1,x2) -> {x0 -> uri_ex_c, x1 -> skc1, x2 -> uri_ex_c}
% 0.42/0.63 === Backtracking. Learning clause 34:5:5:[33.2,4.3,4.3]:TopTopTopTopTop: ren3(x0,x1),ren1(x0,x2,x3),iext(x3,x2,x2),ren1(x1,x2,x4),iext(x4,x2,x2) ->
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 188
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Conflict found: 33:3:3:[14.2,8.1]:TopTopTop: ren3(x0,x1),icext(x0,x2),icext(x1,x2) -> {x0 -> uri_rdf_type, x1 -> uri_owl_Restriction, x2 -> skc1}
% 0.42/0.63 === Backtracking. Learning clause 35:2:1:[33.3,25.1]:Top: ren3(x0,uri_owl_Restriction),icext(x0,skc1) ->
% 0.42/0.63 === Backtracking. Learning clause 36:2:1:[8.3,25.1]:Top: ren2(x0,skc1,uri_owl_Restriction),icext(x0,skc1) ->
% 0.42/0.63 === Backtracking. Learning clause 37:2:1:[5.1,25.1]:Top: iext(x0,skc1,skc1) -> ren1(uri_owl_Restriction,skc1,x0)
% 0.42/0.63 === Backtracking. Learning clause 38:3:2:[4.1,28.1,33.3,1.2]:TopTop: iext(uri_rdf_type,x0,x0),ren3(x1,skc1),iext(uri_rdf_type,x0,x1) ->
% 0.42/0.63 === Conflict found: 33:3:3:[14.2,8.1]:TopTopTop: ren3(x0,x1),icext(x0,x2),icext(x1,x2) -> {x0 -> uri_ex_c, x1 -> skc1, x2 -> uri_ex_c}
% 0.42/0.63 === Backtracking. Learning clause 39:2:1:[33.1,22.1,4.3,28.1,1.2]:Top: iext(uri_rdf_type,x0,x0),iext(uri_rdf_type,x0,uri_ex_c) ->
% 0.42/0.63 === Clause set with instances from active satisfied. Growing active. New size: 188
% 0.42/0.63 === Restarting.
% 0.42/0.63 === Backtracking. Learning clause 40:2:1:[9.1,31.1]:Top: -> icext(skc1,x0),icext(uri_ex_c,x0)
% 0.42/0.63
% 0.42/0.63 SZS status Unsatisfiable
% 0.42/0.63
% 0.42/0.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.63
% 0.42/0.63 SPASS-SCL-FOL Statistics:
% 0.42/0.63 Number of learned clauses: 20
% 0.42/0.63 Number of propagations: 868
% 0.42/0.63 Number of decisions: 506
% 0.42/0.63 Number of resolutions: 31
% 0.42/0.63 Number of condensations: 0
% 0.42/0.63 Number of sub resolutions: 0
% 0.42/0.63 Number of input literals (deduplicated): 15
% 0.42/0.63 Number of grows: 12
% 0.42/0.63 Number of considered ground atoms: 188
% 0.42/0.63
% 0.42/0.63 Needed: 0:00:00.03
% 0.42/0.63
%------------------------------------------------------------------------------