%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SWB004+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 : 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:35:41 PM UTC 2026
% Result : Theorem 3.73s 1.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWB004+2 : TPTP v9.2.1. Released v5.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n011.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:19:33 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 3.73/1.27 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.27 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.27 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.27 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.27 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.27 Execution resolution_1 ended with status: unsatisfiable
% 3.73/1.27 Used heuristic: resolution_1
% 3.73/1.27
% 3.73/1.27 Input Clauses:
% 3.73/1.27
% 3.73/1.27 Predicates: ir iext icext idc ic ren1 ren2
% 3.73/1.27 Fol Constants: uri_rdf_type uri_owl_Class uri_rdfs_Class uri_rdfs_Datatype uri_owl_Thing uri_rdfs_subClassOf uri_owl_equivalentClass
% 3.73/1.27 Fol Functions: skf1 skf2
% 3.73/1.27 Problem Properties:
% 3.73/1.27 This is a full first-order problem without equality.
% 3.73/1.27
% 3.73/1.27 After reduction: Problem Properties:
% 3.73/1.27 This is a full first-order problem without equality.
% 3.73/1.27
% 3.73/1.27
% 3.73/1.27 Reduced Input Clauses:
% 3.73/1.27 33:1:1:[1.0,16.0]:Top: -> icext(uri_owl_Thing,x0)
% 3.73/1.27
% 3.73/1.27 Most General Atoms: ir(x0) iext(uri_rdf_type,x1,x0) idc(x0) icext(x2,x1) iext(uri_rdfs_subClassOf,x0,x1) ic(x1) ren1(x0,x2,x1) iext(uri_owl_equivalentClass,x0,x1) ren2(x0,x2,x1)
% 3.73/1.27
% 3.73/1.27 === Starting SPASS-SCL-FOL A Little Less Naive, considering 15 atoms initially, heuristics mode: resolution_1 ===
% 3.73/1.27
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 79
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 143
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 207
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 271
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 335
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 399
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 463
% 3.73/1.27 === Backtracking. Learning clause 34:3:3:[27.2,3.1]:TopTopTop: -> icext(x0,x1),ren2(x0,x1,x2),iext(uri_rdf_type,x1,x2)
% 3.73/1.27 === Backtracking. Learning clause 35:4:3:[4.1,12.2,7.1,24.3,26.1,24.3]:TopTopTop: ren2(x0,x1,uri_rdfs_Datatype),ren2(x2,x1,x0),icext(x2,x1) -> ren2(uri_owl_Class,x1,x0)
% 3.73/1.27 === Backtracking. Learning clause 36:3:3:[24.2,27.2,3.1]:TopTopTop: ren2(x0,x1,x2) -> ren2(x2,x1,x0),iext(uri_rdf_type,x1,x2)
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 527
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 591
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 655
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 719
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 783
% 3.73/1.27 === Backtracking. Learning clause 37:2:2:[7.2,19.1]:TopTop: ic(x0) -> ren1(x1,x0,uri_owl_Class)
% 3.73/1.27 === Backtracking. Learning clause 38:1:2:[27.1,26.1]:TopTop: -> ren2(x0,x1,x0)
% 3.73/1.27 === Backtracking. Learning clause 40:4:3:[38.0,39.1,6.2,10.1,25.3,35.4,26.2,25.3]:TopTopTop: ren2(x0,x1,uri_rdfs_Datatype),ren2(x0,x1,x2),icext(x2,x1) -> ren2(x0,x1,uri_rdfs_Class)
% 3.73/1.27 === Backtracking. Learning clause 41:2:3:[9.2,37.1,18.1]:TopTopTop: -> ren1(x0,x1,uri_owl_Class),ren1(uri_rdfs_Class,x1,x2)
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 847
% 3.73/1.27 === Backtracking. Learning clause 42:2:1:[31.3,38.1]:Top: ic(x0) -> iext(uri_owl_equivalentClass,x0,x0)
% 3.73/1.27 === Backtracking. Learning clause 43:2:3:[6.1,18.1,37.1]:TopTopTop: -> ren1(uri_owl_Class,x0,x1),ren1(x2,x0,uri_owl_Class)
% 3.73/1.27 === Conflict found: 35:4:3:[4.1,12.2,7.1,24.3,26.1,24.3]:TopTopTop: ren2(x0,x1,uri_rdfs_Datatype),ren2(x2,x1,x0),icext(x2,x1) -> ren2(uri_owl_Class,x1,x0) {x0 -> uri_rdfs_Datatype, x1 -> skf1(uri_rdfs_Class,uri_rdf_type), x2 -> uri_rdfs_Datatype}
% 3.73/1.27 === Backtracking. Learning clause 45:3:2:[38.0,44.1,35.4,25.1,27.2,6.1,9.1]:TopTop: ren2(x0,x1,uri_rdfs_Datatype) -> ren2(uri_rdfs_Class,x1,x0),ic(x1)
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 911
% 3.73/1.27 === Backtracking. Learning clause 46:2:1:[26.1,33.1,7.2,9.2]:Top: icext(uri_rdfs_Class,x0) -> ren2(uri_owl_Thing,x0,uri_owl_Class)
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 975
% 3.73/1.27 === Clause set with instances from active satisfied. Growing active. New size: 1039
% 3.73/1.27 === Backtracking. Learning clause 47:2:2:[9.1,18.1]:TopTop: -> ic(x0),ren1(uri_rdfs_Class,x0,x1)
% 3.73/1.27 === Backtracking. Learning clause 48:2:1:[26.1,13.2,7.2,4.2]:Top: idc(x0) -> ren2(uri_rdfs_Datatype,x0,uri_owl_Class)
% 3.73/1.27 === Backtracking. Learning clause 49:2:1:[26.2,10.2,7.2]:Top: ic(x0) -> ren2(uri_owl_Class,x0,uri_rdfs_Class)
% 3.73/1.27 === Backtracking. Learning clause 50:1:0:[10.1,14.1,3.1]:: -> iext(uri_rdf_type,uri_owl_Thing,uri_rdfs_Class)
% 3.73/1.27 === Conflict found: 35:4:3:[4.1,12.2,7.1,24.3,26.1,24.3]:TopTopTop: ren2(x0,x1,uri_rdfs_Datatype),ren2(x2,x1,x0),icext(x2,x1) -> ren2(uri_owl_Class,x1,x0) {x0 -> uri_rdfs_Datatype, x1 -> skf1(uri_rdfs_Datatype,uri_owl_Class), x2 -> uri_rdfs_Datatype}
% 3.73/1.27 === Backtracking. Learning clause 54:5:0:[11.0,51.1,20.1,52.5,8.0,53.6,35.4,25.1,18.1,19.1,23.3,32.5,31.4]:: ren2(uri_rdfs_Datatype,skf1(uri_rdfs_Datatype,uri_owl_Class),uri_rdfs_Datatype),iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing),iext(uri_rdf_type,uri_owl_Class,uri_owl_Class),iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing),ren2(uri_owl_Class,skf2(uri_owl_Class,uri_rdfs_Class),uri_rdfs_Class) ->
% 3.73/1.27
% 3.73/1.27 SZS status Unsatisfiable
% 3.73/1.27
% 3.73/1.27 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.27
% 3.73/1.27 SPASS-SCL-FOL Statistics:
% 3.73/1.27 Number of learned clauses: 16
% 3.73/1.27 Number of propagations: 7453
% 3.73/1.27 Number of decisions: 866
% 3.73/1.27 Number of resolutions: 55
% 3.73/1.27 Number of condensations: 0
% 3.73/1.27 Number of sub resolutions: 6
% 3.73/1.27 Number of input literals (deduplicated): 24
% 3.73/1.27 Number of grows: 16
% 3.73/1.27 Number of considered ground atoms: 1039
% 3.73/1.27
% 3.73/1.27 Needed: 0:00:00.74
% 3.73/1.27
%------------------------------------------------------------------------------