385 "-t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) |
385 "-t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) |
386 ^ " -s " ^ the_system system_name system_versions, |
386 ^ " -s " ^ the_system system_name system_versions, |
387 proof_delims = union (op =) tstp_proof_delims proof_delims, |
387 proof_delims = union (op =) tstp_proof_delims proof_delims, |
388 known_failures = known_failures @ known_perl_failures @ |
388 known_failures = known_failures @ known_perl_failures @ |
389 [(Unprovable, "says Satisfiable"), |
389 [(Unprovable, "says Satisfiable"), |
|
390 (Unprovable, "says CounterSatisfiable"), |
390 (ProofMissing, "says Theorem"), |
391 (ProofMissing, "says Theorem"), |
|
392 (ProofMissing, "says Unsatisfiable"), |
391 (IncompleteUnprovable, "says Unknown"), |
393 (IncompleteUnprovable, "says Unknown"), |
392 (IncompleteUnprovable, "says GaveUp"), |
394 (IncompleteUnprovable, "says GaveUp"), |
393 (TimedOut, "says Timeout"), |
395 (TimedOut, "says Timeout"), |
394 (Inappropriate, "says Inappropriate")], |
396 (Inappropriate, "says Inappropriate")], |
395 conj_sym_kind = conj_sym_kind, |
397 conj_sym_kind = conj_sym_kind, |