%------------------------------------------------------------------------------ % File : Satallax-MaLeS---1.3 % Problem : NUM811^5 : TPTP v7.0.0. Bugfixed v5.2.0. % Transfm : none % Format : tptp:raw % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % Computer : n094.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.625MB % OS : Linux 3.10.0-693.2.2.el7.x86_64 % CPULimit : 300s % DateTime : Mon Jan 8 15:01:21 EST 2018 % Result : Theorem 210.43s % Output : Assurance 0s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM811^5 : TPTP v7.0.0. Bugfixed v5.2.0. % 0.00/0.04 % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % 0.02/0.23 % Computer : n094.star.cs.uiowa.edu % 0.02/0.23 % Model : x86_64 x86_64 % 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.23 % Memory : 32218.625MB % 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.02/0.23 % CPULimit : 300 % 0.02/0.23 % DateTime : Fri Jan 5 14:31:47 CST 2018 % 0.02/0.23 % CPUTime : % 1.51/2.43 % Running -m mode500 for 0.0746741294861 seconds % 1.60/2.51 % Running -m NewStrategy25012 for 1.15038013458 seconds % 2.31/3.82 % Running -m NewStrategy31551 for 7.74439811707 seconds % 11.07/11.59 % Running -m NewStrategy56535 for 0.0329518318176 seconds % 11.07/11.60 % Running -m NewStrategy68939 for 0.553977012634 seconds % 11.61/12.16 % Running -m mode251 for 9.27129101753 seconds % 20.94/21.45 % Running -m NewStrategy72394 for 12.0491919518 seconds % 20.94/21.46 % Running -m mode369 for 0.0164971351624 seconds % 20.94/21.48 % Running -m NewStrategy10189 for 0.0147910118103 seconds % 20.97/21.49 % Running -m NewStrategy31440 for 0.0322110652924 seconds % 20.97/21.53 % Running -m NewStrategy36822 for 0.0202889442444 seconds % 21.03/21.54 % Running -m NewStrategy61701 for 0.469702005386 seconds % 21.03/21.55 % Running -m NewStrategy29999 for 55.0910689831 seconds % 76.19/76.66 % Running -m NewStrategy31076 for 0.282725095749 seconds % 76.22/76.95 % Running -m NewStrategy34763 for 0.00944900512695 seconds % 76.22/76.97 % Running -m NewStrategy29644 for 0.0159990787506 seconds % 76.22/76.98 % Running -m mode252d for 0.117980957031 seconds % 76.54/77.10 % Running -m NewStrategy8000 for 35.2114069462 seconds % 76.66/77.11 % Running -m NewStrategy63501 for 0.242960929871 seconds % 76.67/77.36 % Running -m mode325 for 31.0973038673 seconds % 111.65/108.47 % Running -m NewStrategy18901 for 0.00690793991089 seconds % 111.65/108.48 % Running -m NewStrategy53030 for 93.1254749298 seconds % 204.87/201.63 % Running -m NewStrategy63339 for 0.102976083755 seconds % 204.99/201.74 % Running -m NewStrategy72417 for 12.2378571033 seconds % 204.99/201.75 % Running -m NewStrategy13727 for 0.056174993515 seconds % 204.99/201.76 % Running -m NewStrategy32467 for 0.0582859516144 seconds % 205.03/201.83 % Running -m NewStrategy59789 for 31.8605279922 seconds % 210.43/207.15 % % 210.43/207.15 % SZS status Theorem % 210.43/207.15 % NewStrategy59789 % 210.43/207.15 %------------------------------------------------------------------------------