%------------------------------------------------------------------------------ % File : Satallax-MaLeS---1.3 % Problem : CSR150^3 : TPTP v6.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % Computer : n117.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 12:56:31 EDT 2015 % Result : Theorem 177.95s % 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 : CSR150^3 : TPTP v6.2.0. Released v5.3.0. % 0.00/0.02 % Command : src/helsing.py -t %d -c ../satallax.ini -p %s % 0.00/1.05 % Computer : n117.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 : Wed Oct 7 12:31:52 CDT 2015 % 0.00/1.05 % CPUTime : % 1.60/2.93 % Running -m NewStrategy70786 for 9.71954011917 seconds % 11.32/12.66 % Running -m mode390 for 0.0690660476685 seconds % 11.41/12.75 % Running -m NewStrategy21546 for 10.405479908 seconds % 11.41/12.76 % Running -m mode316 for 30.0226969719 seconds % 41.49/42.79 % Running -m NewStrategy32530 for 56.2154941559 seconds % 97.93/99.03 % Running -m NewStrategy10189 for 0.0147910118103 seconds % 97.93/99.04 % Running -m NewStrategy36822 for 0.0202889442444 seconds % 97.93/99.05 % Running -m mode165 for 0.0204191207886 seconds % 97.93/99.08 % Running -m NewStrategy56535 for 0.0329518318176 seconds % 97.93/99.09 % Running -m NewStrategy61701 for 0.0890719890594 seconds % 98.03/99.10 % Running -m NewStrategy63501 for 0.242960929871 seconds % 98.03/99.36 % Running -m mode245 for 0.0183751583099 seconds % 98.03/99.38 % Running -m NewStrategy62949 for 0.0302178859711 seconds % 98.32/99.42 % Running -m NewStrategy72394 for 20.4193341732 seconds % 98.32/99.44 % Running -m NewStrategy63579 for 16.0358059406 seconds % 114.35/115.49 % Running -m NewStrategy59789 for 19.7055459023 seconds % 133.45/135.20 % Running -m mode320 for 2.31782484055 seconds % 136.77/137.53 % Running -m mode397 for 0.0140738487244 seconds % 136.77/137.55 % Running -m NewStrategy18901 for 0.00690793991089 seconds % 136.77/137.56 % Running -m NewStrategy57901 for 0.0843760967255 seconds % 136.86/137.65 % Running -m NewStrategy30812 for 0.0114359855652 seconds % 136.86/137.66 % Running -m NewStrategy53030 for 0.194667100906 seconds % 136.96/137.87 % Running -m NewStrategy63339 for 0.102976083755 seconds % 137.16/137.98 % Running -m NewStrategy67852 for 0.181189060211 seconds % 137.27/138.17 % Running -m NewStrategy32550 for 0.332719087601 seconds % 137.79/138.51 % Running -m NewStrategy13531 for 0.794187068939 seconds % 137.81/139.34 % Running -m NewStrategy28542 for 0.0422439575195 seconds % 137.81/139.39 % Running -m NewStrategy72141 for 0.63912987709 seconds % 139.26/140.04 % Running -m NewStrategy57901 for 38.5259349346 seconds % 177.86/178.58 % Running -m NewStrategy68939 for 51.9914669991 seconds % 177.95/178.95 % % 177.95/178.95 % SZS status Theorem % 177.95/178.95 % NewStrategy68939 % 177.95/178.95 %------------------------------------------------------------------------------