%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO650-1 : TPTP v9.2.1. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:14 PM UTC 2026
% Result : Unsatisfiable 0.38s 0.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO650-1 : TPTP v9.2.1. Released v7.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n015.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 13:56:32 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.38/0.72 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.72 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.72 Execution resolution_2 ended with status: unsatisfiable
% 0.38/0.72 Used heuristic: resolution_2
% 0.38/0.72
% 0.38/0.72 Input Clauses:
% 0.38/0.72
% 0.38/0.72 Predicates: 'E' iLEQ 'LE'
% 0.38/0.72 Fol Constants: '0' z
% 0.38/0.72 Fol Functions: suc f s
% 0.38/0.72 Problem Properties:
% 0.38/0.72 This is a full first-order problem without equality.
% 0.38/0.72
% 0.38/0.72 After reduction: Problem Properties:
% 0.38/0.72 This is a full first-order problem without equality.
% 0.38/0.72
% 0.38/0.72
% 0.38/0.72 Reduced Input Clauses:
% 0.38/0.72 38:12:3:[31.11,1.8,21.9,37.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 39:15:3:[31.12,2.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0))))
% 0.38/0.72 41:16:3:[32.14,3.4,39.14,40.9]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0))))
% 0.38/0.72 42:12:3:[21.8,4.6]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 44:14:3:[38.12,5.8,42.11,43.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 45:14:3:[31.12,6.4]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 46:2:1:[10.0,7.0]:Top: -> 'E'('0',f(x0)),'LE'(f(x0),'0')
% 0.38/0.72 47:15:3:[33.13,8.4]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 50:16:3:[35.15,9.5,41.16,48.9,39.14,49.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.38/0.72 52:15:3:[44.14,12.8,38.12,51.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(suc(x1))))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(x2)))
% 0.38/0.72 53:15:3:[42.12,13.3]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1)))
% 0.38/0.72 55:5:1:[26.4,14.4,34.2,54.5]:Top: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)) -> iLEQ(suc(x0),suc(x0))
% 0.38/0.72 57:15:3:[32.14,15.4,45.12,56.9]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 58:14:3:[42.12,16.3]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(suc(x0)))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 59:13:3:[21.10,17.3]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1)))
% 0.38/0.72 61:17:3:[52.16,18.5,47.14,60.16]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 64:15:3:[35.15,20.5,57.14,62.9,45.12,63.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 66:14:3:[38.13,23.4,45.13,65.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 68:18:3:[52.16,24.5,61.18,67.14]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x1))))),'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x1),suc(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(x1)),'E'(f(x1),f(suc(suc(x1)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) ->
% 0.38/0.72 70:15:3:[38.13,25.4,66.15,69.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1)))
% 0.38/0.72 71:5:1:[34.2,26.2]:Top: 'E'('0',f(suc(suc(x0)))),'E'('0',f(suc(x0))),'E'('0',f(x0)) -> 'E'(f(x0),f(suc(suc(x0)))),iLEQ(suc(x0),suc(x0))
% 0.38/0.72 74:15:3:[44.15,27.4,66.14,72.10,57.15,73.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72 77:16:3:[44.15,29.4,70.16,75.10,74.17,76.12]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),'E'('0',f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'(f(x0),f(suc(suc(x0)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'(f(x0),f(suc(x0))),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1))))
% 0.38/0.72 80:14:3:[33.13,30.4,53.14,78.8,59.12,79.10]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'(f(x2),f(suc(suc(x2)))),'E'('0',f(suc(suc(suc(x2))))),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1)))
% 0.38/0.72 81:12:3:[21.9,31.8]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 83:13:3:[81.10,32.7,42.11,82.10]:TopTopTop: 'E'('0',f(suc(suc(x0)))),iLEQ(suc(x1),suc(x0)),'E'('0',f(suc(x2))),'E'('0',f(suc(x1))),'E'('0',f(suc(suc(x1)))),'E'('0',f(x1)),iLEQ(suc(x0),suc(x2)),'E'('0',f(x0)),'E'('0',f(x2)),'E'('0',f(suc(x0))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x0),f(suc(suc(x0)))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 85:12:3:[42.10,33.6,21.8,84.8]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 88:13:3:[83.12,35.7,81.10,86.9,85.12,87.12]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(x2)))
% 0.38/0.72 89:12:3:[21.10,36.3]:TopTopTop: iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'('0',f(suc(x1))) -> 'E'(f(x0),f(suc(x0))),'E'(f(x1),f(suc(x1))),'E'(f(x2),f(suc(suc(x2))))
% 0.38/0.72
% 0.38/0.72 Most General Atoms: 'E'('0',f(x2)) 'E'(f(x0),f(suc(x0))) 'E'(f(x1),f(suc(suc(x1)))) iLEQ(suc(x1),suc(x2)) 'LE'(f(x0),'0') 'LE'(f(x0),s('0'))
% 0.38/0.72
% 0.38/0.72 === Starting SPASS-SCL-FOL A Little Less Naive, considering 53 atoms initially, heuristics mode: resolution_2 ===
% 0.38/0.72
% 0.38/0.72 === Conflict found: 64:15:3:[35.15,20.5,57.14,62.9,45.12,63.11]:TopTopTop: 'E'('0',f(suc(suc(suc(x0))))),'E'('0',f(suc(suc(x1)))),iLEQ(suc(x0),suc(x1)),'E'('0',f(suc(x2))),'E'('0',f(suc(x0))),'E'('0',f(suc(suc(x0)))),'E'('0',f(x0)),'E'('0',f(suc(suc(x2)))),iLEQ(suc(x1),suc(x2)),'E'('0',f(x1)),'E'('0',f(x2)),'E'(f(x1),f(suc(x1))),'E'('0',f(suc(x1))) -> 'E'(f(x1),f(suc(suc(x1)))),'E'(f(x2),f(suc(suc(x2)))) {x0 -> z, x1 -> z, x2 -> z}
% 0.38/0.72
% 0.38/0.72 SZS status Unsatisfiable
% 0.38/0.72
% 0.38/0.72 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.72
% 0.38/0.72 SPASS-SCL-FOL Statistics:
% 0.38/0.72 Number of learned clauses: 0
% 0.38/0.72 Number of propagations: 23
% 0.38/0.72 Number of decisions: 0
% 0.38/0.72 Number of resolutions: 11
% 0.38/0.72 Number of condensations: 0
% 0.38/0.72 Number of sub resolutions: 53
% 0.38/0.72 Number of input literals (deduplicated): 14
% 0.38/0.72 Number of grows: 0
% 0.38/0.72 Number of considered ground atoms: 53
% 0.38/0.72
% 0.38/0.72 Needed: 0:00:00.15
% 0.38/0.72
%------------------------------------------------------------------------------