%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : KRS090+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 : n001.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:21 PM UTC 2026 % Result : Unsatisfiable 0.29s 0.51s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS090+1 : TPTP v9.2.1. Released v3.1.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 : n001.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 12:20:19 EDT 2026 % 0.15/0.33 % CPUTime : % 0.15/0.33 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.29/0.51 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.29/0.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.29/0.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.29/0.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.29/0.51 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.29/0.51 Execution normal ended with status: unsatisfiable % 0.29/0.51 Used heuristic: normal % 0.29/0.51 % 0.29/0.51 Input Clauses: % 0.29/0.51 % 0.29/0.51 Predicates: cowlThing cowlNothing xsd_string xsd_integer cC1 cB5 cA5 cB13 cA13 cA1 cB1 cA27 cB27 cA4 cB4 cB12 cA12 cB30 cA30 cA20 cB20 cB14 cA14 cB28 cA28 cA3 cB3 cB7 cA7 cB21 cA21 cB22 cA22 cB17 cA17 cB11 cA11 cB19 cA19 cA8 cB8 cA26 cB26 cA25 cB25 cA29 cB29 cB23 cA23 cB18 cA18 cB10 cA10 cB2 cA2 cA16 cB16 cB0 cA0 cB31 cA31 cB9 cA9 cB6 cA6 cB24 cA24 cB15 cA15 cC2 cB cA cC3 cC4 rR cC5 cTEST ren1 ren2 ren3 ren4 ren5 % 0.29/0.51 Fol Constants: i2003_11_14_17_19_57994 % 0.29/0.51 Fol Functions: skf1 % 0.29/0.51 Problem Properties: % 0.29/0.51 This is a full first-order problem without equality. % 0.29/0.51 % 0.29/0.51 After reduction: Problem Properties: % 0.29/0.51 This is a full first-order problem without equality. % 0.29/0.51 % 0.29/0.51 % 0.29/0.51 Reduced Input Clauses: % 0.29/0.51 53:2:1:[39.1,38.1]:Top: ren2(x0) -> cA(x0) % 0.29/0.51 54:2:1:[42.2,41.1]:Top: ren3(x0),cA(x0) -> % 0.29/0.51 % 0.29/0.51 Most General Atoms: cowlThing(x0) cowlNothing(x0) xsd_string(x0) xsd_integer(x0) ren1(x0) cB5(x0) cA5(x0) cB13(x0) cA13(x0) cA1(x0) cB1(x0) cA27(x0) cB27(x0) cA4(x0) cB4(x0) cB12(x0) cA12(x0) cB30(x0) cA30(x0) cA20(x0) cB20(x0) cB14(x0) cA14(x0) cB28(x0) cA28(x0) cA3(x0) cB3(x0) cB7(x0) cA7(x0) cB21(x0) cA21(x0) cB22(x0) cA22(x0) cB17(x0) cA17(x0) cB11(x0) cA11(x0) cB19(x0) cA19(x0) cA8(x0) cB8(x0) cA26(x0) cB26(x0) cA25(x0) cB25(x0) cA29(x0) cB29(x0) cB23(x0) cA23(x0) cB18(x0) cA18(x0) cB10(x0) cA10(x0) cB2(x0) cA2(x0) cA16(x0) cB16(x0) cB0(x0) cA0(x0) cB31(x0) cA31(x0) cB9(x0) cA9(x0) cB6(x0) cA6(x0) cB24(x0) cA24(x0) cB15(x0) cA15(x0) cC1(x0) ren2(x0) cA(x0) cB(x0) ren3(x0) ren4(x0,x1) rR(x0,x1) cC2(x1) cC4(x0) cC5(x0) cC3(x1) ren5(x0) cTEST(x0) % 0.29/0.51 % 0.29/0.51 === Starting SPASS-SCL-FOL A Little Less Naive, considering 84 atoms initially, heuristics mode: normal === % 0.29/0.51 % 0.29/0.51 === Clause set with instances from active satisfied. Growing active. New size: 148 % 0.29/0.51 % 0.29/0.51 SZS status Unsatisfiable % 0.29/0.51 % 0.29/0.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.29/0.51 % 0.29/0.51 SPASS-SCL-FOL Statistics: % 0.29/0.51 Number of learned clauses: 0 % 0.29/0.51 Number of propagations: 68 % 0.29/0.51 Number of decisions: 54 % 0.29/0.51 Number of resolutions: 11 % 0.29/0.51 Number of condensations: 0 % 0.29/0.51 Number of sub resolutions: 2 % 0.29/0.51 Number of input literals (deduplicated): 84 % 0.29/0.51 Number of grows: 1 % 0.29/0.51 Number of considered ground atoms: 148 % 0.29/0.51 % 0.29/0.51 Needed: 0:00:00.00 % 0.29/0.51 %------------------------------------------------------------------------------