DFG2TPTP(1) SPASS DFG2TPTP(1)NAME
dfg2tptp - transforms DFG files into TPTP files
SYNOPSIS
dfg2tptp <input-file> <output-file>
DESCRIPTION
dfg2tptp is a program which converts a problem input file in DFG format into a problem input file in TPTP format. The TPTP problem format
is used by the TPTP library of test problems for automated theorem proving, available at http://www.math.miami.edu/~tptp/. Various tools
exist to convert problems in TPTP format into input files for other theorem provers.
SEE ALSO checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), SPASS(1)AUTHORS
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
Contact : spass@mpi-inf.mpg.de
perl v5.10.0 2010-02-23 DFG2TPTP(1)
Check Out this Related Man Page
DFG2OTTER(1) SPASS DFG2OTTER(1)NAME
dfg2otter - transforms DFG clause files into Otter format
SYNOPSIS
dfg2otter [options] <infile> <outfile>
DESCRIPTION
dfg2otter is a C-program to transform problem input files in DFG syntax into Otter syntax. It accepts all options from SPASS, although only
a subset has an effect on translation.
dfg2otter negates conjecture formulae of the SPASS input file before printing the Otter usable list. The SPASS conjecture formula list is
translated into a disjunction of the negated single conjectures. If the SPASS input file consits of clauses, these are not modified.
SEE ALSO checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter.pl(1), SPASS(1)AUTHORS
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
Contact : spass@mpi-inf.mpg.de
perl v5.10.0 2010-02-23 DFG2OTTER(1)
HI there,
I need to backup some files from other pcs.
I want to do it from my backupserver.
I am using Unicon (developed from icon) for programming a backupscript, my BS is Mandrake Linux.
The problem I have is:
I cannot use tar multivolume with dd
the command looks something like... (6 Replies)
Could one of you, please, provide some input regarding my problem below and it is as follows:
I have 2 files that I need to make sure are identical before processing:
First, I sort both files
Second, I do a diff file1 file2 > File 3
This provides me with the difference.
Now, I need to... (6 Replies)
I install a software xchm for opening chm files.
I install software and also its required libraries. But when i start it; no GUI appears. Application got halt. Process name also appears in process list when i run top command. Appliation continously using cpu but no GUI appears. Please tell me... (7 Replies)
I'm having a problem getting my variables to work in dishing out an RMC script.
The $1 works fine. $2 does not
Here's a portion of the script:
server=$1
filesystem1=$2
#
dsh -w $1 'mkcondition -c "/var space used" -s "Name == \"$2\"" -e "PercentTotUsed > 90" -d "An event will be generated... (7 Replies)
Hi,
I'd like to share this...
I see all the luns on my aix when I do lspv, 10 of them, configured by the san contractor. I defined the first sanvg no problem, the second one no problem, but the third got problem and so on. It's random after the second, I think. The error is 0516-024 mkvg:... (5 Replies)
Hi everyone!
Can you please help me with some shell scripting?
I have an input file input.txt
It has 3 columns (Time, Event, Value)
Time event Value
03:38:22 A 57
03:38:23 A 56
03:38:24 B 24
03:38:25 C 51
03:38:26 B 7
03:38:26 ... (7 Replies)
Hi guys, i am putting this problem again please help me out..
The RPC problem is appearing on the screen while starting the portmap service,take a look of the real..
#/etc/init.d/portmap restart
Stopping portmap:
Starting portmap:
Cannot register service: RPC: Timed out
not registered:... (15 Replies)
Hi guys,
I am new to AWK and unix scripting. Please see below my problem and let me know if anyone you can help.
I have 2 input files (example given below)
Input file 2 is a standard file (it will not change) and we have to get the name (second column after comma) from it and append it... (5 Replies)
First of all thanks to all for the good post, and the great site. I'm a noob, but I've been able to learna a lot by checking past posts.
I haven't been able to make sense of a problem that I've been working on for a while, hopefully someone can help me out. The script I wrote telnets into... (7 Replies)
Hello all
I am having problems using a bash script to read the input from the user and checking that its a valid number. I only want the user to input a maximum of a 3 number string (321 , 521 , 871 etc.). Anything longer or that includes a chararcter or symbol will display an error message.
... (8 Replies)
I've gone through bunch of threads on time calculations but none of them helps on my problem
I've to get the time difference in HHMM format from following inputs
Input 1 :
01/08/2010 01:30
01/08/2010 03:20
Input 2 :
01/06/2010 22:00
01/07/2010 16:00
First input is easy but... (8 Replies)
Wonderful evening to all of you!
My problem has to possible starting points.
Well, not really, but getting to either one is no problem at all.
So i got either a string in the format of "1920x1080" or simply the integers X = 1920 and Y = 1080.
When I am done, I would like to have an output... (5 Replies)
Hello guys,
I have a problem. I'm trying to use SDiff with two files which are containing spaces.
My problem is that I want to save the output with > in an extra file.
If I try to use it like this.
sdiff "test file1" "test file2" > OutputfileI get this message:
usage: diff ... (11 Replies)
Hello, I am trying to find a solution to problem that's proving to be beyond my newbie skills. The below files comes from a genetics study. File 1 describes a position on the genome and file 2 does the same but is formatted differently and has more information. I am trying to match all lines in... (5 Replies)