%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : KRS116+1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n025.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:26:22 PM UTC 2026
% Result : Unsatisfiable 0.55s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS116+1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.32 % Computer : n025.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Thu May 7 12:19:44 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.32 SPASS-SCL-FOL version:
% 0.18/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.55/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.55/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.55/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.55/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.55/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.55/0.60 Execution resolution_2 ended with status: unsatisfiable
% 0.55/0.60 Used heuristic: resolution_2
% 0.55/0.60
% 0.55/0.60 Input Clauses:
% 0.55/0.60
% 0.55/0.60 Predicates: cowlThing cowlNothing xsd_string xsd_integer cUnsatisfiable ca rs ca_Ax2 ra_Px1 caxcomp cc rinvR ca_Vx7 rp ca_Vx3 ca_Vx5 rr ca_Vx4 ca_Vx6 rinvS rinvP ren1 ren2 ren3 ren4 ren5 ren6 ren7
% 0.55/0.60 Fol Constants: i2003_11_14_17_21_33997
% 0.55/0.60 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15
% 0.55/0.60 Problem Properties:
% 0.55/0.60 This is a full first-order problem without equality.
% 0.55/0.60
% 0.55/0.60 After reduction: Problem Properties:
% 0.55/0.60 This is a full first-order problem without equality.
% 0.55/0.60
% 0.55/0.60
% 0.55/0.60 Reduced Input Clauses:
% 0.55/0.60 64:2:2:[1.0,27.1]:TopTop: rr(x0,x1) -> ren5(x0,x1)
% 0.55/0.60 65:2:2:[1.0,30.1]:TopTop: rp(x0,x1) -> ren6(x0,x1)
% 0.55/0.60 66:2:2:[1.0,43.1]:TopTop: rr(x0,x1) -> ca_Vx3(x0)
% 0.55/0.60 67:2:2:[1.0,46.1]:TopTop: rp(x0,x1) -> ca_Vx4(x0)
% 0.55/0.60
% 0.55/0.60 Most General Atoms: cowlThing(x0) cowlNothing(x0) xsd_string(x0) xsd_integer(x0) cUnsatisfiable(x0) ca(x0) ren1(x0,x1) ra_Px1(x0,x1) ca_Vx3(x0) ren2(x1,x0) ca_Vx5(x0) ren3(x1,x0) cc(x1) ren4(x1,x0) ren5(x0,x1) ca_Vx4(x0) ren7(x1,x0) ca_Ax2(x0) ren6(x0,x2) rinvS(x0,x1) rs(x1,x0) caxcomp(x1) ca_Vx7(x0) ca_Vx6(x1) rp(x1,x0) rinvP(x1,x0) rr(x1,x0) rinvR(x1,x0)
% 0.55/0.60
% 0.55/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 95 atoms initially, heuristics mode: resolution_2 ===
% 0.55/0.60
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 95
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 68:1:0:[5.1,63.1]:: -> ca(i2003_11_14_17_21_33997)
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 95
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 69:1:1:[9.1,68.1]:Top: ra_Px1(i2003_11_14_17_21_33997,x0) ->
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 95
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 70:3:2:[61.1,6.2,50.2,51.2]:TopTop: ren1(x0,x1) -> caxcomp(x0),rinvS(x1,skf14(x1))
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 95
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Conflict found: 67:2:2:[1.0,46.1]:TopTop: rp(x0,x1) -> ca_Vx4(x0) {x0 -> skf1(i2003_11_14_17_21_33997), x1 -> skf12(skf1(i2003_11_14_17_21_33997))}
% 0.55/0.60 === Backtracking. Learning clause 71:2:3:[67.2,33.1]:TopTopTop: rp(x0,x1) -> ren7(x2,x0)
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 159
% 0.55/0.60 === Conflict found: 66:2:2:[1.0,43.1]:TopTop: rr(x0,x1) -> ca_Vx3(x0) {x0 -> i2003_11_14_17_21_33997, x1 -> skf9(i2003_11_14_17_21_33997)}
% 0.55/0.60 === Backtracking. Learning clause 72:2:2:[66.1,23.1,41.1]:TopTop: -> ren4(x0,x1),rr(x0,skf11(x0))
% 0.55/0.60 === Backtracking. Learning clause 73:2:2:[47.3,24.1,23.1]:TopTop: ca_Vx5(x0) -> ren4(x0,x1)
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 159
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 74:2:2:[32.1,67.1]:TopTop: -> ren7(x0,x1),ca_Vx4(x0)
% 0.55/0.60 === Backtracking. Learning clause 75:2:1:[22.2,48.1,49.1]:Top: ren4(x0,skf13(x0)) -> ca_Vx5(x0)
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 159
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 76:1:0:[8.2,6.1,63.1]:: -> rs(i2003_11_14_17_21_33997,skf1(i2003_11_14_17_21_33997))
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 159
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 77:1:0:[61.1,76.1]:: -> rinvS(skf1(i2003_11_14_17_21_33997),i2003_11_14_17_21_33997)
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 159
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Backtracking. Learning clause 78:2:0:[50.2,77.1]:: ca_Vx6(skf1(i2003_11_14_17_21_33997)) -> caxcomp(i2003_11_14_17_21_33997)
% 0.55/0.60 === Backtracking. Learning clause 79:1:0:[11.2,69.1,78.2]:: ca_Vx6(skf1(i2003_11_14_17_21_33997)) ->
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 223
% 0.55/0.60 === Backtracking. Learning clause 80:5:4:[13.2,59.2,47.3,53.1,57.2,28.2]:TopTopTopTop: rr(x0,x1),ca_Vx5(x2),rr(x2,x1),ren6(x3,x0) -> ca_Vx6(x3)
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 223
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Conflict found: 80:5:4:[13.2,59.2,47.3,53.1,57.2,28.2]:TopTopTopTop: rr(x0,x1),ca_Vx5(x2),rr(x2,x1),ren6(x3,x0) -> ca_Vx6(x3) {x0 -> i2003_11_14_17_21_33997, x1 -> i2003_11_14_17_21_33997, x2 -> i2003_11_14_17_21_33997, x3 -> skf1(i2003_11_14_17_21_33997)}
% 0.55/0.60 === Backtracking. Learning clause 81:4:3:[80.5,79.1]:TopTopTop: rr(x0,x1),ca_Vx5(x2),rr(x2,x1),ren6(skf1(i2003_11_14_17_21_33997),x0) ->
% 0.55/0.60 === Backtracking. Learning clause 82:2:1:[53.3,79.1]:Top: ca_Vx7(x0),rinvP(x0,skf1(i2003_11_14_17_21_33997)) ->
% 0.55/0.60 === Backtracking. Learning clause 83:1:0:[52.2,79.1]:: caxcomp(skf14(skf1(i2003_11_14_17_21_33997))) ->
% 0.55/0.60 === Backtracking. Learning clause 84:3:1:[41.2,81.1,16.3,19.3,65.2,56.2]:Top: ren2(skf1(i2003_11_14_17_21_33997),x0),ren3(skf1(i2003_11_14_17_21_33997),x0),rinvP(x0,skf1(i2003_11_14_17_21_33997)) ->
% 0.55/0.60 === Clause set with instances from active satisfied. Growing active. New size: 226
% 0.55/0.60 === Restarting.
% 0.55/0.60 === Conflict found: 70:3:2:[61.1,6.2,50.2,51.2]:TopTop: ren1(x0,x1) -> caxcomp(x0),rinvS(x1,skf14(x1)) {x0 -> skf14(skf1(i2003_11_14_17_21_33997)), x1 -> i2003_11_14_17_21_33997}
% 0.55/0.60 === Backtracking. Learning clause 85:2:1:[70.2,83.1]:Top: ren1(skf14(skf1(i2003_11_14_17_21_33997)),x0) -> rinvS(x0,skf14(x0))
% 0.55/0.60 === Backtracking. Learning clause 86:2:1:[50.3,83.1]:Top: ca_Vx6(x0),rinvS(x0,skf14(skf1(i2003_11_14_17_21_33997))) ->
% 0.55/0.60 === Backtracking. Learning clause 87:1:1:[12.2,83.1]:Top: ra_Px1(skf14(skf1(i2003_11_14_17_21_33997)),x0) ->
% 0.55/0.60 === Backtracking. Learning clause 88:4:3:[34.2,16.1,7.2,41.1,81.1]:TopTopTop: rp(x0,x1),ren1(x2,x0),ca_Vx5(x1),ren6(skf1(i2003_11_14_17_21_33997),x1) ->
% 0.55/0.60 === Backtracking. Learning clause 89:2:2:[35.2,19.1,7.2,88.3,65.2,56.2]:TopTop: ren1(x0,skf1(i2003_11_14_17_21_33997)),rinvP(x1,skf1(i2003_11_14_17_21_33997)) ->
% 0.55/0.60 === Conflict found: 67:2:2:[1.0,46.1]:TopTop: rp(x0,x1) -> ca_Vx4(x0) {x0 -> skf1(i2003_11_14_17_21_33997), x1 -> skf6(skf1(i2003_11_14_17_21_33997))}
% 0.55/0.60
% 0.55/0.60 SZS status Unsatisfiable
% 0.55/0.60
% 0.55/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.55/0.60
% 0.55/0.60 SPASS-SCL-FOL Statistics:
% 0.55/0.60 Number of learned clauses: 22
% 0.55/0.60 Number of propagations: 1452
% 0.55/0.60 Number of decisions: 584
% 0.55/0.60 Number of resolutions: 52
% 0.55/0.60 Number of condensations: 2
% 0.55/0.60 Number of sub resolutions: 4
% 0.55/0.60 Number of input literals (deduplicated): 48
% 0.55/0.60 Number of grows: 12
% 0.55/0.60 Number of considered ground atoms: 226
% 0.55/0.60
% 0.55/0.60 Needed: 0:00:00.07
% 0.55/0.60
%------------------------------------------------------------------------------