%------------------------------------------------------------------------------ % File : Satallax-MaLeS---1.3 % Problem : SEU948^5 : TPTP v6.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % Computer : n062.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-573.1.1.el6.x86_64 % CPULimit : 300s % DateTime : Thu Oct 8 17:02:17 EDT 2015 % Result : Theorem 259.87s % 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.02 % Problem : SEU948^5 : TPTP v6.2.0. Released v4.0.0. % 0.00/0.02 % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % 0.00/1.05 % Computer : n062.star.cs.uiowa.edu % 0.00/1.05 % Model : x86_64 x86_64 % 0.00/1.05 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.00/1.05 % Memory : 32286.75MB % 0.00/1.05 % OS : Linux 2.6.32-573.1.1.el6.x86_64 % 0.00/1.05 % CPULimit : 300 % 0.00/1.05 % DateTime : Mon Oct 5 19:41:45 CDT 2015 % 0.00/1.06 % CPUTime : % 1.54/2.65 % Running -m NewStrategy32261 for 0.0434880256653 seconds % 1.60/2.79 % Running -m NewStrategy20272 for 0.0263228416443 seconds % 1.61/2.83 % Running -m NewStrategy26866 for 0.020427942276 seconds % 1.61/2.86 % Running -m NewStrategy25012 for 121.280528069 seconds % 123.14/124.15 % Running -m mode325 for 0.00964713096619 seconds % 123.14/124.17 % Running -m NewStrategy28259 for 1.72401595116 seconds % 124.95/125.91 % Running -m NewStrategy18901 for 0.0142230987549 seconds % 124.95/125.92 % Running -m NewStrategy31551 for 7.74439811707 seconds % 132.64/133.68 % Running -m mode369 for 0.0164971351624 seconds % 132.77/133.71 % Running -m NewStrategy35034 for 0.0290069580078 seconds % 132.77/133.72 % Running -m NewStrategy13727 for 0.0965240001678 seconds % 132.77/133.73 % Running -m NewStrategy72394 for 20.4193341732 seconds % 132.77/133.73 % Running -m NewStrategy68939 for 0.553977012634 seconds % 133.37/134.30 % Running -m NewStrategy35504 for 101.351564884 seconds % 235.82/235.66 % Running -m NewStrategy29644 for 0.0159990787506 seconds % 235.82/235.67 % Running -m NewStrategy36822 for 0.0202889442444 seconds % 235.82/235.68 % Running -m NewStrategy22562 for 23.6540961266 seconds % 259.47/259.34 % Running -m mode165 for 0.115596055984 seconds % 259.55/259.47 % Running -m NewStrategy31076 for 0.237552881241 seconds % 259.87/259.71 % Running -m NewStrategy31440 for 41.6892168522 seconds % 259.87/259.72 % % 259.87/259.72 % SZS status Theorem % 259.87/259.72 % NewStrategy31440 % 259.87/259.72 %------------------------------------------------------------------------------