%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : LAT355+1 : TPTP v8.1.0. Released v3.4.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 : Sun Jul 17 05:14:57 EDT 2022 % Result : FiniteTheorem 227.43s 227.42s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.10 % Problem : LAT355+1 : TPTP v8.1.0. Released v3.4.0. % 0.08/0.10 % Command : run_infinox %s % 0.09/0.30 % Computer : n032.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 600 % 0.09/0.30 % DateTime : Wed Jun 29 15:41:28 EDT 2022 % 0.09/0.30 % CPUTime : % 2.44/2.66 eprover: CPU time limit exceeded, terminating % 4.44/4.67 eprover: CPU time limit exceeded, terminating % 6.45/6.68 eprover: CPU time limit exceeded, terminating % 8.51/8.69 eprover: CPU time limit exceeded, terminating % 10.58/10.70 eprover: CPU time limit exceeded, terminating % 12.55/12.71 eprover: CPU time limit exceeded, terminating % 14.60/14.72 eprover: CPU time limit exceeded, terminating % 16.64/16.73 eprover: CPU time limit exceeded, terminating % 18.63/18.74 eprover: CPU time limit exceeded, terminating % 20.64/20.75 eprover: CPU time limit exceeded, terminating % 22.69/22.76 eprover: CPU time limit exceeded, terminating % 24.65/24.77 eprover: CPU time limit exceeded, terminating % 26.72/26.79 eprover: CPU time limit exceeded, terminating % 28.77/28.81 eprover: CPU time limit exceeded, terminating % 30.80/30.82 eprover: CPU time limit exceeded, terminating % 32.78/32.83 eprover: CPU time limit exceeded, terminating % 34.82/34.85 eprover: CPU time limit exceeded, terminating % 36.79/36.87 eprover: CPU time limit exceeded, terminating % 38.86/38.89 eprover: CPU time limit exceeded, terminating % 40.92/40.90 eprover: CPU time limit exceeded, terminating % 42.96/42.92 eprover: CPU time limit exceeded, terminating % 44.95/44.93 eprover: CPU time limit exceeded, terminating % 47.00/46.94 eprover: CPU time limit exceeded, terminating % 48.96/48.95 eprover: CPU time limit exceeded, terminating % 50.99/50.98 eprover: CPU time limit exceeded, terminating % 53.06/52.99 eprover: CPU time limit exceeded, terminating % 55.09/55.01 eprover: CPU time limit exceeded, terminating % 57.09/57.05 eprover: CPU time limit exceeded, terminating % 59.09/59.06 eprover: CPU time limit exceeded, terminating % 61.11/61.07 eprover: CPU time limit exceeded, terminating % 63.10/63.09 eprover: CPU time limit exceeded, terminating % 65.20/65.11 eprover: CPU time limit exceeded, terminating % 67.24/67.12 eprover: CPU time limit exceeded, terminating % 69.24/69.14 eprover: CPU time limit exceeded, terminating % 71.23/71.15 eprover: CPU time limit exceeded, terminating % 73.27/73.16 eprover: CPU time limit exceeded, terminating % 75.29/75.18 eprover: CPU time limit exceeded, terminating % 77.37/77.20 eprover: CPU time limit exceeded, terminating % 79.40/79.21 eprover: CPU time limit exceeded, terminating % 81.40/81.22 eprover: CPU time limit exceeded, terminating % 83.40/83.23 eprover: CPU time limit exceeded, terminating % 85.44/85.25 eprover: CPU time limit exceeded, terminating % 87.42/87.26 eprover: CPU time limit exceeded, terminating % 89.45/89.27 eprover: CPU time limit exceeded, terminating % 91.44/91.29 eprover: CPU time limit exceeded, terminating % 93.55/93.30 eprover: CPU time limit exceeded, terminating % 95.56/95.32 eprover: CPU time limit exceeded, terminating % 97.57/97.34 eprover: CPU time limit exceeded, terminating % 99.62/99.35 eprover: CPU time limit exceeded, terminating % 101.58/101.36 eprover: CPU time limit exceeded, terminating % 103.60/103.39 eprover: CPU time limit exceeded, terminating % 105.70/105.41 eprover: CPU time limit exceeded, terminating % 107.73/107.42 eprover: CPU time limit exceeded, terminating % 109.71/109.44 eprover: CPU time limit exceeded, terminating % 111.73/111.45 eprover: CPU time limit exceeded, terminating % 113.76/113.46 eprover: CPU time limit exceeded, terminating % 115.74/115.48 eprover: CPU time limit exceeded, terminating % 117.78/117.49 eprover: CPU time limit exceeded, terminating % 119.85/119.50 eprover: CPU time limit exceeded, terminating % 121.88/121.51 eprover: CPU time limit exceeded, terminating % 123.90/123.52 eprover: CPU time limit exceeded, terminating % 125.92/125.53 eprover: CPU time limit exceeded, terminating % 127.92/127.54 eprover: CPU time limit exceeded, terminating % 129.93/129.55 eprover: CPU time limit exceeded, terminating % 131.95/131.56 eprover: CPU time limit exceeded, terminating % 133.97/133.57 eprover: CPU time limit exceeded, terminating % 135.99/135.58 eprover: CPU time limit exceeded, terminating % 137.99/137.59 eprover: CPU time limit exceeded, terminating % 140.11/139.60 eprover: CPU time limit exceeded, terminating % 142.05/141.61 eprover: CPU time limit exceeded, terminating % 144.14/143.62 eprover: CPU time limit exceeded, terminating % 146.13/145.63 eprover: CPU time limit exceeded, terminating % 148.16/147.64 eprover: CPU time limit exceeded, terminating % 150.16/149.65 eprover: CPU time limit exceeded, terminating % 152.19/151.67 eprover: CPU time limit exceeded, terminating % 154.24/153.68 eprover: CPU time limit exceeded, terminating % 156.22/155.69 eprover: CPU time limit exceeded, terminating % 158.27/157.69 eprover: CPU time limit exceeded, terminating % 160.36/159.70 eprover: CPU time limit exceeded, terminating % 162.39/161.71 eprover: CPU time limit exceeded, terminating % 164.36/163.73 eprover: CPU time limit exceeded, terminating % 166.40/165.74 eprover: CPU time limit exceeded, terminating % 168.43/167.75 eprover: CPU time limit exceeded, terminating % 170.43/169.76 eprover: CPU time limit exceeded, terminating % 172.44/171.77 eprover: CPU time limit exceeded, terminating % 174.46/173.78 eprover: CPU time limit exceeded, terminating % 176.54/175.79 eprover: CPU time limit exceeded, terminating % 178.50/177.80 eprover: CPU time limit exceeded, terminating % 180.59/179.81 eprover: CPU time limit exceeded, terminating % 182.62/181.82 eprover: CPU time limit exceeded, terminating % 184.62/183.83 eprover: CPU time limit exceeded, terminating % 186.64/185.84 eprover: CPU time limit exceeded, terminating % 188.65/187.87 eprover: CPU time limit exceeded, terminating % 190.63/189.88 eprover: CPU time limit exceeded, terminating % 192.74/191.89 eprover: CPU time limit exceeded, terminating % 194.77/193.91 eprover: CPU time limit exceeded, terminating % 196.77/195.92 eprover: CPU time limit exceeded, terminating % 198.81/197.94 eprover: CPU time limit exceeded, terminating % 200.78/199.95 eprover: CPU time limit exceeded, terminating % 202.81/201.96 eprover: CPU time limit exceeded, terminating % 204.82/203.97 eprover: CPU time limit exceeded, terminating % 206.89/205.98 eprover: CPU time limit exceeded, terminating % 208.84/207.99 eprover: CPU time limit exceeded, terminating % 210.94/210.01 eprover: CPU time limit exceeded, terminating % 212.95/212.02 eprover: CPU time limit exceeded, terminating % 214.95/214.03 eprover: CPU time limit exceeded, terminating % 216.97/216.05 eprover: CPU time limit exceeded, terminating % 218.97/218.06 eprover: CPU time limit exceeded, terminating % 221.01/220.07 eprover: CPU time limit exceeded, terminating % 223.09/222.10 eprover: CPU time limit exceeded, terminating % 225.11/224.11 eprover: CPU time limit exceeded, terminating % 227.12/226.14 eprover: CPU time limit exceeded, terminating % 227.43/227.42 Infinox, version 1.0, 2009-07-20. % 227.43/227.42 +++ PROBLEM: /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.43/227.42 Reading '/export/starexec/sandbox2/benchmark/theBenchmark.p' ... OK % 227.43/227.42 +++ SOLVING: /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.43/227.42 InjNotSurj % 227.43/227.42 SurjNotInj % 227.43/227.42 +++ RESULT: FinitelyCounterUnsatisfiable % 227.43/227.42 % SZS status FiniteTheorem %------------------------------------------------------------------------------