%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : NLP057-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_infinox %s % Computer : n018.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:04 EDT 2022 % Result : Timeout 285.72s 285.36s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP057-1 : TPTP v8.1.0. Released v2.4.0. % 0.04/0.13 % Command : run_infinox %s % 0.14/0.34 % Computer : n018.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Thu Jun 30 18:05:32 EDT 2022 % 0.14/0.34 % CPUTime : % 3.02/3.23 eprover: CPU time limit exceeded, terminating % 5.05/5.24 eprover: CPU time limit exceeded, terminating % 7.08/7.25 eprover: CPU time limit exceeded, terminating % 9.10/9.25 eprover: CPU time limit exceeded, terminating % 11.07/11.26 eprover: CPU time limit exceeded, terminating % 13.12/13.27 eprover: CPU time limit exceeded, terminating % 15.13/15.28 eprover: CPU time limit exceeded, terminating % 17.12/17.29 eprover: CPU time limit exceeded, terminating % 19.11/19.29 eprover: CPU time limit exceeded, terminating % 21.14/21.30 eprover: CPU time limit exceeded, terminating % 23.14/23.31 eprover: CPU time limit exceeded, terminating % 25.13/25.31 eprover: CPU time limit exceeded, terminating % 27.14/27.32 eprover: CPU time limit exceeded, terminating % 29.17/29.33 eprover: CPU time limit exceeded, terminating % 31.22/31.34 eprover: CPU time limit exceeded, terminating % 33.19/33.34 eprover: CPU time limit exceeded, terminating % 35.18/35.35 eprover: CPU time limit exceeded, terminating % 37.23/37.36 eprover: CPU time limit exceeded, terminating % 39.24/39.37 eprover: CPU time limit exceeded, terminating % 41.28/41.37 eprover: CPU time limit exceeded, terminating % 43.29/43.38 eprover: CPU time limit exceeded, terminating % 45.25/45.39 eprover: CPU time limit exceeded, terminating % 47.29/47.39 eprover: CPU time limit exceeded, terminating % 49.31/49.40 eprover: CPU time limit exceeded, terminating % 51.26/51.41 eprover: CPU time limit exceeded, terminating % 53.29/53.42 eprover: CPU time limit exceeded, terminating % 55.32/55.42 eprover: CPU time limit exceeded, terminating % 57.35/57.43 eprover: CPU time limit exceeded, terminating % 59.35/59.44 eprover: CPU time limit exceeded, terminating % 61.33/61.44 eprover: CPU time limit exceeded, terminating % 63.37/63.45 eprover: CPU time limit exceeded, terminating % 65.39/65.46 eprover: CPU time limit exceeded, terminating % 67.40/67.47 eprover: CPU time limit exceeded, terminating % 69.40/69.48 eprover: CPU time limit exceeded, terminating % 71.41/71.48 eprover: CPU time limit exceeded, terminating % 73.42/73.49 eprover: CPU time limit exceeded, terminating % 75.46/75.50 eprover: CPU time limit exceeded, terminating % 77.42/77.50 eprover: CPU time limit exceeded, terminating % 79.41/79.51 eprover: CPU time limit exceeded, terminating % 81.47/81.52 eprover: CPU time limit exceeded, terminating % 83.44/83.53 eprover: CPU time limit exceeded, terminating % 85.47/85.53 eprover: CPU time limit exceeded, terminating % 87.47/87.54 eprover: CPU time limit exceeded, terminating % 89.45/89.55 eprover: CPU time limit exceeded, terminating % 91.54/91.56 eprover: CPU time limit exceeded, terminating % 93.53/93.56 eprover: CPU time limit exceeded, terminating % 95.54/95.57 eprover: CPU time limit exceeded, terminating % 97.54/97.58 eprover: CPU time limit exceeded, terminating % 99.59/99.58 eprover: CPU time limit exceeded, terminating % 101.57/101.59 eprover: CPU time limit exceeded, terminating % 103.57/103.60 eprover: CPU time limit exceeded, terminating % 105.62/105.61 eprover: CPU time limit exceeded, terminating % 107.57/107.61 eprover: CPU time limit exceeded, terminating % 109.56/109.62 eprover: CPU time limit exceeded, terminating % 111.66/111.63 eprover: CPU time limit exceeded, terminating % 113.65/113.64 eprover: CPU time limit exceeded, terminating % 115.68/115.64 eprover: CPU time limit exceeded, terminating % 117.67/117.65 eprover: CPU time limit exceeded, terminating % 119.69/119.66 eprover: CPU time limit exceeded, terminating % 121.69/121.66 eprover: CPU time limit exceeded, terminating % 123.69/123.67 eprover: CPU time limit exceeded, terminating % 125.72/125.68 eprover: CPU time limit exceeded, terminating % 129.29/129.23 eprover: CPU time limit exceeded, terminating % 137.22/137.16 eprover: CPU time limit exceeded, terminating % 139.27/139.19 eprover: CPU time limit exceeded, terminating % 143.15/143.11 eprover: CPU time limit exceeded, terminating % 145.21/145.15 eprover: CPU time limit exceeded, terminating % 147.27/147.18 eprover: CPU time limit exceeded, terminating % 149.57/149.53 eprover: CPU time limit exceeded, terminating % 151.79/151.68 eprover: CPU time limit exceeded, terminating % 153.90/153.78 eprover: CPU time limit exceeded, terminating % 155.99/155.92 eprover: CPU time limit exceeded, terminating % 158.13/158.02 eprover: CPU time limit exceeded, terminating % 160.19/160.11 eprover: CPU time limit exceeded, terminating % 162.22/162.12 eprover: CPU time limit exceeded, terminating % 164.28/164.13 eprover: CPU time limit exceeded, terminating % 166.19/166.14 eprover: CPU time limit exceeded, terminating % 168.50/168.36 eprover: CPU time limit exceeded, terminating % 170.50/170.37 eprover: CPU time limit exceeded, terminating % 172.54/172.38 eprover: CPU time limit exceeded, terminating % 174.52/174.38 eprover: CPU time limit exceeded, terminating % 176.54/176.39 eprover: CPU time limit exceeded, terminating % 178.55/178.40 eprover: CPU time limit exceeded, terminating % 180.56/180.41 eprover: CPU time limit exceeded, terminating % 182.54/182.42 eprover: CPU time limit exceeded, terminating % 184.59/184.42 eprover: CPU time limit exceeded, terminating % 186.56/186.43 eprover: CPU time limit exceeded, terminating % 188.61/188.44 eprover: CPU time limit exceeded, terminating % 190.59/190.45 eprover: CPU time limit exceeded, terminating % 192.61/192.46 eprover: CPU time limit exceeded, terminating % 194.66/194.46 eprover: CPU time limit exceeded, terminating % 196.68/196.47 eprover: CPU time limit exceeded, terminating % 198.66/198.48 eprover: CPU time limit exceeded, terminating % 200.68/200.49 eprover: CPU time limit exceeded, terminating % 202.68/202.50 eprover: CPU time limit exceeded, terminating % 204.68/204.50 eprover: CPU time limit exceeded, terminating % 206.72/206.51 eprover: CPU time limit exceeded, terminating % 208.74/208.52 eprover: CPU time limit exceeded, terminating % 210.71/210.53 eprover: CPU time limit exceeded, terminating % 212.74/212.54 eprover: CPU time limit exceeded, terminating % 214.76/214.54 eprover: CPU time limit exceeded, terminating % 216.75/216.55 eprover: CPU time limit exceeded, terminating % 218.81/218.56 eprover: CPU time limit exceeded, terminating % 220.78/220.57 eprover: CPU time limit exceeded, terminating % 222.80/222.58 eprover: CPU time limit exceeded, terminating % 224.81/224.58 eprover: CPU time limit exceeded, terminating % 226.80/226.59 eprover: CPU time limit exceeded, terminating % 228.84/228.60 eprover: CPU time limit exceeded, terminating % 230.82/230.61 eprover: CPU time limit exceeded, terminating % 232.83/232.62 eprover: CPU time limit exceeded, terminating % 234.87/234.62 eprover: CPU time limit exceeded, terminating % 236.87/236.63 eprover: CPU time limit exceeded, terminating % 238.92/238.64 eprover: CPU time limit exceeded, terminating % 240.92/240.65 eprover: CPU time limit exceeded, terminating % 242.95/242.66 eprover: CPU time limit exceeded, terminating % 244.94/244.66 eprover: CPU time limit exceeded, terminating % 246.96/246.67 eprover: CPU time limit exceeded, terminating % 248.98/248.68 eprover: CPU time limit exceeded, terminating % 250.98/250.69 eprover: CPU time limit exceeded, terminating % 252.96/252.70 eprover: CPU time limit exceeded, terminating % 254.99/254.70 eprover: CPU time limit exceeded, terminating % 256.97/256.71 eprover: CPU time limit exceeded, terminating % 258.99/258.72 eprover: CPU time limit exceeded, terminating % 261.06/260.84 eprover: CPU time limit exceeded, terminating % 263.17/262.84 eprover: CPU time limit exceeded, terminating % 265.15/264.85 eprover: CPU time limit exceeded, terminating % 267.23/266.95 eprover: CPU time limit exceeded, terminating % 269.30/268.96 eprover: CPU time limit exceeded, terminating % 271.29/270.97 eprover: CPU time limit exceeded, terminating % 273.40/273.10 eprover: CPU time limit exceeded, terminating % 275.41/275.11 eprover: CPU time limit exceeded, terminating % 277.44/277.12 eprover: CPU time limit exceeded, terminating % 279.54/279.25 eprover: CPU time limit exceeded, terminating % 281.58/281.25 eprover: CPU time limit exceeded, terminating % 283.58/283.26 eprover: CPU time limit exceeded, terminating % 285.72/285.36 eprover: CPU time limit exceeded, terminating % 287.71/287.37 eprover: CPU time limit exceeded, terminating % 289.74/289.38 eprover: CPU time limit exceeded, terminating % 293.01/293.61 Infinox, version 1.0, 2009-07-20. % 293.01/293.61 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 293.01/293.61 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 293.01/293.61 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 293.01/293.61 InjNotSurj % 293.01/293.61 SurjNotInj % 293.01/293.61 Serial % 293.01/293.61 Trans % 293.01/293.61 Auto % 293.01/293.61 Leo % 293.01/293.61 ... % 293.01/293.61 % 293.01/293.61 No.of.Axioms: 93 % 293.01/293.61 % 293.01/293.61 Length.of.Defs: 0 % 293.01/293.61 % 293.01/293.61 Contains.Choice.Funs: false % 293.01/293.61 .................................................................. % 293.01/293.61 % 293.01/293.61 % 293.01/293.61 NO EXECUTABLE FOR PROVER E FOUND % 293.01/293.61 % SZS status Error for /tmp/Infinox_15494/exportstarexecsandboxbenchmarktheBenchmarkp_TEMP/axiomfile : (rf:0,axioms:93,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:14,atp_calls_frequency:10,ordering:none,proof_output:0,clause_count:943,loop_count:0,foatp_calls:1,translation:fof_full) % 293.01/293.61 +++ RESULT: GaveUp %------------------------------------------------------------------------------