%------------------------------------------------------------------------------ % File : Satallax-MaLeS---1.3 % Problem : NUN023^1 : TPTP v6.4.0. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % Computer : n015.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16091.75MB % OS : Linux 3.10.0-327.10.1.el7.x86_64 % CPULimit : 300s % DateTime : Mon Mar 28 10:08:24 EDT 2016 % Result : Theorem 72.99s % 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.01/0.03 % Problem : NUN023^1 : TPTP v6.4.0. Released v6.4.0. % 0.01/0.04 % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % 0.02/0.23 % Computer : n015.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 : 16091.75MB % 0.02/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.02/0.23 % CPULimit : 300 % 0.02/0.23 % DateTime : Fri Mar 25 14:05:53 CDT 2016 % 0.02/0.23 % CPUTime : % 1.53/1.76 % Running -m mode320 for 0.0559279918671 seconds % 1.58/1.83 % Running -m NewStrategy31362 for 0.0852649211884 seconds % 1.64/1.92 % Running -m mode454 for 15.8333239555 seconds % 17.50/17.77 % Running -m NewStrategy31551 for 0.173868894577 seconds % 17.63/17.95 % Running -m mode122b for 2.69752717018 seconds % 20.46/20.66 % Running -m mode187 for 7.1962890625 seconds % 27.66/27.87 % Running -m NewStrategy29644 for 0.0159990787506 seconds % 27.74/27.88 % Running -m NewStrategy61701 for 1.12459087372 seconds % 27.74/27.89 % Running -m NewStrategy36822 for 0.0202889442444 seconds % 27.74/27.90 % Running -m NewStrategy29644 for 141.371892929 seconds % 27.74/27.91 % Running -m mode446 for 18.9846539497 seconds % 46.79/46.91 % Running -m NewStrategy63501 for 0.242960929871 seconds % 46.82/47.16 % Running -m NewStrategy31076 for 0.237552881241 seconds % 47.31/51.66 % Running -m NewStrategy72394 for 20.4193341732 seconds % 47.31/51.67 % Running -m NewStrategy56614 for 0.0971121788025 seconds % 47.32/51.78 % Running -m NewStrategy56535 for 0.0329518318176 seconds % 47.32/51.79 % Running -m NewStrategy31076 for 0.282725095749 seconds % 47.44/52.08 % Running -m mode325 for 0.00964713096619 seconds % 47.72/52.09 % Running -m NewStrategy63339 for 0.102976083755 seconds % 47.74/52.20 % Running -m mode165 for 0.0204191207886 seconds % 47.86/52.23 % Running -m NewStrategy53030 for 0.194667100906 seconds % 48.04/52.43 % Running -m NewStrategy57901 for 0.0843760967255 seconds % 48.09/52.53 % Running -m NewStrategy13531 for 0.794187068939 seconds % 48.99/53.54 % Running -m NewStrategy70786 for 0.395126104355 seconds % 48.99/53.95 % Running -m NewStrategy32467 for 0.0582859516144 seconds % 48.99/54.01 % Running -m NewStrategy18901 for 0.00690793991089 seconds % 48.99/54.02 % Running -m NewStrategy20272 for 0.0263228416443 seconds % 49.47/54.05 % Running -m NewStrategy72141 for 12.0027141571 seconds % 61.48/66.07 % Running -m mode325 for 31.0973038673 seconds % 72.99/77.56 % % 72.99/77.56 % SZS status Theorem % 72.99/77.56 % mode325 % 72.99/77.56 %------------------------------------------------------------------------------