↑ Up

Infinox---1.0.FTH-Ass.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : Infinox---1.0
% Problem  : SWB020+2 : TPTP v8.1.0. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_infinox %s

% Computer : n032.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  : 600s
% DateTime : Tue Jul 19 19:04:36 EDT 2022

% Result   : FiniteTheorem 214.22s 215.13s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.09  % Problem  : SWB020+2 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.10  % Command  : run_infinox %s
% 0.09/0.29  % Computer : n032.cluster.edu
% 0.09/0.29  % Model    : x86_64 x86_64
% 0.09/0.29  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29  % Memory   : 8042.1875MB
% 0.09/0.29  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29  % CPULimit : 300
% 0.09/0.29  % WCLimit  : 600
% 0.09/0.29  % DateTime : Wed Jun  1 07:30:59 EDT 2022
% 0.09/0.29  % CPUTime  : 
% 2.12/2.33  eprover: CPU time limit exceeded, terminating
% 4.12/4.34  eprover: CPU time limit exceeded, terminating
% 6.12/6.35  eprover: CPU time limit exceeded, terminating
% 8.14/8.36  eprover: CPU time limit exceeded, terminating
% 10.11/10.37  eprover: CPU time limit exceeded, terminating
% 12.20/12.38  eprover: CPU time limit exceeded, terminating
% 14.20/14.40  eprover: CPU time limit exceeded, terminating
% 16.22/16.41  eprover: CPU time limit exceeded, terminating
% 18.24/18.42  eprover: CPU time limit exceeded, terminating
% 20.23/20.43  eprover: CPU time limit exceeded, terminating
% 22.26/22.44  eprover: CPU time limit exceeded, terminating
% 24.25/24.45  eprover: CPU time limit exceeded, terminating
% 26.26/26.46  eprover: CPU time limit exceeded, terminating
% 28.22/28.47  eprover: CPU time limit exceeded, terminating
% 30.25/30.48  eprover: CPU time limit exceeded, terminating
% 32.28/32.50  eprover: CPU time limit exceeded, terminating
% 34.34/34.51  eprover: CPU time limit exceeded, terminating
% 36.35/36.52  eprover: CPU time limit exceeded, terminating
% 38.35/38.53  eprover: CPU time limit exceeded, terminating
% 40.37/40.54  eprover: CPU time limit exceeded, terminating
% 42.38/42.55  eprover: CPU time limit exceeded, terminating
% 44.37/44.56  eprover: CPU time limit exceeded, terminating
% 46.44/46.57  eprover: CPU time limit exceeded, terminating
% 48.36/48.58  eprover: CPU time limit exceeded, terminating
% 50.45/50.59  eprover: CPU time limit exceeded, terminating
% 52.48/52.61  eprover: CPU time limit exceeded, terminating
% 54.45/54.62  eprover: CPU time limit exceeded, terminating
% 56.47/56.63  eprover: CPU time limit exceeded, terminating
% 58.46/58.64  eprover: CPU time limit exceeded, terminating
% 60.51/60.65  eprover: CPU time limit exceeded, terminating
% 62.52/62.66  eprover: CPU time limit exceeded, terminating
% 64.56/64.67  eprover: CPU time limit exceeded, terminating
% 66.54/66.68  eprover: CPU time limit exceeded, terminating
% 68.58/68.69  eprover: CPU time limit exceeded, terminating
% 70.53/70.70  eprover: CPU time limit exceeded, terminating
% 72.62/72.71  eprover: CPU time limit exceeded, terminating
% 74.55/74.72  eprover: CPU time limit exceeded, terminating
% 76.59/76.74  eprover: CPU time limit exceeded, terminating
% 78.61/78.75  eprover: CPU time limit exceeded, terminating
% 80.62/80.76  eprover: CPU time limit exceeded, terminating
% 82.65/82.77  eprover: CPU time limit exceeded, terminating
% 84.70/84.78  eprover: CPU time limit exceeded, terminating
% 86.63/86.80  eprover: CPU time limit exceeded, terminating
% 88.74/88.81  eprover: CPU time limit exceeded, terminating
% 90.72/90.82  eprover: CPU time limit exceeded, terminating
% 92.76/92.83  eprover: CPU time limit exceeded, terminating
% 94.73/94.85  eprover: CPU time limit exceeded, terminating
% 96.76/96.86  eprover: CPU time limit exceeded, terminating
% 98.76/98.88  eprover: CPU time limit exceeded, terminating
% 100.75/100.89  eprover: CPU time limit exceeded, terminating
% 102.80/102.90  eprover: CPU time limit exceeded, terminating
% 104.85/104.92  eprover: CPU time limit exceeded, terminating
% 106.84/106.93  eprover: CPU time limit exceeded, terminating
% 108.89/108.94  eprover: CPU time limit exceeded, terminating
% 110.83/110.95  eprover: CPU time limit exceeded, terminating
% 112.90/112.97  eprover: CPU time limit exceeded, terminating
% 114.84/114.98  eprover: CPU time limit exceeded, terminating
% 116.90/116.99  eprover: CPU time limit exceeded, terminating
% 118.96/119.00  eprover: CPU time limit exceeded, terminating
% 120.96/121.02  eprover: CPU time limit exceeded, terminating
% 122.94/123.03  eprover: CPU time limit exceeded, terminating
% 124.98/125.04  eprover: CPU time limit exceeded, terminating
% 126.96/127.05  eprover: CPU time limit exceeded, terminating
% 128.99/129.06  eprover: CPU time limit exceeded, terminating
% 131.03/131.07  eprover: CPU time limit exceeded, terminating
% 133.01/133.08  eprover: CPU time limit exceeded, terminating
% 135.00/135.09  eprover: CPU time limit exceeded, terminating
% 137.07/137.10  eprover: CPU time limit exceeded, terminating
% 139.10/139.11  eprover: CPU time limit exceeded, terminating
% 141.10/141.12  eprover: CPU time limit exceeded, terminating
% 143.14/143.13  eprover: CPU time limit exceeded, terminating
% 145.08/145.14  eprover: CPU time limit exceeded, terminating
% 147.15/147.15  eprover: CPU time limit exceeded, terminating
% 149.15/149.17  eprover: CPU time limit exceeded, terminating
% 151.18/151.18  eprover: CPU time limit exceeded, terminating
% 153.13/153.19  eprover: CPU time limit exceeded, terminating
% 155.21/155.20  eprover: CPU time limit exceeded, terminating
% 157.25/157.21  eprover: CPU time limit exceeded, terminating
% 159.22/159.22  eprover: CPU time limit exceeded, terminating
% 161.21/161.24  eprover: CPU time limit exceeded, terminating
% 163.23/163.25  eprover: CPU time limit exceeded, terminating
% 165.29/165.26  eprover: CPU time limit exceeded, terminating
% 167.24/167.27  eprover: CPU time limit exceeded, terminating
% 169.27/169.29  eprover: CPU time limit exceeded, terminating
% 171.33/171.30  eprover: CPU time limit exceeded, terminating
% 173.28/173.31  eprover: CPU time limit exceeded, terminating
% 175.32/175.32  eprover: CPU time limit exceeded, terminating
% 177.37/177.33  eprover: CPU time limit exceeded, terminating
% 179.33/179.34  eprover: CPU time limit exceeded, terminating
% 181.37/181.35  eprover: CPU time limit exceeded, terminating
% 183.36/183.36  eprover: CPU time limit exceeded, terminating
% 185.41/185.37  eprover: CPU time limit exceeded, terminating
% 187.37/187.38  eprover: CPU time limit exceeded, terminating
% 189.39/189.39  eprover: CPU time limit exceeded, terminating
% 191.45/191.40  eprover: CPU time limit exceeded, terminating
% 193.40/193.41  eprover: CPU time limit exceeded, terminating
% 195.45/195.42  eprover: CPU time limit exceeded, terminating
% 197.50/197.43  eprover: CPU time limit exceeded, terminating
% 199.42/199.44  eprover: CPU time limit exceeded, terminating
% 201.49/201.45  eprover: CPU time limit exceeded, terminating
% 203.46/203.46  eprover: CPU time limit exceeded, terminating
% 205.50/205.47  eprover: CPU time limit exceeded, terminating
% 207.56/207.48  eprover: CPU time limit exceeded, terminating
% 209.51/209.49  eprover: CPU time limit exceeded, terminating
% 211.57/211.50  eprover: CPU time limit exceeded, terminating
% 213.51/213.51  eprover: CPU time limit exceeded, terminating
% 214.22/215.13  Infinox, version 1.0, 2009-07-20.
% 214.22/215.13  +++ PROBLEM: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 214.22/215.13  Reading '/export/starexec/sandbox2/benchmark/theBenchmark.p' ... OK
% 214.22/215.13  +++ SOLVING: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 214.22/215.13  InjNotSurj
% 214.22/215.13  SurjNotInj
% 214.22/215.13  Serial
% 214.22/215.13  Trans
% 214.22/215.13  +++ RESULT: FinitelyCounterUnsatisfiable
% 214.22/215.13  % SZS status FiniteTheorem
%------------------------------------------------------------------------------