%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SWB025+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 : 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:47 PM UTC 2026
% Result : Theorem 10.18s 3.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWB025+2 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n007.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 13:19:39 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.21/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 10.18/3.82 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.18/3.82 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.18/3.82 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.18/3.82 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.18/3.82 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.18/3.82 Execution resolution_1 ended with status: unsatisfiable
% 10.18/3.82 Used heuristic: resolution_1
% 10.18/3.82
% 10.18/3.82 Input Clauses:
% 10.18/3.82
% 10.18/3.82 Predicates: iext ip ren1 ren2 ren3 ren4 ren5
% 10.18/3.82 Fol Constants: uri_rdf_first uri_rdf_rest uri_rdf_nil uri_owl_propertyChainAxiom uri_owl_inverseOf uri_ex_hasUncle uri_ex_alice uri_ex_charly uri_ex_hasCousin uri_ex_bob uri_ex_hasFather uri_ex_dave skc6 skc7 skc8 skc9 skc10
% 10.18/3.82 Fol Functions: skf1 skf2 skf3 skf4 skf5
% 10.18/3.82 Problem Properties:
% 10.18/3.82 This is a full first-order problem without equality.
% 10.18/3.82
% 10.18/3.82 After reduction: Problem Properties:
% 10.18/3.82 This is a full first-order problem without equality.
% 10.18/3.82
% 10.18/3.82
% 10.18/3.82 Reduced Input Clauses:
% 10.18/3.82
% 10.18/3.82 Most General Atoms: ren1(x0,x1,x2,x3,x4) ip(x2) ren2(x1,x3,x4,x2,x5,x0) ren3(x0,x2,x3) ren4(x4,x0,x1,x3) iext(x3,x2,x1) ren5(x0,x2,x3,x1)
% 10.18/3.82
% 10.18/3.82 === Starting SPASS-SCL-FOL A Little Less Naive, considering 20 atoms initially, heuristics mode: resolution_1 ===
% 10.18/3.82
% 10.18/3.82 === Backtracking. Learning clause 41:1:0:[22.1,36.1]:: -> ip(uri_ex_hasFather)
% 10.18/3.82 === Backtracking. Learning clause 42:1:0:[21.1,36.1]:: -> ip(skc10)
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 82
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 146
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 210
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 274
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 338
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 402
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 466
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 530
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 594
% 10.18/3.82 === Backtracking. Learning clause 43:7:8:[12.1,16.5,10.1,4.1]:TopTopTopTopTopTopTopTop: iext(uri_owl_propertyChainAxiom,x0,x1),iext(uri_rdf_first,x1,x2),iext(uri_rdf_rest,x1,x3),iext(uri_rdf_first,x3,x4),iext(uri_rdf_rest,x3,uri_rdf_nil),ren1(x2,x5,x6,x4,x7) -> iext(x0,x5,x7)
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 658
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 722
% 10.18/3.82 === Conflict found: 43:7:8:[12.1,16.5,10.1,4.1]:TopTopTopTopTopTopTopTop: iext(uri_owl_propertyChainAxiom,x0,x1),iext(uri_rdf_first,x1,x2),iext(uri_rdf_rest,x1,x3),iext(uri_rdf_first,x3,x4),iext(uri_rdf_rest,x3,uri_rdf_nil),ren1(x2,x5,x6,x4,x7) -> iext(x0,x5,x7) {x0 -> uri_rdf_first, x1 -> uri_rdf_first, x2 -> uri_rdf_nil, x3 -> uri_rdf_first, x4 -> uri_rdf_nil, x5 -> uri_rdf_first, x6 -> uri_rdf_first, x7 -> uri_rdf_first}
% 10.18/3.82 === Backtracking. Learning clause 44:8:9:[43.6,3.3,4.3]:TopTopTopTopTopTopTopTopTop: iext(uri_owl_propertyChainAxiom,x0,x1),iext(uri_rdf_rest,x1,x1),iext(uri_rdf_rest,x1,uri_rdf_nil),iext(x2,x3,x4),iext(x2,x4,x5),ren2(x6,x1,x7,x8,x2,uri_rdf_first),ren1(x6,x1,x7,x8,x2) -> iext(x0,x3,x5)
% 10.18/3.82 === Backtracking. Learning clause 45:1:2:[19.1,20.1]:TopTop: -> ren5(x0,x1,x1,x0)
% 10.18/3.82 === Backtracking. Learning clause 46:3:10:[2.2,12.2,5.1,10.1]:TopTopTopTopTopTopTopTopTopTop: ren4(x0,x1,x2,x3) -> ren2(x4,x5,x0,uri_owl_propertyChainAxiom,x1,x6),ren2(x2,x7,x8,x3,x9,x0)
% 10.18/3.82 === Backtracking. Learning clause 47:4:4:[3.3,4.2,20.2]:TopTopTopTop: ren2(x0,x1,x1,x0,x1,x2) -> iext(x2,x1,x1),iext(x3,x1,x1),ren5(x3,x1,x1,x0)
% 10.18/3.82 === Backtracking. Learning clause 48:3:8:[19.1,2.2,1.2]:TopTopTopTopTopTopTopTop: ren1(x0,x1,x2,x3,x4),ren1(x5,x4,x2,x6,x7) -> ren5(x3,x2,x4,x5)
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 786
% 10.18/3.82 === Conflict found: 43:7:8:[12.1,16.5,10.1,4.1]:TopTopTopTopTopTopTopTop: iext(uri_owl_propertyChainAxiom,x0,x1),iext(uri_rdf_first,x1,x2),iext(uri_rdf_rest,x1,x3),iext(uri_rdf_first,x3,x4),iext(uri_rdf_rest,x3,uri_rdf_nil),ren1(x2,x5,x6,x4,x7) -> iext(x0,x5,x7) {x0 -> uri_rdf_first, x1 -> uri_rdf_first, x2 -> uri_owl_propertyChainAxiom, x3 -> uri_rdf_rest, x4 -> uri_ex_dave, x5 -> uri_rdf_first, x6 -> uri_rdf_first, x7 -> uri_rdf_first}
% 10.18/3.82 === Backtracking. Learning clause 49:8:8:[43.6,3.3]:TopTopTopTopTopTopTopTop: iext(uri_owl_propertyChainAxiom,x0,x1),iext(uri_rdf_first,x1,x2),iext(uri_rdf_rest,x1,x3),iext(uri_rdf_first,x3,x4),iext(uri_rdf_rest,x3,uri_rdf_nil),iext(x2,x5,x6),iext(x4,x6,x7) -> iext(x0,x5,x7)
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 850
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 914
% 10.18/3.82 === Backtracking. Learning clause 50:6:5:[12.1,16.5]:TopTopTopTopTop: iext(uri_owl_propertyChainAxiom,x0,x1),iext(uri_rdf_first,x1,x2),iext(uri_rdf_rest,x1,x3),iext(uri_rdf_first,x3,x4),iext(uri_rdf_rest,x3,uri_rdf_nil) -> ren3(x0,x2,x4)
% 10.18/3.82 === Clause set with instances from active satisfied. Growing active. New size: 978
% 10.18/3.82
% 10.18/3.82 SZS status Unsatisfiable
% 10.18/3.82
% 10.18/3.82 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.18/3.82
% 10.18/3.82 SPASS-SCL-FOL Statistics:
% 10.18/3.82 Number of learned clauses: 10
% 10.18/3.82 Number of propagations: 3376
% 10.18/3.82 Number of decisions: 1203
% 10.18/3.82 Number of resolutions: 37
% 10.18/3.82 Number of condensations: 0
% 10.18/3.82 Number of sub resolutions: 0
% 10.18/3.82 Number of input literals (deduplicated): 31
% 10.18/3.82 Number of grows: 15
% 10.18/3.82 Number of considered ground atoms: 978
% 10.18/3.82
% 10.18/3.82 Needed: 0:00:03.27
% 10.18/3.82
%------------------------------------------------------------------------------