#!/usr/bin/perl

my $hypfile = shift or die "Requires hypothesis output file name";

$hypfile =~ s!\\!\\\\!g;
$hypfile =~ s!\'!\\\'!g;

open (HYPFILE, ">$hypfile") or die "Cannot open hypothesis output file $hypfile";

while (<>) {
    if (m!^[[:space:]]*(fof|cnf)[[:space:]]*\([^,]*,[[:space:]]*hypothesis[[:space:]]*,!) {
        print HYPFILE;
    } else {
        if (m!^[[:space:]]*(fof|cnf)[[:space:]]*\(([^,]*),[[:space:]]*conjecture[[:space:]]*,!) {
            my $conjfile = $2;
            $conjfile =~ s![[:space:]]!!g;
            $conjfile .= ".tp";
            system ("cat $hypfile > $conjfile") && die "Cannot copy $hypfile to $conjfile : $?";
            open (CONJFILE, ">>$conjfile") or die "Cannot open conjecture output file $conjfile";
#            print CONJFILE "include('$hypfile').\n";
            s!&!&\n!g;
            print CONJFILE;
            close CONJFILE;
        } else {
            print STDERR "#Bad line.\n";
            print STDOUT;
        }
    }
}
close HYPFILE;