:- assert(method(method('.', 'semantic methods'), category(rc, innermost), command('/home/georg/.tct/tct', '+RTS -N -RTS -a irc -s "semantics" -t 300 $problem'), 320)).
:- assert(method(method('.', 'decompose'), category(rc, innermost), command('/home/georg/.tct/tct', '+RTS -N -RTS -a irc -s "simple :dp Off" -t 300 $problem'), 320)).
:- assert(method(method('.', 'DP + decompose'), category(rc, innermost), command('/home/georg/.tct/tct', '+RTS -N -RTS -a irc -s "simple :dp On" -t 300 $problem'), 320)).
:- assert(method(method('.', 'DP + DG decompose'), category(rc, innermost), command('/home/georg/.tct/tct', '+RTS -N -RTS -a irc -s "raml :inner-timeout 20 :greedy Off :smallbits On :bigbits On :semdegree 2" -t 300 $problem'), 320)).
:- assert(method(method('.', 'DP + DG decompose (greedy)'), category(rc, innermost), command('/home/georg/.tct/tct', '+RTS -N -RTS -a irc -s "raml :inner-timeout 20 :greedy On :smallbits On :bigbits On :semdegree 2" -t 300 $problem'), 320)).
:- assert(trs('minsort.raml', './tpdb/minsort.raml.trs')).
:- assert(trs('bitonic.raml', './tpdb/bitonic.raml.trs')).
:- assert(trs('duplicates.raml', './tpdb/duplicates.raml.trs')).
:- assert(trs('longestCommonSubsequence.raml', './tpdb/longestCommonSubsequence.raml.trs')).
:- assert(trs('insertionsort.raml', './tpdb/insertionsort.raml.trs')).
:- assert(trs('rationalPotential.raml', './tpdb/rationalPotential.raml.trs')).
:- assert(trs('ticks.raml', './tpdb/ticks.raml.trs')).
:- assert(trs('bitvectors.raml', './tpdb/bitvectors.raml.trs')).
:- assert(trs('eratosthenes.raml', './tpdb/eratosthenes.raml.trs')).
:- assert(trs('dyade.raml', './tpdb/dyade.raml.trs')).
:- assert(trs('bfs.raml', './tpdb/bfs.raml.trs')).
:- assert(trs('flatten.raml', './tpdb/flatten.raml.trs')).
:- assert(trs('mergesort.raml', './tpdb/mergesort.raml.trs')).
:- assert(trs('appendAll.raml', './tpdb/appendAll.raml.trs')).
:- assert(trs('subtrees.raml', './tpdb/subtrees.raml.trs')).
:- assert(trs('quicksort.raml', './tpdb/quicksort.raml.trs')).
:- assert(trs('listsort.raml', './tpdb/listsort.raml.trs')).
:- assert(trs('matrix.raml', './tpdb/matrix.raml.trs')).
:- assert(trs('bft mmult.raml', './tpdb/bft_mmult.raml.trs')).
:- assert(trs('clevermmult.raml', './tpdb/clevermmult.raml.trs')).
:- assert(trs('tuples.raml', './tpdb/tuples.raml.trs')).
:- assert(trs('queue.raml', './tpdb/queue.raml.trs')).
:- assert(trs('splitandsort.raml', './tpdb/splitandsort.raml.trs')).
:- assert(result('tuples.raml', method('.', 'DP + DG decompose (greedy)'), timeout, './DP + DG decompose (greedy)/tuples.raml.proof', none)).
:- assert(result('ticks.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(0)), './DP + DG decompose (greedy)/ticks.raml.proof', none)).
:- assert(result('subtrees.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/subtrees.raml.proof', none)).
:- assert(result('splitandsort.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(3)), './DP + DG decompose (greedy)/splitandsort.raml.proof', none)).
:- assert(result('rationalPotential.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(1)), './DP + DG decompose (greedy)/rationalPotential.raml.proof', none)).
:- assert(result('quicksort.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/quicksort.raml.proof', none)).
:- assert(result('queue.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(5)), './DP + DG decompose (greedy)/queue.raml.proof', none)).
:- assert(result('minsort.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/minsort.raml.proof', none)).
:- assert(result('mergesort.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/mergesort.raml.proof', none)).
:- assert(result('matrix.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(4)), './DP + DG decompose (greedy)/matrix.raml.proof', none)).
:- assert(result('longestCommonSubsequence.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/longestCommonSubsequence.raml.proof', none)).
:- assert(result('listsort.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(3)), './DP + DG decompose (greedy)/listsort.raml.proof', none)).
:- assert(result('insertionsort.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/insertionsort.raml.proof', none)).
:- assert(result('flatten.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/flatten.raml.proof', none)).
:- assert(result('eratosthenes.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/eratosthenes.raml.proof', none)).
:- assert(result('dyade.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/dyade.raml.proof', none)).
:- assert(result('duplicates.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(3)), './DP + DG decompose (greedy)/duplicates.raml.proof', none)).
:- assert(result('clevermmult.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(3)), './DP + DG decompose (greedy)/clevermmult.raml.proof', none)).
:- assert(result('bitvectors.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/bitvectors.raml.proof', none)).
:- assert(result('bitonic.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(4)), './DP + DG decompose (greedy)/bitonic.raml.proof', none)).
:- assert(result('bft mmult.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(4)), './DP + DG decompose (greedy)/bft_mmult.raml.proof', none)).
:- assert(result('bfs.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(2)), './DP + DG decompose (greedy)/bfs.raml.proof', none)).
:- assert(result('appendAll.raml', method('.', 'DP + DG decompose (greedy)'), yes(poly(0), poly(1)), './DP + DG decompose (greedy)/appendAll.raml.proof', none)).
:- assert(result('tuples.raml', method('.', 'DP + DG decompose'), timeout, './DP + DG decompose/tuples.raml.proof', none)).
:- assert(result('ticks.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(0)), './DP + DG decompose/ticks.raml.proof', none)).
:- assert(result('subtrees.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/subtrees.raml.proof', none)).
:- assert(result('splitandsort.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(3)), './DP + DG decompose/splitandsort.raml.proof', none)).
:- assert(result('rationalPotential.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(1)), './DP + DG decompose/rationalPotential.raml.proof', none)).
:- assert(result('quicksort.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/quicksort.raml.proof', none)).
:- assert(result('queue.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(5)), './DP + DG decompose/queue.raml.proof', none)).
:- assert(result('minsort.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/minsort.raml.proof', none)).
:- assert(result('mergesort.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/mergesort.raml.proof', none)).
:- assert(result('matrix.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(3)), './DP + DG decompose/matrix.raml.proof', none)).
:- assert(result('longestCommonSubsequence.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/longestCommonSubsequence.raml.proof', none)).
:- assert(result('listsort.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/listsort.raml.proof', none)).
:- assert(result('insertionsort.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/insertionsort.raml.proof', none)).
:- assert(result('flatten.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/flatten.raml.proof', none)).
:- assert(result('eratosthenes.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/eratosthenes.raml.proof', none)).
:- assert(result('dyade.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/dyade.raml.proof', none)).
:- assert(result('duplicates.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/duplicates.raml.proof', none)).
:- assert(result('clevermmult.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/clevermmult.raml.proof', none)).
:- assert(result('bitvectors.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(2)), './DP + DG decompose/bitvectors.raml.proof', none)).
:- assert(result('bitonic.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(4)), './DP + DG decompose/bitonic.raml.proof', none)).
:- assert(result('bft mmult.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(3)), './DP + DG decompose/bft_mmult.raml.proof', none)).
:- assert(result('bfs.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(1)), './DP + DG decompose/bfs.raml.proof', none)).
:- assert(result('appendAll.raml', method('.', 'DP + DG decompose'), yes(poly(0), poly(1)), './DP + DG decompose/appendAll.raml.proof', none)).
:- assert(result('tuples.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/tuples.raml.proof', none)).
:- assert(result('ticks.raml', method('.', 'DP + decompose'), yes(poly(0), poly(0)), './DP + decompose/ticks.raml.proof', none)).
:- assert(result('subtrees.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/subtrees.raml.proof', none)).
:- assert(result('splitandsort.raml', method('.', 'DP + decompose'), maybe, './DP + decompose/splitandsort.raml.proof', none)).
:- assert(result('rationalPotential.raml', method('.', 'DP + decompose'), yes(poly(0), poly(1)), './DP + decompose/rationalPotential.raml.proof', none)).
:- assert(result('quicksort.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/quicksort.raml.proof', none)).
:- assert(result('queue.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/queue.raml.proof', none)).
:- assert(result('minsort.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/minsort.raml.proof', none)).
:- assert(result('mergesort.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/mergesort.raml.proof', none)).
:- assert(result('matrix.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/matrix.raml.proof', none)).
:- assert(result('longestCommonSubsequence.raml', method('.', 'DP + decompose'), maybe, './DP + decompose/longestCommonSubsequence.raml.proof', none)).
:- assert(result('listsort.raml', method('.', 'DP + decompose'), maybe, './DP + decompose/listsort.raml.proof', none)).
:- assert(result('insertionsort.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/insertionsort.raml.proof', none)).
:- assert(result('flatten.raml', method('.', 'DP + decompose'), maybe, './DP + decompose/flatten.raml.proof', none)).
:- assert(result('eratosthenes.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/eratosthenes.raml.proof', none)).
:- assert(result('dyade.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/dyade.raml.proof', none)).
:- assert(result('duplicates.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/duplicates.raml.proof', none)).
:- assert(result('clevermmult.raml', method('.', 'DP + decompose'), maybe, './DP + decompose/clevermmult.raml.proof', none)).
:- assert(result('bitvectors.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/bitvectors.raml.proof', none)).
:- assert(result('bitonic.raml', method('.', 'DP + decompose'), none, none, none)).
:- assert(result('bft mmult.raml', method('.', 'DP + decompose'), timeout, './DP + decompose/bft_mmult.raml.proof', none)).
:- assert(result('bfs.raml', method('.', 'DP + decompose'), yes(poly(0), poly(1)), './DP + decompose/bfs.raml.proof', none)).
:- assert(result('appendAll.raml', method('.', 'DP + decompose'), yes(poly(0), poly(2)), './DP + decompose/appendAll.raml.proof', none)).
:- assert(result('tuples.raml', method('.', 'decompose'), maybe, './decompose/tuples.raml.proof', none)).
:- assert(result('ticks.raml', method('.', 'decompose'), yes(poly(0), poly(0)), './decompose/ticks.raml.proof', none)).
:- assert(result('subtrees.raml', method('.', 'decompose'), yes(poly(0), poly(2)), './decompose/subtrees.raml.proof', none)).
:- assert(result('splitandsort.raml', method('.', 'decompose'), maybe, './decompose/splitandsort.raml.proof', none)).
:- assert(result('rationalPotential.raml', method('.', 'decompose'), yes(poly(0), poly(1)), './decompose/rationalPotential.raml.proof', none)).
:- assert(result('quicksort.raml', method('.', 'decompose'), timeout, './decompose/quicksort.raml.proof', none)).
:- assert(result('queue.raml', method('.', 'decompose'), maybe, './decompose/queue.raml.proof', none)).
:- assert(result('minsort.raml', method('.', 'decompose'), yes(poly(0), poly(3)), './decompose/minsort.raml.proof', none)).
:- assert(result('mergesort.raml', method('.', 'decompose'), timeout, './decompose/mergesort.raml.proof', none)).
:- assert(result('matrix.raml', method('.', 'decompose'), maybe, './decompose/matrix.raml.proof', none)).
:- assert(result('longestCommonSubsequence.raml', method('.', 'decompose'), maybe, './decompose/longestCommonSubsequence.raml.proof', none)).
:- assert(result('listsort.raml', method('.', 'decompose'), maybe, './decompose/listsort.raml.proof', none)).
:- assert(result('insertionsort.raml', method('.', 'decompose'), yes(poly(0), poly(3)), './decompose/insertionsort.raml.proof', none)).
:- assert(result('flatten.raml', method('.', 'decompose'), maybe, './decompose/flatten.raml.proof', none)).
:- assert(result('eratosthenes.raml', method('.', 'decompose'), yes(poly(0), poly(3)), './decompose/eratosthenes.raml.proof', none)).
:- assert(result('dyade.raml', method('.', 'decompose'), maybe, './decompose/dyade.raml.proof', none)).
:- assert(result('duplicates.raml', method('.', 'decompose'), yes(poly(0), poly(2)), './decompose/duplicates.raml.proof', none)).
:- assert(result('clevermmult.raml', method('.', 'decompose'), maybe, './decompose/clevermmult.raml.proof', none)).
:- assert(result('bitvectors.raml', method('.', 'decompose'), timeout, './decompose/bitvectors.raml.proof', none)).
:- assert(result('bitonic.raml', method('.', 'decompose'), maybe, './decompose/bitonic.raml.proof', none)).
:- assert(result('bft mmult.raml', method('.', 'decompose'), maybe, './decompose/bft_mmult.raml.proof', none)).
:- assert(result('bfs.raml', method('.', 'decompose'), maybe, './decompose/bfs.raml.proof', none)).
:- assert(result('appendAll.raml', method('.', 'decompose'), yes(poly(0), poly(2)), './decompose/appendAll.raml.proof', none)).
:- assert(result('tuples.raml', method('.', 'semantic methods'), maybe, './semantic methods/tuples.raml.proof', none)).
:- assert(result('ticks.raml', method('.', 'semantic methods'), yes(unknown, poly(0)), './semantic methods/ticks.raml.proof', none)).
:- assert(result('subtrees.raml', method('.', 'semantic methods'), maybe, './semantic methods/subtrees.raml.proof', none)).
:- assert(result('splitandsort.raml', method('.', 'semantic methods'), maybe, './semantic methods/splitandsort.raml.proof', none)).
:- assert(result('rationalPotential.raml', method('.', 'semantic methods'), yes(unknown, poly(1)), './semantic methods/rationalPotential.raml.proof', none)).
:- assert(result('quicksort.raml', method('.', 'semantic methods'), maybe, './semantic methods/quicksort.raml.proof', none)).
:- assert(result('queue.raml', method('.', 'semantic methods'), maybe, './semantic methods/queue.raml.proof', none)).
:- assert(result('minsort.raml', method('.', 'semantic methods'), maybe, './semantic methods/minsort.raml.proof', none)).
:- assert(result('mergesort.raml', method('.', 'semantic methods'), maybe, './semantic methods/mergesort.raml.proof', none)).
:- assert(result('matrix.raml', method('.', 'semantic methods'), maybe, './semantic methods/matrix.raml.proof', none)).
:- assert(result('longestCommonSubsequence.raml', method('.', 'semantic methods'), maybe, './semantic methods/longestCommonSubsequence.raml.proof', none)).
:- assert(result('listsort.raml', method('.', 'semantic methods'), maybe, './semantic methods/listsort.raml.proof', none)).
:- assert(result('insertionsort.raml', method('.', 'semantic methods'), maybe, './semantic methods/insertionsort.raml.proof', none)).
:- assert(result('flatten.raml', method('.', 'semantic methods'), maybe, './semantic methods/flatten.raml.proof', none)).
:- assert(result('eratosthenes.raml', method('.', 'semantic methods'), maybe, './semantic methods/eratosthenes.raml.proof', none)).
:- assert(result('dyade.raml', method('.', 'semantic methods'), maybe, './semantic methods/dyade.raml.proof', none)).
:- assert(result('duplicates.raml', method('.', 'semantic methods'), maybe, './semantic methods/duplicates.raml.proof', none)).
:- assert(result('clevermmult.raml', method('.', 'semantic methods'), maybe, './semantic methods/clevermmult.raml.proof', none)).
:- assert(result('bitvectors.raml', method('.', 'semantic methods'), timeout, './semantic methods/bitvectors.raml.proof', none)).
:- assert(result('bitonic.raml', method('.', 'semantic methods'), maybe, './semantic methods/bitonic.raml.proof', none)).
:- assert(result('bft mmult.raml', method('.', 'semantic methods'), maybe, './semantic methods/bft_mmult.raml.proof', none)).
:- assert(result('bfs.raml', method('.', 'semantic methods'), maybe, './semantic methods/bfs.raml.proof', none)).
:- assert(result('appendAll.raml', method('.', 'semantic methods'), yes(unknown, poly(2)), './semantic methods/appendAll.raml.proof', none)).