%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : NLP074-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_infinox %s % Computer : n015.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:13 EDT 2022 % Result : Timeout 287.44s 288.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NLP074-1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_infinox %s % 0.12/0.33 % Computer : n015.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 12:19:28 EDT 2022 % 0.12/0.33 % CPUTime : % 2.95/3.20 eprover: CPU time limit exceeded, terminating % 5.02/5.21 eprover: CPU time limit exceeded, terminating % 7.03/7.22 eprover: CPU time limit exceeded, terminating % 9.02/9.25 eprover: CPU time limit exceeded, terminating % 11.06/11.26 eprover: CPU time limit exceeded, terminating % 13.03/13.28 eprover: CPU time limit exceeded, terminating % 15.06/15.29 eprover: CPU time limit exceeded, terminating % 17.07/17.30 eprover: CPU time limit exceeded, terminating % 19.08/19.32 eprover: CPU time limit exceeded, terminating % 21.03/21.33 eprover: CPU time limit exceeded, terminating % 23.06/23.34 eprover: CPU time limit exceeded, terminating % 25.11/25.35 eprover: CPU time limit exceeded, terminating % 27.15/27.36 eprover: CPU time limit exceeded, terminating % 29.11/29.37 eprover: CPU time limit exceeded, terminating % 31.15/31.38 eprover: CPU time limit exceeded, terminating % 33.11/33.39 eprover: CPU time limit exceeded, terminating % 35.17/35.40 eprover: CPU time limit exceeded, terminating % 37.20/37.41 eprover: CPU time limit exceeded, terminating % 39.21/39.42 eprover: CPU time limit exceeded, terminating % 41.13/41.43 eprover: CPU time limit exceeded, terminating % 43.23/43.43 eprover: CPU time limit exceeded, terminating % 45.23/45.44 eprover: CPU time limit exceeded, terminating % 47.19/47.45 eprover: CPU time limit exceeded, terminating % 49.22/49.46 eprover: CPU time limit exceeded, terminating % 51.20/51.47 eprover: CPU time limit exceeded, terminating % 53.24/53.48 eprover: CPU time limit exceeded, terminating % 55.28/55.49 eprover: CPU time limit exceeded, terminating % 57.24/57.50 eprover: CPU time limit exceeded, terminating % 59.33/59.51 eprover: CPU time limit exceeded, terminating % 61.31/61.53 eprover: CPU time limit exceeded, terminating % 63.34/63.54 eprover: CPU time limit exceeded, terminating % 65.36/65.56 eprover: CPU time limit exceeded, terminating % 67.34/67.57 eprover: CPU time limit exceeded, terminating % 69.36/69.58 eprover: CPU time limit exceeded, terminating % 71.39/71.58 eprover: CPU time limit exceeded, terminating % 73.38/73.59 eprover: CPU time limit exceeded, terminating % 75.38/75.60 eprover: CPU time limit exceeded, terminating % 77.41/77.61 eprover: CPU time limit exceeded, terminating % 79.37/79.61 eprover: CPU time limit exceeded, terminating % 81.40/81.62 eprover: CPU time limit exceeded, terminating % 83.42/83.63 eprover: CPU time limit exceeded, terminating % 85.45/85.64 eprover: CPU time limit exceeded, terminating % 87.48/87.65 eprover: CPU time limit exceeded, terminating % 89.50/89.66 eprover: CPU time limit exceeded, terminating % 91.47/91.68 eprover: CPU time limit exceeded, terminating % 93.51/93.70 eprover: CPU time limit exceeded, terminating % 95.49/95.71 eprover: CPU time limit exceeded, terminating % 97.53/97.72 eprover: CPU time limit exceeded, terminating % 99.50/99.73 eprover: CPU time limit exceeded, terminating % 101.57/101.74 eprover: CPU time limit exceeded, terminating % 103.57/103.75 eprover: CPU time limit exceeded, terminating % 105.57/105.76 eprover: CPU time limit exceeded, terminating % 107.55/107.77 eprover: CPU time limit exceeded, terminating % 109.58/109.77 eprover: CPU time limit exceeded, terminating % 111.58/111.78 eprover: CPU time limit exceeded, terminating % 113.60/113.79 eprover: CPU time limit exceeded, terminating % 115.59/115.81 eprover: CPU time limit exceeded, terminating % 117.60/117.82 eprover: CPU time limit exceeded, terminating % 119.58/119.82 eprover: CPU time limit exceeded, terminating % 121.59/121.83 eprover: CPU time limit exceeded, terminating % 123.65/123.84 eprover: CPU time limit exceeded, terminating % 125.65/125.85 eprover: CPU time limit exceeded, terminating % 127.68/127.86 eprover: CPU time limit exceeded, terminating % 129.70/129.87 eprover: CPU time limit exceeded, terminating % 131.69/131.88 eprover: CPU time limit exceeded, terminating % 133.71/133.89 eprover: CPU time limit exceeded, terminating % 135.69/135.90 eprover: CPU time limit exceeded, terminating % 137.76/137.92 eprover: CPU time limit exceeded, terminating % 139.76/139.93 eprover: CPU time limit exceeded, terminating % 141.78/141.94 eprover: CPU time limit exceeded, terminating % 143.76/143.95 eprover: CPU time limit exceeded, terminating % 145.72/145.96 eprover: CPU time limit exceeded, terminating % 147.78/147.97 eprover: CPU time limit exceeded, terminating % 149.77/149.98 eprover: CPU time limit exceeded, terminating % 151.79/151.99 eprover: CPU time limit exceeded, terminating % 153.84/154.00 eprover: CPU time limit exceeded, terminating % 155.85/156.01 eprover: CPU time limit exceeded, terminating % 157.86/158.02 eprover: CPU time limit exceeded, terminating % 159.86/160.03 eprover: CPU time limit exceeded, terminating % 161.88/162.04 eprover: CPU time limit exceeded, terminating % 163.86/164.06 eprover: CPU time limit exceeded, terminating % 165.86/166.07 eprover: CPU time limit exceeded, terminating % 167.92/168.08 eprover: CPU time limit exceeded, terminating % 169.95/170.09 eprover: CPU time limit exceeded, terminating % 171.96/172.10 eprover: CPU time limit exceeded, terminating % 173.95/174.11 eprover: CPU time limit exceeded, terminating % 175.94/176.12 eprover: CPU time limit exceeded, terminating % 177.98/178.13 eprover: CPU time limit exceeded, terminating % 180.00/180.14 eprover: CPU time limit exceeded, terminating % 181.93/182.15 eprover: CPU time limit exceeded, terminating % 183.99/184.16 eprover: CPU time limit exceeded, terminating % 186.00/186.17 eprover: CPU time limit exceeded, terminating % 188.05/188.19 eprover: CPU time limit exceeded, terminating % 190.05/190.20 eprover: CPU time limit exceeded, terminating % 192.05/192.21 eprover: CPU time limit exceeded, terminating % 194.06/194.22 eprover: CPU time limit exceeded, terminating % 196.07/196.23 eprover: CPU time limit exceeded, terminating % 198.09/198.24 eprover: CPU time limit exceeded, terminating % 200.09/200.25 eprover: CPU time limit exceeded, terminating % 202.10/202.26 eprover: CPU time limit exceeded, terminating % 204.13/204.27 eprover: CPU time limit exceeded, terminating % 206.10/206.28 eprover: CPU time limit exceeded, terminating % 208.11/208.28 eprover: CPU time limit exceeded, terminating % 210.16/210.29 eprover: CPU time limit exceeded, terminating % 212.15/212.31 eprover: CPU time limit exceeded, terminating % 214.11/214.32 eprover: CPU time limit exceeded, terminating % 216.19/216.34 eprover: CPU time limit exceeded, terminating % 218.20/218.34 eprover: CPU time limit exceeded, terminating % 220.19/220.35 eprover: CPU time limit exceeded, terminating % 222.21/222.36 eprover: CPU time limit exceeded, terminating % 224.24/224.38 eprover: CPU time limit exceeded, terminating % 226.18/226.39 eprover: CPU time limit exceeded, terminating % 228.22/228.40 eprover: CPU time limit exceeded, terminating % 230.25/230.41 eprover: CPU time limit exceeded, terminating % 232.25/232.42 eprover: CPU time limit exceeded, terminating % 234.28/234.44 eprover: CPU time limit exceeded, terminating % 236.24/236.45 eprover: CPU time limit exceeded, terminating % 238.28/238.45 eprover: CPU time limit exceeded, terminating % 240.32/240.46 eprover: CPU time limit exceeded, terminating % 242.32/242.47 eprover: CPU time limit exceeded, terminating % 244.33/244.49 eprover: CPU time limit exceeded, terminating % 246.32/246.49 eprover: CPU time limit exceeded, terminating % 248.33/248.50 eprover: CPU time limit exceeded, terminating % 250.36/250.51 eprover: CPU time limit exceeded, terminating % 252.30/252.52 eprover: CPU time limit exceeded, terminating % 254.39/254.53 eprover: CPU time limit exceeded, terminating % 260.03/260.17 eprover: CPU time limit exceeded, terminating % 271.64/271.88 eprover: CPU time limit exceeded, terminating % 273.67/273.91 eprover: CPU time limit exceeded, terminating % 279.04/279.31 eprover: CPU time limit exceeded, terminating % 283.72/283.93 eprover: CPU time limit exceeded, terminating % 287.44/288.62 Infinox, version 1.0, 2009-07-20. % 287.44/288.62 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 287.44/288.62 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 287.44/288.62 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 287.44/288.62 InjNotSurj % 287.44/288.62 SurjNotInj % 287.44/288.62 Serial % 287.44/288.62 Trans % 287.44/288.62 Auto % 287.44/288.62 Leo % 287.44/288.62 ... % 287.44/288.62 % 287.44/288.62 No.of.Axioms: 82 % 287.44/288.62 % 287.44/288.62 Length.of.Defs: 0 % 287.44/288.62 % 287.44/288.62 Contains.Choice.Funs: false % 287.44/288.62 ........................................................................... % 287.44/288.62 % 287.44/288.62 % 287.44/288.62 NO EXECUTABLE FOR PROVER E FOUND % 287.44/288.62 % SZS status Error for /tmp/Infinox_18311/exportstarexecsandboxbenchmarktheBenchmarkp_TEMP/axiomfile : (rf:0,axioms:82,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:950,loop_count:0,foatp_calls:1,translation:fof_full) % 287.44/288.62 +++ RESULT: GaveUp %------------------------------------------------------------------------------