%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO578+1 : TPTP v9.2.1. Released v5.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.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:41:09 PM UTC 2026
% Result : Theorem 0.52s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO578+1 : TPTP v9.2.1. Released v5.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n023.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:56:24 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.52/0.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.56 Execution normal ended with status: unsatisfiable
% 0.52/0.56 Used heuristic: normal
% 0.52/0.56
% 0.52/0.56 Input Clauses:
% 0.52/0.56
% 0.52/0.56 Predicates: k04_buttercup10620 k04_buttercup10619 k04_buttercup10622 b48_buttercup10102 b48_buttercup10098 b48_buttercup10104 b48_buttercup10107 b48_buttercup10108 b48_buttercup10109 b48_buttercup10110 b48_buttercup10111 k04_buttercup10100 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23
% 0.52/0.56 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc21 skc22 skc23 skc24 skc25 skc26 skc27 skc28 skc29 skc30 skc31 skc32 skc33 skc34 skc35 skc36 skc37 skc38 skc39 skc40 skc41 skc42 skc43 skc44 skc45 skc46 skc47 skc48 skc49 skc50 skc51 skc52 skc53 skc54 skc55 skc56 skc57 skc58
% 0.52/0.56 Fol Functions:
% 0.52/0.56 Problem Properties:
% 0.52/0.56 This is a Bernays Schoenfinkel problem.
% 0.52/0.56
% 0.52/0.56 After reduction: Problem Properties:
% 0.52/0.56 This is a Bernays Schoenfinkel problem.
% 0.52/0.56
% 0.52/0.56
% 0.52/0.56 Reduced Input Clauses:
% 0.52/0.56
% 0.52/0.56 Most General Atoms: k04_buttercup10620(x0) k04_buttercup10622(x0) b48_buttercup10098(x0) ren1(x0,x1,x2) k04_buttercup10100(x2) b48_buttercup10104(x2) ren2 ren3 ren4(x0,x1,x2) k04_buttercup10619(x2) b48_buttercup10111(x2) ren5 ren6 ren7(x0,x1,x2) b48_buttercup10109(x2) ren8 ren9 ren10(x0,x1,x2) b48_buttercup10108(x2) ren11 ren12 ren13(x0,x1,x2) b48_buttercup10110(x2) ren14 ren15 ren16(x0,x1,x2) b48_buttercup10102(x2) ren17 ren18 ren19(x0,x1,x2) b48_buttercup10107(x2) ren20 ren21 ren23(x0) ren22(x0)
% 0.52/0.56
% 0.52/0.56 === Starting SPASS-SCL-FOL A Little Less Naive, considering 101 atoms initially, heuristics mode: normal ===
% 0.52/0.56
% 0.52/0.56 === Backtracking. Learning clause 196:2:5:[13.2,15.2]:TopTopTopTopTop: ren1(x0,x1,x2),ren1(x3,x4,x1) ->
% 0.52/0.56 === Clause set with instances from active satisfied. Growing active. New size: 154
% 0.52/0.56 === Backtracking. Learning clause 197:2:1:[84.2,2.1]:Top: b48_buttercup10104(x0) -> k04_buttercup10619(x0)
% 0.52/0.56 === Conflict found: 197:2:1:[84.2,2.1]:Top: b48_buttercup10104(x0) -> k04_buttercup10619(x0) {x0 -> skc3}
% 0.52/0.56 === Backtracking. Learning clause 198:1:3:[197.2,142.1,11.2,10.2]:TopTopTop: ren1(x0,x1,x2) ->
% 0.52/0.56 === Clause set with instances from active satisfied. Growing active. New size: 218
% 0.52/0.56 === Clause set with instances from active satisfied. Growing active. New size: 282
% 0.52/0.56 === Clause set with instances from active satisfied. Growing active. New size: 346
% 0.52/0.56 === Backtracking. Learning clause 199:1:3:[55.2,142.2,27.2,26.2]:TopTopTop: ren4(x0,x1,x2) ->
% 0.52/0.56 === Backtracking. Learning clause 200:2:5:[72.2,74.2]:TopTopTopTopTop: ren13(x0,x1,x2),ren13(x3,x0,x4) ->
% 0.52/0.56 === Backtracking. Learning clause 201:2:3:[43.2,170.1]:TopTopTop: ren7(x0,x1,x2),b48_buttercup10108(x0) ->
% 0.52/0.56 === Clause set with instances from active satisfied. Growing active. New size: 410
% 0.52/0.56
% 0.52/0.56 SZS status Unsatisfiable
% 0.52/0.56
% 0.52/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.56
% 0.52/0.56 SPASS-SCL-FOL Statistics:
% 0.52/0.56 Number of learned clauses: 6
% 0.52/0.56 Number of propagations: 1073
% 0.52/0.56 Number of decisions: 166
% 0.52/0.56 Number of resolutions: 15
% 0.52/0.56 Number of condensations: 2
% 0.52/0.56 Number of sub resolutions: 0
% 0.52/0.56 Number of input literals (deduplicated): 101
% 0.52/0.56 Number of grows: 5
% 0.52/0.56 Number of considered ground atoms: 410
% 0.52/0.56
% 0.52/0.56 Needed: 0:00:00.07
% 0.52/0.56
%------------------------------------------------------------------------------