%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL663+1.005 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:28:10 PM UTC 2026
% Result : CounterSatisfiable 0.78s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL663+1.005 : TPTP v9.2.1. Released v4.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n018.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 12:38:18 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.16/0.39 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.78/0.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.66 Execution resolution_2 ended with status: satisfiable
% 0.78/0.66 Used heuristic: resolution_2
% 0.78/0.66
% 0.78/0.66 Input Clauses:
% 0.78/0.66
% 0.78/0.66 Predicates: r1 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10
% 0.78/0.66 Fol Constants: skc7
% 0.78/0.66 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf8 skf9 skf10 skf11
% 0.78/0.66 Problem Properties:
% 0.78/0.66 This is a full first-order problem without equality.
% 0.78/0.66
% 0.78/0.66 After reduction: Problem Properties:
% 0.78/0.66 This is a full first-order problem without equality.
% 0.78/0.66
% 0.78/0.66
% 0.78/0.66 Reduced Input Clauses:
% 0.78/0.66 27:2:1:[26.0,25.2]:Top: r1(skc7,x0),ren10(x0,skf11(x0)) ->
% 0.78/0.66
% 0.78/0.66 Most General Atoms: r1(x3,x4) ren1(x5,x0) p1(x3) ren2(x5,x0) ren3(x4,x0) ren4(x4,x0) ren5(x5,x0) ren6(x5,x0) ren7(x4,x0) ren8(x5,x0) ren9(x5,x0) ren10(x5,x0)
% 0.78/0.66
% 0.78/0.66 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: resolution_2 ===
% 0.78/0.66
% 0.78/0.66 === Clause set with instances from active satisfied. Growing active. New size: 49
% 0.78/0.66 === Restarting.
% 0.78/0.66 === Backtracking. Learning clause 28:3:2:[19.1,1.1]:TopTop: ren8(x0,skf6(x0)) -> p1(x0),ren9(x1,x0)
% 0.78/0.66 === Backtracking. Learning clause 29:3:2:[13.1,1.1]:TopTop: ren5(x0,skf4(x0)) -> p1(x0),ren6(x1,x0)
% 0.78/0.66 === Backtracking. Learning clause 30:3:2:[5.1,1.1]:TopTop: ren1(x0,skf1(x0)) -> p1(x0),ren2(x1,x0)
% 0.78/0.66 === Backtracking. Learning clause 31:2:2:[15.1,1.1]:TopTop: ren6(x0,skf5(x0)) -> ren7(x1,x0)
% 0.78/0.66 === Backtracking. Learning clause 32:2:2:[9.1,1.1]:TopTop: ren3(x0,skf3(x0)) -> ren4(x1,x0)
% 0.78/0.66 === Backtracking. Learning clause 33:2:2:[7.1,1.1]:TopTop: ren2(x0,skf2(x0)) -> ren3(x1,x0)
% 0.78/0.66 === Backtracking. Learning clause 34:1:0:[24.1,1.1]:: ren9(skc7,skf10(skc7)) ->
% 0.78/0.66 === Clause set with instances from active satisfied. Growing active. New size: 49
% 0.78/0.66 === Restarting.
% 0.78/0.66 === Backtracking. Learning clause 35:2:1:[5.6,26.1,1.1]:Top: ren1(skc7,skf1(skc7)) -> ren2(x0,skc7)
% 0.78/0.66 === Backtracking. Learning clause 36:2:1:[13.6,26.1,1.1]:Top: ren5(skc7,skf4(skc7)) -> ren6(x0,skc7)
% 0.78/0.66 === Backtracking. Learning clause 37:2:1:[19.6,26.1,1.1]:Top: ren8(skc7,skf6(skc7)) -> ren9(x0,skc7)
% 0.78/0.66 === Clause set with instances from active satisfied. Growing active. New size: 53
% 0.78/0.66 === Restarting.
% 0.78/0.66 === Conflict found: 28:3:2:[19.1,1.1]:TopTop: ren8(x0,skf6(x0)) -> p1(x0),ren9(x1,x0) {x0 -> skf10(skc7), x1 -> skc7}
% 0.78/0.66 === Backtracking. Learning clause 38:2:0:[28.3,34.1]:: ren8(skf10(skc7),skf6(skf10(skc7))) -> p1(skf10(skc7))
% 0.78/0.66 === Backtracking. Learning clause 39:1:0:[18.2,34.1]:: -> r1(skc7,skf10(skc7))
% 0.78/0.66 === Clause set with instances from active satisfied. Growing active. New size: 55
% 0.78/0.66 === Restarting.
% 0.78/0.66 === Backtracking. Learning clause 40:1:0:[23.1,1.1]:: ren7(skc7,skf9(skc7)) ->
% 0.78/0.66
% 0.78/0.66 Linear Model Building succeeded.
% 0.78/0.66 SZS status Satisfiable
% 0.78/0.66
% 0.78/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.66
% 0.78/0.66 SPASS-SCL-FOL Statistics:
% 0.78/0.66 Number of learned clauses: 13
% 0.78/0.66 Number of propagations: 164
% 0.78/0.66 Number of decisions: 147
% 0.78/0.66 Number of resolutions: 16
% 0.78/0.66 Number of condensations: 0
% 0.78/0.66 Number of sub resolutions: 1
% 0.78/0.66 Number of input literals (deduplicated): 25
% 0.78/0.66 Number of grows: 4
% 0.78/0.66 Number of considered ground atoms: 55
% 0.78/0.66
% 0.78/0.66 Needed: 0:00:00.12
% 0.78/0.66
%------------------------------------------------------------------------------