%------------------------------------------------------------------------------ % File : Satallax-MaLeS---1.3 % Problem : PHI008^4 : 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 : n022.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:47 EDT 2016 % Result : Theorem 101.17s % 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 : PHI008^4 : TPTP v6.4.0. Released v6.4.0. % 0.00/0.04 % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % 0.02/0.23 % Computer : n022.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:00:38 CDT 2016 % 0.02/0.23 % CPUTime : % 1.55/3.04 % Running -m NewStrategy30350 for 0.0450479984283 seconds % 1.64/3.10 % Running -m NewStrategy67852 for 65.8015289307 seconds % 67.55/68.92 % Running -m NewStrategy33260 for 2.09500098228 seconds % 67.55/68.94 % Running -m NewStrategy35034 for 25.0609071255 seconds % 67.55/68.95 % Running -m NewStrategy36343 for 0.34478521347 seconds % 67.55/68.96 % Running -m NewStrategy26075 for 31.1500561237 seconds % 67.55/68.97 % Running -m NewStrategy13205 for 2.12560510635 seconds % 69.70/71.10 % Running -m NewStrategy35943 for 1.08488607407 seconds % 70.90/72.76 % Running -m NewStrategy32261 for 0.0434880256653 seconds % 70.90/72.77 % Running -m NewStrategy57901 for 0.15877199173 seconds % 70.91/72.94 % Running -m NewStrategy61701 for 0.469702005386 seconds % 70.91/72.95 % Running -m NewStrategy18901 for 0.00690793991089 seconds % 70.91/72.96 % Running -m mode165 for 0.0204191207886 seconds % 71.12/72.99 % Running -m NewStrategy20272 for 0.0263228416443 seconds % 71.12/73.02 % Running -m NewStrategy63579 for 15.8970880508 seconds % 87.05/88.93 % Running -m NewStrategy56535 for 0.0329518318176 seconds % 87.05/88.94 % Running -m mode187 for 6.44168305397 seconds % 93.56/95.39 % Running -m mode446 for 1.72408986092 seconds % 95.28/97.13 % Running -m NewStrategy32550 for 0.332719087601 seconds % 95.32/97.47 % Running -m mode369 for 0.0164971351624 seconds % 95.32/97.49 % Running -m NewStrategy68939 for 0.553977012634 seconds % 96.19/98.06 % Running -m NewStrategy72394 for 20.4193341732 seconds % 96.19/98.07 % Running -m NewStrategy29644 for 141.371892929 seconds % 96.19/98.08 % Running -m mode446 for 4.49235391617 seconds % 100.66/102.59 % Running -m NewStrategy34763 for 0.00944900512695 seconds % 100.78/102.60 % Running -m NewStrategy36822 for 0.0202889442444 seconds % 100.81/102.61 % Running -m NewStrategy63501 for 0.242960929871 seconds % 100.81/102.86 % Running -m NewStrategy63339 for 0.102976083755 seconds % 101.11/102.97 % Running -m NewStrategy53030 for 0.194667100906 seconds % 101.17/103.14 % % 101.17/103.14 % SZS status Theorem % 101.17/103.14 % NewStrategy53030 % 101.17/103.14 %------------------------------------------------------------------------------