%------------------------------------------------------------------------------ % File : Infinox---1.0 % Problem : NLP072-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_infinox %s % Computer : n023.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:12 EDT 2022 % Result : Timeout 287.48s 288.07s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP072-1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_infinox %s % 0.12/0.33 % Computer : n023.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 05:49:44 EDT 2022 % 0.12/0.33 % CPUTime : % 3.12/3.36 eprover: CPU time limit exceeded, terminating % 5.11/5.37 eprover: CPU time limit exceeded, terminating % 7.14/7.38 eprover: CPU time limit exceeded, terminating % 9.22/9.39 eprover: CPU time limit exceeded, terminating % 11.16/11.40 eprover: CPU time limit exceeded, terminating % 13.23/13.40 eprover: CPU time limit exceeded, terminating % 15.25/15.41 eprover: CPU time limit exceeded, terminating % 17.24/17.42 eprover: CPU time limit exceeded, terminating % 19.27/19.43 eprover: CPU time limit exceeded, terminating % 21.23/21.44 eprover: CPU time limit exceeded, terminating % 23.27/23.44 eprover: CPU time limit exceeded, terminating % 25.26/25.45 eprover: CPU time limit exceeded, terminating % 27.25/27.46 eprover: CPU time limit exceeded, terminating % 29.27/29.46 eprover: CPU time limit exceeded, terminating % 31.30/31.47 eprover: CPU time limit exceeded, terminating % 33.31/33.48 eprover: CPU time limit exceeded, terminating % 35.37/35.49 eprover: CPU time limit exceeded, terminating % 37.37/37.50 eprover: CPU time limit exceeded, terminating % 39.37/39.50 eprover: CPU time limit exceeded, terminating % 41.39/41.51 eprover: CPU time limit exceeded, terminating % 43.40/43.52 eprover: CPU time limit exceeded, terminating % 45.39/45.53 eprover: CPU time limit exceeded, terminating % 47.43/47.53 eprover: CPU time limit exceeded, terminating % 49.42/49.54 eprover: CPU time limit exceeded, terminating % 51.40/51.55 eprover: CPU time limit exceeded, terminating % 53.41/53.56 eprover: CPU time limit exceeded, terminating % 55.45/55.56 eprover: CPU time limit exceeded, terminating % 57.41/57.57 eprover: CPU time limit exceeded, terminating % 59.49/59.58 eprover: CPU time limit exceeded, terminating % 61.42/61.59 eprover: CPU time limit exceeded, terminating % 63.45/63.59 eprover: CPU time limit exceeded, terminating % 65.45/65.60 eprover: CPU time limit exceeded, terminating % 67.54/67.61 eprover: CPU time limit exceeded, terminating % 69.53/69.62 eprover: CPU time limit exceeded, terminating % 71.52/71.62 eprover: CPU time limit exceeded, terminating % 73.56/73.63 eprover: CPU time limit exceeded, terminating % 75.56/75.64 eprover: CPU time limit exceeded, terminating % 77.57/77.65 eprover: CPU time limit exceeded, terminating % 79.57/79.65 eprover: CPU time limit exceeded, terminating % 81.58/81.66 eprover: CPU time limit exceeded, terminating % 83.59/83.67 eprover: CPU time limit exceeded, terminating % 85.65/85.68 eprover: CPU time limit exceeded, terminating % 87.58/87.68 eprover: CPU time limit exceeded, terminating % 89.66/89.69 eprover: CPU time limit exceeded, terminating % 91.68/91.70 eprover: CPU time limit exceeded, terminating % 93.69/93.70 eprover: CPU time limit exceeded, terminating % 95.67/95.71 eprover: CPU time limit exceeded, terminating % 97.68/97.72 eprover: CPU time limit exceeded, terminating % 99.72/99.73 eprover: CPU time limit exceeded, terminating % 101.72/101.73 eprover: CPU time limit exceeded, terminating % 103.74/103.74 eprover: CPU time limit exceeded, terminating % 105.71/105.75 eprover: CPU time limit exceeded, terminating % 107.71/107.76 eprover: CPU time limit exceeded, terminating % 109.73/109.76 eprover: CPU time limit exceeded, terminating % 111.75/111.77 eprover: CPU time limit exceeded, terminating % 113.72/113.78 eprover: CPU time limit exceeded, terminating % 115.81/115.78 eprover: CPU time limit exceeded, terminating % 117.74/117.79 eprover: CPU time limit exceeded, terminating % 119.76/119.80 eprover: CPU time limit exceeded, terminating % 121.76/121.81 eprover: CPU time limit exceeded, terminating % 123.85/123.81 eprover: CPU time limit exceeded, terminating % 125.87/125.82 eprover: CPU time limit exceeded, terminating % 127.86/127.83 eprover: CPU time limit exceeded, terminating % 129.84/129.84 eprover: CPU time limit exceeded, terminating % 131.85/131.84 eprover: CPU time limit exceeded, terminating % 133.87/133.85 eprover: CPU time limit exceeded, terminating % 135.88/135.86 eprover: CPU time limit exceeded, terminating % 137.90/137.87 eprover: CPU time limit exceeded, terminating % 139.88/139.87 eprover: CPU time limit exceeded, terminating % 141.96/141.88 eprover: CPU time limit exceeded, terminating % 143.87/143.89 eprover: CPU time limit exceeded, terminating % 145.96/145.89 eprover: CPU time limit exceeded, terminating % 147.99/147.90 eprover: CPU time limit exceeded, terminating % 149.99/149.91 eprover: CPU time limit exceeded, terminating % 152.00/151.92 eprover: CPU time limit exceeded, terminating % 153.98/153.92 eprover: CPU time limit exceeded, terminating % 156.03/155.93 eprover: CPU time limit exceeded, terminating % 158.00/157.94 eprover: CPU time limit exceeded, terminating % 160.01/159.95 eprover: CPU time limit exceeded, terminating % 162.03/161.95 eprover: CPU time limit exceeded, terminating % 164.01/163.96 eprover: CPU time limit exceeded, terminating % 166.02/165.97 eprover: CPU time limit exceeded, terminating % 168.05/167.97 eprover: CPU time limit exceeded, terminating % 170.03/169.98 eprover: CPU time limit exceeded, terminating % 172.11/171.99 eprover: CPU time limit exceeded, terminating % 174.06/174.00 eprover: CPU time limit exceeded, terminating % 176.15/176.00 eprover: CPU time limit exceeded, terminating % 178.15/178.01 eprover: CPU time limit exceeded, terminating % 180.17/180.02 eprover: CPU time limit exceeded, terminating % 182.18/182.03 eprover: CPU time limit exceeded, terminating % 184.17/184.03 eprover: CPU time limit exceeded, terminating % 186.17/186.04 eprover: CPU time limit exceeded, terminating % 188.16/188.05 eprover: CPU time limit exceeded, terminating % 190.15/190.05 eprover: CPU time limit exceeded, terminating % 192.18/192.06 eprover: CPU time limit exceeded, terminating % 194.21/194.07 eprover: CPU time limit exceeded, terminating % 196.18/196.08 eprover: CPU time limit exceeded, terminating % 198.25/198.08 eprover: CPU time limit exceeded, terminating % 200.27/200.09 eprover: CPU time limit exceeded, terminating % 202.28/202.10 eprover: CPU time limit exceeded, terminating % 204.29/204.10 eprover: CPU time limit exceeded, terminating % 206.31/206.11 eprover: CPU time limit exceeded, terminating % 208.31/208.12 eprover: CPU time limit exceeded, terminating % 210.31/210.13 eprover: CPU time limit exceeded, terminating % 212.29/212.13 eprover: CPU time limit exceeded, terminating % 214.32/214.14 eprover: CPU time limit exceeded, terminating % 216.29/216.15 eprover: CPU time limit exceeded, terminating % 218.33/218.16 eprover: CPU time limit exceeded, terminating % 220.35/220.16 eprover: CPU time limit exceeded, terminating % 222.34/222.17 eprover: CPU time limit exceeded, terminating % 224.35/224.18 eprover: CPU time limit exceeded, terminating % 226.35/226.18 eprover: CPU time limit exceeded, terminating % 228.35/228.19 eprover: CPU time limit exceeded, terminating % 230.43/230.20 eprover: CPU time limit exceeded, terminating % 232.36/232.21 eprover: CPU time limit exceeded, terminating % 234.47/234.21 eprover: CPU time limit exceeded, terminating % 236.46/236.22 eprover: CPU time limit exceeded, terminating % 238.44/238.23 eprover: CPU time limit exceeded, terminating % 240.46/240.23 eprover: CPU time limit exceeded, terminating % 242.48/242.24 eprover: CPU time limit exceeded, terminating % 244.47/244.25 eprover: CPU time limit exceeded, terminating % 246.46/246.26 eprover: CPU time limit exceeded, terminating % 248.48/248.26 eprover: CPU time limit exceeded, terminating % 250.50/250.27 eprover: CPU time limit exceeded, terminating % 252.52/252.28 eprover: CPU time limit exceeded, terminating % 254.49/254.28 eprover: CPU time limit exceeded, terminating % 259.83/259.57 eprover: CPU time limit exceeded, terminating % 271.11/270.76 eprover: CPU time limit exceeded, terminating % 273.18/272.79 eprover: CPU time limit exceeded, terminating % 278.58/278.27 eprover: CPU time limit exceeded, terminating % 283.71/283.34 eprover: CPU time limit exceeded, terminating % 287.48/288.07 Infinox, version 1.0, 2009-07-20. % 287.48/288.07 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p % 287.48/288.07 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK % 287.48/288.07 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p % 287.48/288.07 InjNotSurj % 287.48/288.07 SurjNotInj % 287.48/288.07 Serial % 287.48/288.07 Trans % 287.48/288.07 Auto % 287.48/288.07 Leo % 287.48/288.07 ... % 287.48/288.07 % 287.48/288.07 No.of.Axioms: 81 % 287.48/288.07 % 287.48/288.07 Length.of.Defs: 0 % 287.48/288.07 % 287.48/288.07 Contains.Choice.Funs: false % 287.48/288.07 ............................................................................. % 287.48/288.07 % 287.48/288.07 % 287.48/288.07 NO EXECUTABLE FOR PROVER E FOUND % 287.48/288.07 % SZS status Error for /tmp/Infinox_32351/exportstarexecsandboxbenchmarktheBenchmarkp_TEMP/axiomfile : (rf:0,axioms:81,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:962,loop_count:0,foatp_calls:1,translation:fof_full) % 287.48/288.07 +++ RESULT: GaveUp %------------------------------------------------------------------------------