%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : NLP084-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_infinox %s % Computer : n028.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:32:18 EDT 2022 % Result : Timeout 290.43s 291.49s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP084-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_infinox %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 08:05:45 EDT 2022 % 0.12/0.33 % CPUTime : % 2.83/3.02 eprover: CPU time limit exceeded, terminating % 4.80/5.03 eprover: CPU time limit exceeded, terminating % 6.83/7.04 eprover: CPU time limit exceeded, terminating % 8.82/9.05 eprover: CPU time limit exceeded, terminating % 10.88/11.06 eprover: CPU time limit exceeded, terminating % 12.90/13.08 eprover: CPU time limit exceeded, terminating % 14.87/15.08 eprover: CPU time limit exceeded, terminating % 16.88/17.10 eprover: CPU time limit exceeded, terminating % 18.87/19.10 eprover: CPU time limit exceeded, terminating % 20.90/21.11 eprover: CPU time limit exceeded, terminating % 22.90/23.13 eprover: CPU time limit exceeded, terminating % 24.95/25.14 eprover: CPU time limit exceeded, terminating % 26.96/27.16 eprover: CPU time limit exceeded, terminating % 28.98/29.17 eprover: CPU time limit exceeded, terminating % 30.99/31.18 eprover: CPU time limit exceeded, terminating % 33.01/33.19 eprover: CPU time limit exceeded, terminating % 35.00/35.19 eprover: CPU time limit exceeded, terminating % 37.01/37.20 eprover: CPU time limit exceeded, terminating % 39.02/39.22 eprover: CPU time limit exceeded, terminating % 40.99/41.23 eprover: CPU time limit exceeded, terminating % 43.07/43.23 eprover: CPU time limit exceeded, terminating % 45.07/45.25 eprover: CPU time limit exceeded, terminating % 47.07/47.27 eprover: CPU time limit exceeded, terminating % 49.09/49.28 eprover: CPU time limit exceeded, terminating % 51.07/51.29 eprover: CPU time limit exceeded, terminating % 53.13/53.30 eprover: CPU time limit exceeded, terminating % 55.07/55.32 eprover: CPU time limit exceeded, terminating % 57.14/57.33 eprover: CPU time limit exceeded, terminating % 59.08/59.34 eprover: CPU time limit exceeded, terminating % 61.15/61.35 eprover: CPU time limit exceeded, terminating % 63.11/63.36 eprover: CPU time limit exceeded, terminating % 65.11/65.37 eprover: CPU time limit exceeded, terminating % 67.21/67.38 eprover: CPU time limit exceeded, terminating % 69.16/69.39 eprover: CPU time limit exceeded, terminating % 71.23/71.40 eprover: CPU time limit exceeded, terminating % 73.22/73.41 eprover: CPU time limit exceeded, terminating % 75.23/75.42 eprover: CPU time limit exceeded, terminating % 77.24/77.44 eprover: CPU time limit exceeded, terminating % 79.23/79.45 eprover: CPU time limit exceeded, terminating % 81.24/81.46 eprover: CPU time limit exceeded, terminating % 83.23/83.47 eprover: CPU time limit exceeded, terminating % 85.22/85.48 eprover: CPU time limit exceeded, terminating % 87.31/87.49 eprover: CPU time limit exceeded, terminating % 89.33/89.50 eprover: CPU time limit exceeded, terminating % 91.34/91.51 eprover: CPU time limit exceeded, terminating % 93.31/93.52 eprover: CPU time limit exceeded, terminating % 95.34/95.53 eprover: CPU time limit exceeded, terminating % 97.36/97.54 eprover: CPU time limit exceeded, terminating % 99.34/99.55 eprover: CPU time limit exceeded, terminating % 101.33/101.57 eprover: CPU time limit exceeded, terminating % 103.31/103.59 eprover: CPU time limit exceeded, terminating % 105.42/105.60 eprover: CPU time limit exceeded, terminating % 107.42/107.61 eprover: CPU time limit exceeded, terminating % 109.42/109.62 eprover: CPU time limit exceeded, terminating % 111.40/111.65 eprover: CPU time limit exceeded, terminating % 113.39/113.67 eprover: CPU time limit exceeded, terminating % 115.41/115.67 eprover: CPU time limit exceeded, terminating % 117.42/117.68 eprover: CPU time limit exceeded, terminating % 119.50/119.69 eprover: CPU time limit exceeded, terminating % 121.50/121.71 eprover: CPU time limit exceeded, terminating % 123.52/123.71 eprover: CPU time limit exceeded, terminating % 125.51/125.72 eprover: CPU time limit exceeded, terminating % 127.52/127.73 eprover: CPU time limit exceeded, terminating % 129.50/129.75 eprover: CPU time limit exceeded, terminating % 131.50/131.76 eprover: CPU time limit exceeded, terminating % 133.53/133.77 eprover: CPU time limit exceeded, terminating % 135.49/135.78 eprover: CPU time limit exceeded, terminating % 137.54/137.79 eprover: CPU time limit exceeded, terminating % 139.52/139.80 eprover: CPU time limit exceeded, terminating % 141.60/141.81 eprover: CPU time limit exceeded, terminating % 143.62/143.82 eprover: CPU time limit exceeded, terminating % 145.60/145.83 eprover: CPU time limit exceeded, terminating % 147.65/147.84 eprover: CPU time limit exceeded, terminating % 149.62/149.85 eprover: CPU time limit exceeded, terminating % 151.65/151.86 eprover: CPU time limit exceeded, terminating % 153.67/153.88 eprover: CPU time limit exceeded, terminating % 155.70/155.89 eprover: CPU time limit exceeded, terminating % 157.68/157.90 eprover: CPU time limit exceeded, terminating % 159.70/159.91 eprover: CPU time limit exceeded, terminating % 161.72/161.92 eprover: CPU time limit exceeded, terminating % 163.74/163.95 eprover: CPU time limit exceeded, terminating % 165.73/165.95 eprover: CPU time limit exceeded, terminating % 167.75/167.96 eprover: CPU time limit exceeded, terminating % 169.73/169.97 eprover: CPU time limit exceeded, terminating % 171.77/171.98 eprover: CPU time limit exceeded, terminating % 173.81/173.99 eprover: CPU time limit exceeded, terminating % 175.77/176.00 eprover: CPU time limit exceeded, terminating % 177.81/178.02 eprover: CPU time limit exceeded, terminating % 179.82/180.03 eprover: CPU time limit exceeded, terminating % 181.82/182.03 eprover: CPU time limit exceeded, terminating % 183.85/184.04 eprover: CPU time limit exceeded, terminating % 185.88/186.06 eprover: CPU time limit exceeded, terminating % 187.86/188.06 eprover: CPU time limit exceeded, terminating % 189.91/190.07 eprover: CPU time limit exceeded, terminating % 191.88/192.08 eprover: CPU time limit exceeded, terminating % 193.91/194.09 eprover: CPU time limit exceeded, terminating % 195.88/196.10 eprover: CPU time limit exceeded, terminating % 197.90/198.11 eprover: CPU time limit exceeded, terminating % 199.88/200.12 eprover: CPU time limit exceeded, terminating % 201.91/202.13 eprover: CPU time limit exceeded, terminating % 203.96/204.14 eprover: CPU time limit exceeded, terminating % 205.97/206.15 eprover: CPU time limit exceeded, terminating % 207.92/208.16 eprover: CPU time limit exceeded, terminating % 209.98/210.17 eprover: CPU time limit exceeded, terminating % 212.01/212.17 eprover: CPU time limit exceeded, terminating % 213.98/214.18 eprover: CPU time limit exceeded, terminating % 216.01/216.19 eprover: CPU time limit exceeded, terminating % 217.97/218.20 eprover: CPU time limit exceeded, terminating % 220.00/220.21 eprover: CPU time limit exceeded, terminating % 222.03/222.22 eprover: CPU time limit exceeded, terminating % 224.05/224.22 eprover: CPU time limit exceeded, terminating % 226.10/226.23 eprover: CPU time limit exceeded, terminating % 228.03/228.24 eprover: CPU time limit exceeded, terminating % 230.07/230.25 eprover: CPU time limit exceeded, terminating % 232.11/232.26 eprover: CPU time limit exceeded, terminating % 234.12/234.28 eprover: CPU time limit exceeded, terminating % 236.14/236.29 eprover: CPU time limit exceeded, terminating % 238.09/238.30 eprover: CPU time limit exceeded, terminating % 240.14/240.31 eprover: CPU time limit exceeded, terminating % 242.16/242.32 eprover: CPU time limit exceeded, terminating % 244.18/244.33 eprover: CPU time limit exceeded, terminating % 246.18/246.34 eprover: CPU time limit exceeded, terminating % 248.17/248.35 eprover: CPU time limit exceeded, terminating % 250.21/250.36 eprover: CPU time limit exceeded, terminating % 252.17/252.36 eprover: CPU time limit exceeded, terminating % 254.19/254.37 eprover: CPU time limit exceeded, terminating % 259.75/259.87 eprover: CPU time limit exceeded, terminating % 270.40/270.53 eprover: CPU time limit exceeded, terminating % 272.46/272.61 eprover: CPU time limit exceeded, terminating % 278.29/278.41 eprover: CPU time limit exceeded, terminating % 280.36/280.47 eprover: CPU time limit exceeded, terminating % 282.40/282.53 eprover: CPU time limit exceeded, terminating % 290.43/291.49 Infinox, version 1.0, 2009-07-20. % 290.43/291.49 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 290.43/291.49 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 290.43/291.49 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 290.43/291.49 InjNotSurj % 290.43/291.49 SurjNotInj % 290.43/291.49 Serial % 290.43/291.49 Trans % 290.43/291.49 Auto % 290.43/291.49 Leo % 290.43/291.49 ... % 290.43/291.49 % 290.43/291.49 No.of.Axioms: 99 % 290.43/291.49 % 290.43/291.49 Length.of.Defs: 0 % 290.43/291.49 % 290.43/291.49 Contains.Choice.Funs: false % 290.43/291.49 .......................................................................... % 290.43/291.49 % 290.43/291.49 % 290.43/291.49 NO EXECUTABLE FOR PROVER E FOUND % 290.43/291.49 % SZS status Error for /tmp/Infinox_2904/exportstarexecsandboxbenchmarktheBenchmarkp_TEMP/axiomfile : (rf:0,axioms:99,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:13,atp_calls_frequency:10,ordering:none,proof_output:0,clause_count:964,loop_count:0,foatp_calls:1,translation:fof_full) % 290.43/291.49 +++ RESULT: GaveUp %------------------------------------------------------------------------------