%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : NLP173-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_infinox %s % Computer : n029.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 : Mon Jul 18 02:33:09 EDT 2022 % Result : Unknown 66.56s 66.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP173-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_infinox %s % 0.13/0.33 % Computer : n029.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Fri Jul 1 09:28:24 EDT 2022 % 0.13/0.33 % CPUTime : % 2.72/2.91 eprover: CPU time limit exceeded, terminating % 4.75/4.92 eprover: CPU time limit exceeded, terminating % 6.75/6.93 eprover: CPU time limit exceeded, terminating % 8.71/8.95 eprover: CPU time limit exceeded, terminating % 10.73/10.96 eprover: CPU time limit exceeded, terminating % 12.76/12.96 eprover: CPU time limit exceeded, terminating % 14.93/15.15 eprover: CPU time limit exceeded, terminating % 18.41/18.60 eprover: CPU time limit exceeded, terminating % 20.43/20.61 eprover: CPU time limit exceeded, terminating % 22.68/22.88 eprover: CPU time limit exceeded, terminating % 25.30/25.49 eprover: CPU time limit exceeded, terminating % 33.86/34.05 eprover: CPU time limit exceeded, terminating % 36.28/36.45 eprover: CPU time limit exceeded, terminating % 38.22/38.47 eprover: CPU time limit exceeded, terminating % 40.42/40.66 eprover: CPU time limit exceeded, terminating % 42.46/42.67 eprover: CPU time limit exceeded, terminating % 44.70/44.89 eprover: CPU time limit exceeded, terminating % 46.69/46.90 eprover: CPU time limit exceeded, terminating % 48.72/48.92 eprover: CPU time limit exceeded, terminating % 50.74/50.93 eprover: CPU time limit exceeded, terminating % 52.74/52.95 eprover: CPU time limit exceeded, terminating % 54.77/54.97 eprover: CPU time limit exceeded, terminating % 66.56/66.75 infinox: equinox: runProcess: runInteractiveProcess: exec: does not exist (No such file or directory) % 66.56/66.76 Infinox, version 1.0, 2009-07-20. % 66.56/66.76 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 66.56/66.76 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 66.56/66.76 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 66.56/66.76 InjNotSurj % 66.56/66.76 SurjNotInj % 66.56/66.76 Serial % 66.56/66.76 Trans % 66.56/66.76 Auto %------------------------------------------------------------------------------