%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWB004+4 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/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:35:42 PM UTC 2026 % Result : CounterSatisfiable 125.80s 25.66s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWB004+4 : TPTP v9.2.1. Released v5.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.34 % Computer : n007.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:19:09 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] % 125.80/25.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 125.80/25.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 125.80/25.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 125.80/25.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 125.80/25.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 125.80/25.66 Execution lmodel_grow ended with status: satisfiable % 125.80/25.66 Used heuristic: lmodel_grow % 125.80/25.66 % 125.80/25.66 Input Clauses: % 125.80/25.66 % 125.80/25.66 Predicates: iext ip ir lv icext ic ren1 ren2 % 125.80/25.66 Fol Constants: uri_rdf_type uri_rdf_first uri_rdf_Property uri_rdf_nil uri_rdf_List uri_rdf_rest uri_rdf__1 uri_rdf__2 uri_rdf__3 uri_rdf_object uri_rdf_value uri_rdf_subject uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource uri_rdfs_range uri_rdfs_Literal uri_rdfs_isDefinedBy uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_label uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container uri_rdf_Bag uri_rdfs_ContainerMembershipProperty uri_rdfs_member uri_rdfs_Seq uri_rdf_XMLLiteral uri_rdfs_Datatype uri_rdfs_Class uri_rdfs_Statement uri_rdf_predicate uri_owl_Class uri_owl_Thing uri_owl_equivalentClass % 125.80/25.66 Fol Functions: % 125.80/25.66 Problem Properties: % 125.80/25.66 This is a Bernays Schoenfinkel problem. % 125.80/25.66 % 125.80/25.66 After reduction: Problem Properties: % 125.80/25.66 This is a Bernays Schoenfinkel problem. % 125.80/25.66 % 125.80/25.66 % 125.80/25.66 Reduced Input Clauses: % 125.80/25.66 93:1:1:[2.0,58.0]:Top: -> icext(uri_rdfs_Resource,x0) % 125.80/25.66 % 125.80/25.66 Most General Atoms: ir(x0) lv(x0) ren1(x0,x1) ic(x1) icext(x0,x2) ren2(x0,x1) ip(x1) iext(x1,x2,x3) % 125.80/25.66 % 125.80/25.66 === Starting SPASS-SCL-FOL A Little Less Naive, considering 88 atoms initially, heuristics mode: lmodel_grow === % 125.80/25.66 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 106 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 124 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 140 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 160 % 125.80/25.66 === Backtracking. Learning clause 94:3:3:[27.2,64.2]:TopTopTop: icext(x0,x1),iext(uri_rdfs_range,uri_rdf_type,x2) -> icext(x2,x0) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 177 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 194 % 125.80/25.66 === Backtracking. Learning clause 95:2:2:[84.2,82.1]:TopTop: iext(uri_rdfs_subPropertyOf,x0,x1) -> ip(x1) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 211 % 125.80/25.66 === Backtracking. Learning clause 96:3:3:[57.1,64.3,78.1]:TopTopTop: iext(uri_rdfs_range,x0,uri_rdfs_Class),iext(x0,x1,x2) -> iext(uri_rdfs_subClassOf,x2,x2) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 232 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 250 % 125.80/25.66 === Backtracking. Learning clause 97:3:3:[57.1,64.3]:TopTopTop: iext(uri_rdfs_range,x0,uri_rdfs_Class),iext(x0,x1,x2) -> ic(x2) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 271 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 290 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 309 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 326 % 125.80/25.66 === Backtracking. Learning clause 98:4:3:[51.2,79.2,75.3]:TopTopTop: iext(uri_rdfs_subClassOf,x0,x1),ren1(x2,uri_rdfs_Datatype),icext(x2,x1) -> iext(uri_rdfs_subClassOf,x0,uri_rdfs_Literal) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 346 % 125.80/25.66 === Backtracking. Learning clause 99:3:3:[83.3,26.1]:TopTopTop: ren2(x0,uri_rdf_type),iext(x0,x1,x2) -> icext(x2,x1) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 368 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 387 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 409 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 426 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 437 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 450 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 461 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 476 % 125.80/25.66 === Backtracking. Learning clause 100:3:3:[75.1,76.2]:TopTopTop: icext(x0,x1),iext(uri_rdfs_subClassOf,x0,x2) -> icext(x2,x1) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 494 % 125.80/25.66 === Backtracking. Learning clause 101:3:2:[84.2,81.1,35.2,75.3]:TopTop: ren1(x0,uri_rdfs_ContainerMembershipProperty),icext(x0,x1) -> ip(x1) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 519 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 541 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 561 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 579 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 598 % 125.80/25.66 === Backtracking. Learning clause 102:4:5:[83.3,83.2]:TopTopTopTopTop: ren2(x0,x1),iext(x0,x2,x3),ren2(x1,x4) -> iext(x4,x2,x3) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 613 % 125.80/25.66 === Backtracking. Learning clause 103:3:3:[27.1,100.3]:TopTopTop: icext(x0,x1),iext(uri_rdfs_subClassOf,x0,x2) -> iext(uri_rdf_type,x1,x2) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 633 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 645 % 125.80/25.66 === Backtracking. Learning clause 104:2:2:[84.2,81.1]:TopTop: iext(uri_rdfs_subPropertyOf,x0,x1) -> ip(x0) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 663 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 677 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 693 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 705 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 719 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 731 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 742 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 755 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 764 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 774 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 786 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 793 % 125.80/25.66 === Backtracking. Learning clause 105:6:7:[83.3,54.2,84.2,87.3,103.1]:TopTopTopTopTopTopTop: iext(x0,x1,x2),iext(uri_rdfs_domain,x3,x4),iext(uri_rdfs_subPropertyOf,x0,x5),iext(uri_rdfs_subPropertyOf,x5,x3),iext(uri_rdfs_subClassOf,x4,x6) -> iext(uri_rdf_type,x1,x6) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 810 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 825 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 844 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 857 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 874 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 887 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 896 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 909 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 921 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 929 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 936 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 947 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 954 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 960 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 965 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 971 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 976 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 983 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 996 % 125.80/25.66 === Backtracking. Learning clause 106:2:2:[75.2,93.1]:TopTop: ren1(uri_rdfs_Resource,x0) -> icext(x0,x1) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1008 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1019 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1027 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1035 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1044 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1051 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1057 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1064 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1071 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1086 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1097 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1103 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1114 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1121 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1126 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1131 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1137 % 125.80/25.66 === Backtracking. Learning clause 107:6:6:[13.1,105.6,86.1]:TopTopTopTopTopTop: iext(x0,x1,x2),iext(uri_rdfs_domain,x3,x4),iext(uri_rdfs_subPropertyOf,x0,x5),iext(uri_rdfs_subPropertyOf,x5,x3),iext(uri_rdfs_subClassOf,x4,uri_rdf_Property) -> iext(uri_rdfs_subPropertyOf,x1,x1) % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1156 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1172 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1188 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1200 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1214 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1224 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1234 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1241 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1249 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1255 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1261 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1267 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1271 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1276 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1281 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1286 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1291 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1296 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1301 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1306 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1311 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1316 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1321 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1325 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1329 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1333 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1337 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1340 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1343 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1346 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1349 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1352 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1355 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1358 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1361 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1364 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1366 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1367 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1368 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1369 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1370 % 125.80/25.66 === Clause set with instances from active satisfied. Growing active. New size: 1371 % 125.80/25.66 % 125.80/25.66 Linear Model Building succeeded. % 125.80/25.66 SZS status Satisfiable % 125.80/25.66 % 125.80/25.66 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 125.80/25.66 % 125.80/25.66 SPASS-SCL-FOL Statistics: % 125.80/25.66 Number of learned clauses: 14 % 125.80/25.66 Number of propagations: 5597 % 125.80/25.66 Number of decisions: 1809 % 125.80/25.66 Number of resolutions: 22 % 125.80/25.66 Number of condensations: 0 % 125.80/25.66 Number of sub resolutions: 1 % 125.80/25.66 Number of input literals (deduplicated): 88 % 125.80/25.66 Number of grows: 121 % 125.80/25.66 Number of considered ground atoms: 1371 % 125.80/25.66 % 125.80/25.66 Needed: 0:0:25.10 % 125.80/25.66 %------------------------------------------------------------------------------