%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : NLP256+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_infinox %s % Computer : n005.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:58 EDT 2022 % Result : Unknown 156.92s 156.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP256+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_infinox %s % 0.12/0.34 % Computer : n005.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Fri Jul 1 05:09:22 EDT 2022 % 0.12/0.34 % CPUTime : % 28.73/28.89 eprover: CPU time limit exceeded, terminating % 32.86/32.96 eprover: CPU time limit exceeded, terminating % 35.81/35.94 eprover: CPU time limit exceeded, terminating % 39.85/39.91 eprover: CPU time limit exceeded, terminating % 41.82/41.92 eprover: CPU time limit exceeded, terminating % 44.20/44.33 eprover: CPU time limit exceeded, terminating % 47.18/47.27 eprover: CPU time limit exceeded, terminating % 52.50/52.54 eprover: CPU time limit exceeded, terminating % 54.44/54.56 eprover: CPU time limit exceeded, terminating % 58.40/58.45 eprover: CPU time limit exceeded, terminating % 60.39/60.46 eprover: CPU time limit exceeded, terminating % 63.14/63.16 eprover: CPU time limit exceeded, terminating % 65.16/65.17 eprover: CPU time limit exceeded, terminating % 67.13/67.18 eprover: CPU time limit exceeded, terminating % 69.16/69.20 eprover: CPU time limit exceeded, terminating % 71.16/71.21 eprover: CPU time limit exceeded, terminating % 73.15/73.22 eprover: CPU time limit exceeded, terminating % 78.85/78.84 eprover: CPU time limit exceeded, terminating % 80.79/80.85 eprover: CPU time limit exceeded, terminating % 83.29/83.28 eprover: CPU time limit exceeded, terminating % 85.63/85.63 eprover: CPU time limit exceeded, terminating % 88.76/88.78 eprover: CPU time limit exceeded, terminating % 91.19/91.17 eprover: CPU time limit exceeded, terminating % 93.22/93.17 eprover: CPU time limit exceeded, terminating % 95.38/95.36 eprover: CPU time limit exceeded, terminating % 97.57/97.55 eprover: CPU time limit exceeded, terminating % 99.73/99.73 eprover: CPU time limit exceeded, terminating % 102.09/102.08 eprover: CPU time limit exceeded, terminating % 104.10/104.09 eprover: CPU time limit exceeded, terminating % 106.14/106.09 eprover: CPU time limit exceeded, terminating % 109.08/109.04 eprover: CPU time limit exceeded, terminating % 111.10/111.05 eprover: CPU time limit exceeded, terminating % 117.77/117.75 eprover: CPU time limit exceeded, terminating % 124.71/124.60 eprover: CPU time limit exceeded, terminating % 156.63/156.03 infinox: equinox: runProcess: runInteractiveProcess: exec: does not exist (No such file or directory) % 156.63/156.04 Infinox, version 1.0, 2009-07-20. % 156.63/156.04 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 156.63/156.04 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 156.63/156.04 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 156.63/156.04 InjNotSurj % 156.63/156.04 SurjNotInj % 156.63/156.04 Serial % 156.63/156.04 Trans % 156.63/156.04 Auto %------------------------------------------------------------------------------