Given the defaults options in Defaults.hs.
A response gives something like:
"% SZS start RequiredInformation\n% Congratulations - you have become a registered power user
of SystemOnTPTP, at IP address 181.137.110.96.\n% Please consider donating to the TPTP project
- see www.tptp.org for details.\n% When you donate this message will disappear.\n% If you do not
donate a random delay might be added to your processing time.\n% SZS end
RequiredInformation\nE---2.0 system information being retrieved\nE---2.0's non-default
parameters being retrieved\n -t none\n -f tptp:raw\n -x eprover -s --cpu-limit=%d %s\nE--
-2.0's AGT001+1 does not need preparation\nE---2.0 being executed on AGT001+1 using
/home/tptp/Systems/E---2.0/eprover -s --cpu-limit=60 '/home/tptp/TPTP-
v6.4.0/Problems/AGT/AGT001+1.p'\nRESULT: AGT001+1 - E---2.0 says Theorem - CPU = 0.01 WC = 0.03 \nOUTPUT: AGT001+1 - E---2.0 says Assurance - CPU = 0.01 WC = 0.03 \n"
We need a method to check if the response above is Ok or the prover couldn't prove the conjecture. The output suggest check with isInfixOf "ATP says Theorem" in the same line after "RESULT:" . The name of this method should be the same as Apia use for local atps.
Given the defaults options in Defaults.hs. A response gives something like:
We need a method to check if the response above is Ok or the prover couldn't prove the conjecture. The output suggest check with
isInfixOf "ATP says Theorem"in the same line after "RESULT:" . The name of this method should be the same as Apia use for local atps.