#!/usr/bin/perl # This is E.T 0.1, phoning home. Apart from that, he occasionally # proves theorems. He is fond of galaxy-sized problems and calls Eeeee # all the time. # SYNOPSIS: # cd E.T.0.1distro # export MLAR_ROOT=`pwd` # bin/et1.pl 60 very_large_problem.p # NOTES: # - The timelimit is mostly used as CPU time, but not perfectly. Kill # him yourself with your resource limits if this is important. # - By default a lot of junk will be created $MROOT/tmp. E.T. could # delete it, but he is used to galaxy-sized hard drives, so he does # not bother. # - Making a parallel version is easy, but it was not needed so far. use strict; # this needs to be set properly, unless the environment var MLAR_ROOT is set my $MROOT = "/home/mptp/gr/E.T.0.1distro"; $MROOT = $ENV{"MLAR_ROOT"} if(exists($ENV{"MLAR_ROOT"})); my $MBIN = "$MROOT/bin"; # my $MSCRIPT = "$MROOT/script"; my $MTMP0 = "$MROOT/tmp"; sub mywarn { print @_; } sub min { my ($x,$y) = @_; ($x <= $y)? $x : $y } sub max { my ($x,$y) = @_; ($x <= $y)? $y : $x } sub dprint { print @_; } # possible SZS statuses sub szs_INIT () { 'Initial' } # system was not run on the problem yet sub szs_UNKNOWN () { 'Unknown' } # used when system dies sub szs_THEOREM () { 'Theorem' } sub szs_COUNTERSAT () { 'CounterSatisfiable' } sub szs_RESOUT () { 'ResourceOut' } sub szs_GAVEUP () { 'GaveUp' } # system exited before the time limit for unknown reason my $gtimelimit = $ARGV[0]; my $gfilestem0 = $ARGV[$#ARGV]; use File::Basename; my ($name,$path,$suffix) = fileparse($gfilestem0, qr/\.[^.]*/); # $gfilestem0 =~ m/^(.*)\.p$/ or die "bad filename $gfilestem0"; #my $gfilestem = $1; #$gfilestem =~ s/.*\///; my $gfilestem = $name; my $MTMP = "$MTMP0/$gfilestem"; `mkdir -p $MTMP`; use Cwd 'abs_path'; my $gabspath= abs_path($gfilestem0); `ln -s $gabspath $MTMP/$gfilestem.p`; # my $gshgenfeatureprg = "$MBIN/fofshared"; # my $gshgenfeatureprg = "$MBIN/fofdt"; my $gshgenfeatureprgnrm = "$MBIN/fofdt"; my $gshgenfeatureprgstd = "$MBIN/fofshared"; my @gMizGreedStrats0 = ( ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_88760aa43d575e84b7030b8a6188f74ba5f80dc7'], ['mepo3-64-nrm-min',400,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['knn1-8-nrm-min',8,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-std-min',64,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-std-min',512,'protokoll_my8simple_sine13'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-std-min',512,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['knn1-40-nrm-min',96,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['knn1-256-nrm-min',256,'protokoll_atpstr_my_37be21ea059a2fcb865621e373a97f33a9d07b12'], ['knn1-64-nrm-min',64,'protokoll_atpstr_my_c284f1f10aedfccc65cdb7d9b1210ef814cb8f1a'], ['knn1-8-nrm-min',8,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['knn1-48-nrm-min',20,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'] ); my @gMizGreedStrats0_tst = ( ['knn1-128-std-min',128,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['knn1-128-std-min',128,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['knn1-128-std-min',128,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['knn1-128-std-min',128,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['knn1-128-std-min',128,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['knn1-128-std-min',128,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['knn1-128-std-min',128,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['knn1-128-std-min',128,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['knn1-128-std-min',128,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['knn1-128-std-min',128,'protokoll_my8simple_sine13'], ['knn1-128-std-min',128,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['knn1-128-std-min',128,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['knn1-128-std-min',128,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['knn1-128-std-min',128,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['knn1-48-nrm-min',20,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['knn1-48-nrm-min',20,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['knn1-48-nrm-min',20,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['knn1-48-nrm-min',20,'protokoll_my8simple_sine13'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['knn1-8-nrm-min',8,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['knn1-8-nrm-min',8,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['knn1-8-nrm-min',8,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['knn1-8-nrm-min',8,'protokoll_my8simple_sine13'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-nrm-min',128,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-nrm-min',128,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['mepo3-64-nrm-min',128,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['mepo3-64-nrm-min',128,'protokoll_my8simple_sine13'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['mepo3-64-nrm-min',128,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-nrm-min',16,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-nrm-min',16,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['mepo3-64-nrm-min',16,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['mepo3-64-nrm-min',16,'protokoll_my8simple_sine13'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['mepo3-64-nrm-min',16,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-nrm-min',32,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-nrm-min',32,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['mepo3-64-nrm-min',32,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['mepo3-64-nrm-min',32,'protokoll_my8simple_sine13'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['mepo3-64-nrm-min',32,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-nrm-min',400,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-nrm-min',400,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['mepo3-64-nrm-min',400,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['mepo3-64-nrm-min',400,'protokoll_my8simple_sine13'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['mepo3-64-nrm-min',400,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-std-min',512,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-std-min',512,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['mepo3-64-std-min',512,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['mepo3-64-std-min',512,'protokoll_my8simple_sine13'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['mepo3-64-std-min',512,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['mepo3-64-std-min',64,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['mepo3-64-std-min',64,'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['mepo3-64-std-min',64,'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['mepo3-64-std-min',64,'protokoll_my8simple_sine13'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3'], ['mepo3-64-std-min',64,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'] ); my @gMizGreedStrats0_std = ( ['knn-48-nrm-min',160,'protokoll_atpstr_my_a175515211bb22b22434eae9bbbfab623676a2ba'], ['mepo3-32-nrm-min',128,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], # ['lsi-400:16-nrm-min',64,'protokoll_my11simple_sine13'], ['knn-256-nrm-min',256,'protokoll_atpstr_my_37be21ea059a2fcb865621e373a97f33a9d07b12'], # ['lsi-400:48-nrm-min',160,'protokoll_atpstr_my_37be21ea059a2fcb865621e373a97f33a9d07b12'], ['geo-1:0.9999-nrm-min',64,'protokoll_atpstr_my_edc94794a7d25c504761344c2a8b4afaac43a2d0'], ['knn-80-nrm-min',1024,'protokoll_atpstr_my_9cb7c8ca63fd56afb053ade56353a3b00eee7e6a'], ['knn-48-nrm-min',160,'protokoll_my8simple_sine13'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_f9ecf400d7420b0148b2ef7cf4b1498512cf83fd'], ['knn-128-nrm-min',72,'protokoll_X----_auto_sine13'], ['geo-1:0.9-nrm-min',256,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['knn1-128-std-min',128,'protokoll_atpstr_my_c0d9db6a7b7a90437bd07739f25aa91c0ffc1607'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], ['knn1-32-std-min',32,'protokoll_atpstr_my_88760aa43d575e84b7030b8a6188f74ba5f80dc7'], ['knn-64-nrm-min',90,'protokoll_atpstr_my_37be21ea059a2fcb865621e373a97f33a9d07b12'], ['knn1-64-nrm-min',64,'protokoll_my17simple_sine13'], ['knn-200-nrm-min',64,'protokoll_atpstr_my_88760aa43d575e84b7030b8a6188f74ba5f80dc7'], ['knn-80-nrm-min',1024,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], # ['lsi-400:48-nrm-min',160,'protokoll_atpstr_my_c284f1f10aedfccc65cdb7d9b1210ef814cb8f1a'], ['knn-40-nrm-min',96,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['knn-48-std-min',48,'protokoll_my17simple_sine13'], # ['lsi-400:64-nrm-min',64,'protokoll_atpstr_my_a3154f3180cc47331f1b05c36960c32e4805a7c5'], ['knn-48-nrm-min',20,'protokoll_atpstr_my_c13d4886baa4fa2cef7b4f50892895255b04b078'], ['knn1-64-nrm-min',64,'protokoll_atpstr_my_c284f1f10aedfccc65cdb7d9b1210ef814cb8f1a'], ['knn1-64-std-min',64,'protokoll_atpstr_my_edc94794a7d25c504761344c2a8b4afaac43a2d0'], ['knn-128-std-min',128,'protokoll_atpstr_my_2eeaa79326ed674ea9ebfc3531c32ba1feec013b'], ['geo-1:0.9-nrm-min',256,'protokoll_atpstr_my_8fb389ef013a89e03c1aa87be52b2f151b1819cc'], ['knn1-128-std-min',128,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['knn1-8-nrm-min',8,'protokoll_atpstr_my_7b674c1081cd73ca6ce34d02596e6f6fd903ac6c'], ['knn1-48-nrm-min',20,'protokoll_atpstr_my_f67d73f57ffeda22ddd93400237cd848911520e5'], ['comb-geo:0.5-nbayes,0.00001:0.001,nrm,atp-knn,40,nrm,min',96,'protokoll_my8simple_sine13'], ['mepo3-64-nrm-min',256,'protokoll_atpstr_my_88760aa43d575e84b7030b8a6188f74ba5f80dc7'], ['knn-10-nrm-min',48,'protokoll_my23simple'], ['knn-32-nrm-min',32,'protokoll_my21simple'], ['lrnei-3072-sym-min',192,'protokoll_atpstr_my_7b674c1081cd73ca6ce34d02596e6f6fd903ac6c'], # ['lsi-400:32-nrm-min',12,'protokoll_my11simple_sine13'], ['knn-32-std-min',32,'protokoll_atpstr_my_1518b94b1627f7a5f7ce55e37817c09306fe714c'], ['knn-48-std-min',48,'protokoll_atpstr_my_a473e2c35f909af4ba00d9f1a7a8a454a851ed9c'] ); # TODO: put this in a separate file # strategy defs my %sdef = ( 'protokoll_G-E--_008_K18_F1_PI_AE_CS_SP_S0Y' => ' --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', 'protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S0S_sine05' => ' --sine=gf120_gu_RUU_F100_L00100 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_107_C37_F1_PI_AE_Q4_CS_SP_PS_S0Y' => ' --definitional-cnf=24 --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --presat-simplify --prefer-initial-clauses -tKBO6 -warity -c1 -Ginvconjfreq -F1 --delete-bad-limit=1024000000 -WSelectMaxLComplexAvoidPosPred -H\'(4*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_X----_auto_sine03' => ' --delete-bad-limit=1024000000 -xAuto -tAuto --sine=gf120_gu_R02_F100_L20000 ', 'protokoll_X----_auto_sine05' => ' --delete-bad-limit=1024000000 -xAuto -tAuto --sine=gf120_gu_RUU_F100_L00100 ', 'protokoll_X----_auto_sine13' => ' --delete-bad-limit=1024000000 -xAuto -tAuto --sine=gf120_h_gu_R02_F100_L20000 ', 'protokoll_X----_sauto_300' => ' --delete-bad-limit=1024000000 --auto ', 'protokoll_my10simple' => ' --definitional-cnf=24 --split-clauses=7 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(PreferProcessed),1*FIFOWeight(ConstPrio))\' ', 'protokoll_my11simple' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(PreferProcessed),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_my11simple_sine13' => ' --sine=gf120_h_gu_R02_F100_L20000 --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(PreferProcessed),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_my12simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_my13simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),8*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_my14simple' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))\' ', 'protokoll_my15simple' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H\'(1*Refinedweight(SimulateSOS,1,1,2,1.5,2),6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5))\' ', 'protokoll_my16simple' => ' --definitional-cnf=24 --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_my17simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100,1.5, 1.5, 1),10*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_my17simple_sine13' => ' --sine=gf120_h_gu_R02_F100_L20000 --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100,1.5, 1.5, 1),10*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_my18simple' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H\'(1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5))\' ', 'protokoll_my19simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),10*Refinedweight(SimulateSOS,1,1,2,1.5,2),2*FIFOWeight(PreferProcessed),8*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', 'protokoll_my1KBO_SOS' => ' --definitional-cnf=24 --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),10*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my1_SOS' => ' --definitional-cnf=24 --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),10*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my20simple' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*FIFOWeight(ConstPrio),10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5))\' ', 'protokoll_my21simple' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(ConstPrio),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my22simple' => ' --definitional-cnf=24 --split-clauses=7 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*FIFOWeight(ConstPrio),6*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_my23simple' => ' --definitional-cnf=24 --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*FIFOWeight(PreferProcessed),10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_my24simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),8*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_my25simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(2*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed),1*FIFOWeight(ConstPrio))\' ', 'protokoll_my2simple' => ' --definitional-cnf=24 --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*Clauseweight(PreferProcessed,1,1,1),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my3simple' => ' --definitional-cnf=24 --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my4simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1))\' ', 'protokoll_my5simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(ConstPrio),8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my6simple' => ' --definitional-cnf=24 --split-clauses=7 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5))\' ', 'protokoll_my7simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(PreferProcessed),1*FIFOWeight(ConstPrio),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5))\' ', 'protokoll_my8simple' => ' --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(ConstPrio),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my8simple_sine13' => ' --sine=gf120_h_gu_R02_F100_L20000 --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*FIFOWeight(ConstPrio),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_my9simple' => ' --definitional-cnf=24 --split-aggressive --split-clauses=7 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tAuto -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio),2*Refinedweight(SimulateSOS,1,1,2,1.5,2),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*FIFOWeight(PreferProcessed),10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1))\' ', 'protokoll_G-E--_008_B31_F1_PI_AE_S4_CS_SP_S2S' => ' --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', 'protokoll_G-E--_010_B02_F1_PI_AE_S4_CS_SP_S0Y' => ' --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_045_B31_F1_PI_AE_S4_CS_SP_S0Y' => ' --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_024_B07_F1_PI_AE_Q4_CS_SP_S0Y' => ' --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S0S' => ' --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H\'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_107_C37_F1_PI_AE_Q4_CS_SP_PS_S0Y_sine13' => ' --sine=gf120_h_gu_R02_F100_L20000 --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --presat-simplify --prefer-initial-clauses -tKBO6 -warity -c1 -Ginvconjfreq -F1 -s --delete-bad-limit=1024000000 -WSelectMaxLComplexAvoidPosPred -H\'(4*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_052_K18_F1_PI_AE_Q4_CS_SP_S0Y' => ' --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.05, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(SimulateSOS))\' ', 'protokoll_G-E--_092_C01_F1_PI_AE_Q4_CS_SP_PS_S0Y' => ' --definitional-cnf=24 --tstp-in --presat-simplify --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 -s --delete-bad-limit=1024000000 -WSelectMaxLComplexAvoidPosPred -tKBO6 -H\'(4*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_G-E--_008_C18_F1_PI_AE_Q4_CS_SP_PS_S0Y' => ' --definitional-cnf=24 --split-reuse-defs --split-clauses=4 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --presat-simplify --prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreq -F1 -s --delete-bad-limit=1024000000 -WSelectMaxLComplexAvoidPosPred -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', 'protokoll_G-E--_008_B07_F1_PI_AE_Q4_CS_SP_S2S' => ' --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', # the tstf6_40_128 prots 'protokoll_atpstr_my_05c900b7acd7e0314c15fce53bb9e79cf904cd89' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.5,, 03, 40,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectNewComplexAHP --simul-paramod --split-aggressive --split-clauses=4 -tLPO4 -H\'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),4*Clauseweight(ConstPrio,3,1,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ' , 'protokoll_atpstr_my_0b08a1d1a32ffc279e90769114bdfda18e672e1c' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.1,, 03, 40,1.0)\' -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-aggressive --split-reuse-defs -tAuto -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),4*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),12*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed))\' ' , 'protokoll_atpstr_my_37be21ea059a2fcb865621e373a97f33a9d07b12' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 2.0,, 02, 100,1.0)\' --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-clauses=7 --split-reuse-defs -tKBO -H\'(4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed))\' ' , 'protokoll_atpstr_my_3e6c84c618b85cc326775b240e7b2b07e3a2dde9' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Ginvfreqconstmin -WSelectNewComplexAHP --simul-paramod --split-aggressive --split-clauses=4 -tAuto -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))\' ' , 'protokoll_atpstr_my_4e6e6157a8ac18b9bae11142d40377c9660db06b' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 6.0,, 02, 100,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),2*Clauseweight(ConstPrio,3,1,1),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),2*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ' , 'protokoll_atpstr_my_5fce846ef89413a220d0951fb615d42ded72b119' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(PreferProcessed),8*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ' , 'protokoll_atpstr_my_7b674c1081cd73ca6ce34d02596e6f6fd903ac6c' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 5.0,, 02, 80,1.0)\' -Garity -WSelectNewComplexAHP --simul-paramod -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ConstPrio,3,1,1),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ' , 'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 6.0,, 02, 20000,1.0)\' --forward-context-sr -Garity -WSelectNewComplexAHP --simul-paramod --split-aggressive --split-reuse-defs -tAuto -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),12*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),8*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ' , 'protokoll_atpstr_my_a175515211bb22b22434eae9bbbfab623676a2ba' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectComplexG --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ' , 'protokoll_atpstr_my_a473e2c35f909af4ba00d9f1a7a8a454a851ed9c' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.4,, , 20,1.0)\' -Ginvfreqconstmin -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-aggressive --split-clauses=4 -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(PreferProcessed))\' ' , 'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 6.0,, 01, 80,1.0)\' -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ' , 'protokoll_atpstr_my_c284f1f10aedfccc65cdb7d9b1210ef814cb8f1a' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 5.0,, 02, 60,1.0)\' --forward-context-sr -Garity -WSelectComplexG --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ' , 'protokoll_atpstr_my_e4d2b8713a71da3a6bc64790217310975ccdde24' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.1,, 01, 20000,1.0)\' -winvfreqrank -c1 -Ginvfreq -WSelectComplexG --simul-paramod --split-clauses=7 --split-reuse-defs -tLPO4 -H\'(1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(PreferProcessed),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ' , 'protokoll_atpstr_my_e8ac4ce30401bd9e99200725cfa03816a32e3aa4' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 5.0,, 01, 20000,1.0)\' --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-aggressive -tLPO4 -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),12*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', # m10u2_184 'protokoll_atpstr_my_1518b94b1627f7a5f7ce55e37817c09306fe714c' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.2,, 02, 40,1.0)\' -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod -tAuto -H\'(1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),8*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(ByCreationDate,2,1,0.8),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_atpstr_my_2eeaa79326ed674ea9ebfc3531c32ba1feec013b' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Garity -WSelectComplexG --simul-paramod -tAuto -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.1,, 02, 60,1.0)\' --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 -tLPO4 -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),4*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_atpstr_my_69856783cec8fab1acccfe08bb382ad42c8475df' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 6.0,, , 100,1.0)\' -Garity -WSelectComplexG --simul-paramod --split-clauses=7 -tKBO -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_88760aa43d575e84b7030b8a6188f74ba5f80dc7' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 2.0,, 02, 100,1.0)\' --forward-context-sr -Garity -WSelectComplexG --simul-paramod --split-clauses=7 -tKBO -H\'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_atpstr_my_8fb389ef013a89e03c1aa87be52b2f151b1819cc' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.1,, 04, 80,1.0)\' -Garity -WSelectNewComplexAHP --simul-paramod --split-aggressive --split-clauses=4 --split-reuse-defs -tAuto -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),2*FIFOWeight(PreferProcessed),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_a3154f3180cc47331f1b05c36960c32e4805a7c5' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 6.0,, 01, 20000,1.0)\' --forward-context-sr -Garity -WSelectComplexG --simul-paramod --split-clauses=4 -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_a4a4da5778ba9bebf9bc5e616786c7ad501b1af5' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.1,, 03, 20,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-aggressive --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', 'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.5,, 04, 100,1.0)\' --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 -tLPO4 -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),6*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),4*Clauseweight(ConstPrio,3,1,1),1*Clauseweight(PreferProcessed,1,1,1),2*FIFOWeight(PreferProcessed),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),2*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_e3b5200232138aedc93b8882335da60ccd317d87' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.2,, 01, 80,1.0)\' --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-clauses=7 --split-reuse-defs -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1))\' ', 'protokoll_atpstr_my_e6869afe09f22abfbe1163ee95524cfdbfe77603' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 2.0,, 04, 40,1.0)\' --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 -tLPO4 -H\'(2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,3,1,1),2*FIFOWeight(PreferProcessed),10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_e6ff24ca1a5013a612ccffc94da0b282477718de' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.5,, 02, 100,1.0)\' --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --simul-paramod -tKBO -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', 'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.1,, 02, 60,1.0)\' --forward-context-sr -Garity -WSelectNewComplexAHP --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),2*Clauseweight(ConstPrio,3,1,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),8*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_fc3fb6907f504dffe1a6181663296b37fe358480' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 -Ginvfreqconstmin -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5))\' ', # new_mzt_small 'protokoll_atpstr_my_2af8b399ea0b8c22c6fc1b13069ad80214f9fa8b' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 5.0,, 6, 80,1.0)\' -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-reuse-defs -tKBO -H\'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*FIFOWeight(PreferProcessed),10*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_2d0c1ae7703dba890de879a4f4409a64f9856908' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.5,, 2, 60,1.0)\' --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --oriented-simul-paramod --split-aggressive --split-reuse-defs -tLPO4 -H\'(1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),8*Clauseweight(ConstPrio,3,1,1),2*Clauseweight(PreferProcessed,1,1,1),2*FIFOWeight(PreferProcessed),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_40306ce1a432dd48c918ac611d77fc5069b2fbc7' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Garity -WSelectComplexG --simul-paramod -tKBO -H\'(2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),10*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio),4*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_43029cedefea4858aae9c4ebd6be482056ce22f4' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --simul-paramod -tKBO -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(PreferProcessed),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_9cb7c8ca63fd56afb053ade56353a3b00eee7e6a' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.2,, 4, 100,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 --split-reuse-defs -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed))\' ', 'protokoll_atpstr_my_9f72062a403172caf26fbe878a32becf1403c276' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 2.0,, 3, 20,1.0)\' -Garity -WSelectComplexG --simul-paramod --split-clauses=7 --split-reuse-defs -tKBO -H\'(4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),6*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),10*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_9fde028f05afb32f97bced19843d73b32d923682' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --oriented-simul-paramod --split-aggressive -tKBO -H\'(1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),2*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_c0d9db6a7b7a90437bd07739f25aa91c0ffc1607' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -Ginvfreqconstmin -WSelectComplexG --simul-paramod --split-clauses=4 -tKBO -H\'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(PreferProcessed),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_c13d4886baa4fa2cef7b4f50892895255b04b078' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 2.0,, 1, 80,1.0)\' --forward-context-sr -Garity -WSelectMaxLComplexAvoidPosPred --simul-paramod -tKBO -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_d60b37aca40b6e560cee4bde2efc36c05a24873f' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 -Garity -WSelectComplexG --simul-paramod -tLPO4 -H\'(1*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_atpstr_my_edc94794a7d25c504761344c2a8b4afaac43a2d0' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 5.0,, , 100,1.0)\' --forward-context-sr -Ginvfreqconstmin -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-clauses=4 --split-reuse-defs -tKBO -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_f67d73f57ffeda22ddd93400237cd848911520e5' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 -Garity -WSelectComplexG --simul-paramod --split-aggressive --split-clauses=4 -tLPO4 -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(PreferProcessed))\' ', 'protokoll_atpstr_my_f9ecf400d7420b0148b2ef7cf4b1498512cf83fd' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred --simul-paramod -tLPO4 -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1))\' ', 'protokoll_atpstr_my_fe548d15a6fc730fd350de634ad9d912ae198efd' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --simul-paramod --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectMaxLComplexAvoidPosPred -H\'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))\' ', # tptpuns1: (overlapping with others, plus some more mepo) # protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3 # protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219 # protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd # protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91 protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y # protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113 protokoll_my8simple_sine13 # protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a protokoll_atpstr_my_304d2e324da665c057353a60ddd91c0712280c88 # protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3 protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf 'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 2.0,, , 500,1.0)\' -Ginvfreqconstmin -WSelectComplexG --split-aggressive -tLPO4 -warity -H\'(1*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*ClauseWeightAge(ConstPrio,1,1,1,3),4*Clauseweight(ConstPrio,3,1,1),4*FIFOWeight(ByNegLitDist),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),2*FIFOWeight(SimulateSOS),6*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),6*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),2*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),6*RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1),8*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),10*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),3*rweight21_a,3*rweight21_g,3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),4*Refinedweight(PreferNonGoals,2,1,2,3,0.8),6*Refinedweight(PreferGoals,1,2,2,1,0.8),20*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_2af8141978cb6a38e97452761cdbd9e1007307fd' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.1,, 1, 60,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectNewComplexAHP --simul-paramod --split-reuse-defs -tAuto -wfreqrank -H\'(4*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),12*Clauseweight(ConstPrio,3,1,1),8*Clauseweight(ConstPrio,1,1,1),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),8*OrientLMaxWeight(ConstPrio,2,1,2,1,1),8*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),1*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),2*RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1),10*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),10*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),1*rweight21_a,2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Refinedweight(PreferNonGoals,2,1,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),8*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),4*Refinedweight(SimulateSOS,1,1,2,1.5,2),8*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.1,, 1, 60,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectNewComplexAHP --split-clauses=4 -tLPO4 -winvprecedence -H\'(6*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),8*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),8*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),10*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,3,1,1),6*Clauseweight(ConstPrio,1,1,1),2*Clauseweight(PreferProcessed,1,1,1),6*FIFOWeight(ByNegLitDist),1*FIFOWeight(ConstPrio),2*FIFOWeight(SimulateSOS),8*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),8*RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1),2*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),6*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),8*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),5*rweight21_g,3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Refinedweight(PreferNonGoals,2,1,2,2,2),2*Refinedweight(PreferNonGoals,2,1,2,3,0.8),8*Refinedweight(PreferGoals,1,2,2,1,0.8),10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),20*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_acfc28483a7c3604da62fc690beab73ca22404d3' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.1,, , 20,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectComplexG -tAuto -wprecedence -H\'(10*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),6*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),10*ClauseWeightAge(ConstPrio,1,1,1,3),1*Clauseweight(ByCreationDate,2,1,0.8),8*Clauseweight(ConstPrio,3,1,1),4*Clauseweight(ConstPrio,1,1,1),8*FIFOWeight(ByNegLitDist),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),6*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),8*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),10*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),1*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),2*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),1*rweight21_a,5*rweight21_g,1*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Refinedweight(PreferNonGoals,2,1,2,2,2),6*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Refinedweight(PreferGoals,1,2,2,1,0.8),1*Refinedweight(PreferGoals,1,2,2,2,0.5),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2),2*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.5,, 3, 40,1.0)\' --forward-context-sr -winvfreqrank -c1 -Ginvfreq -WSelectNewComplexAHP --simul-paramod --split-aggressive --split-clauses=4 -tLPO4 -winvfreqrank -H\'(8*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),4*Clauseweight(ConstPrio,3,1,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --strong-destructive-er --destructive-er-aggressive --destructive-er --presat-simplify -tKBO6 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=1024000000 -WSelectMaxLComplexAvoidPosPred -H\'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_G-E--_200_B02_F1_SE_CS_SP_PI_S0S' => ' --definitional-cnf=24 --simul-paramod --forward-context-sr --strong-destructive-er --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=1024000000 -WSelectComplexG -H\'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),8*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_G-E--_208_B07_F1_SE_CS_SP_PS_S0Y' => ' --definitional-cnf=24 --simul-paramod --presat-simplify --forward-context-sr --strong-destructive-er --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreq -F1 --delete-bad-limit=1024000000 -WSelectMaxLComplexAvoidPosPred -WSelectMaxLComplexAvoidPosPred -H\'(1*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(PreferProcessed),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_7cec1e0745ab65767d5d930d1f61b255ba334c2c' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 1.5,, 4, 10,1.0)\' -winvfreqrank -c1 -Ginvfreq -WSelectComplexG --split-aggressive --split-reuse-defs -tLPO4 -wprecedence -H\'(2*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),6*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),6*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),4*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),8*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),2*ClauseWeightAge(ConstPrio,1,1,1,3),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(ConstPrio,1,1,1),10*FIFOWeight(ByNegLitDist),2*FIFOWeight(PreferProcessed),1*FIFOWeight(SimulateSOS),2*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),1*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),6*RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1),6*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),6*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),8*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),1*rweight21_g,2*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),6*Refinedweight(PreferNonGoals,2,1,2,3,0.8),8*Refinedweight(PreferGoals,1,2,2,1,0.8),2*Refinedweight(PreferGoals,1,2,2,2,0.5),8*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_669419966351e1ca0e0249835d78cd1d51901ee0' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.1,, , 200,1.0)\' --forward-context-sr --presat-simplify -winvfreqrank -c1 -Ginvfreq -WSelectNewComplexAHP --simul-paramod --split-reuse-defs -tLPO4 -winvfreqranksquare -H\'(10*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),4*ClauseWeightAge(ConstPrio,1,1,1,3),1*Clauseweight(ByCreationDate,2,1,0.8),2*Clauseweight(ConstPrio,3,1,1),4*Clauseweight(ConstPrio,1,1,1),4*FIFOWeight(ByNegLitDist),1*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),10*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),3*rweight21_a,7*rweight21_g,10*Refinedweight(PreferNonGoals,2,1,2,2,2),6*Refinedweight(PreferGoals,1,2,2,1,0.8),1*Refinedweight(PreferGoals,1,2,2,2,0.5),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Refinedweight(SimulateSOS,1,1,2,1.5,2),6*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_788faa8a55fdc886d26091ff2d2d22d28e92cd18' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 2.0,, 2, 200,1.0)\' --forward-context-sr -Garity -WSelectComplexG --simul-paramod --split-aggressive -tLPO4 -winvfreqrank -H\'(2*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),6*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),2*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),7*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),2*ClauseWeightAge(ConstPrio,1,1,1,3),1*Clauseweight(ByCreationDate,2,1,0.8),2*Clauseweight(ConstPrio,1,1,1),8*FIFOWeight(ByNegLitDist),2*FIFOWeight(PreferProcessed),2*FIFOWeight(SimulateSOS),4*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),6*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),8*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),10*RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1),8*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),6*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),6*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),1*rweight21_g,8*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Refinedweight(PreferNonGoals,2,1,2,2,2),4*Refinedweight(PreferNonGoals,2,1,2,3,0.8),8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferGoals,1,2,2,2,0.5),2*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_atpstr_my_f40895a2c8bc7dc39944895b1017297da944cf26' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.1,, , 10,1.0)\' -Ginvfreqconstmin -WSelectNewComplexAHP --simul-paramod --split-clauses=7 --split-reuse-defs -tAuto -wfreqcount -H\'(2*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),2*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),6*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),8*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),8*ClauseWeightAge(ConstPrio,1,1,1,3),2*Clauseweight(ConstPrio,3,1,1),2*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(PreferProcessed,1,1,1),6*FIFOWeight(ByNegLitDist),1*FIFOWeight(ConstPrio),2*FIFOWeight(PreferProcessed),1*OrientLMaxWeight(ConstPrio,2,1,2,1,1),8*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),2*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),6*RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1),4*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),6*RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1),8*RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1),7*rweight21_a,9*rweight21_g,8*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),4*Refinedweight(PreferNonGoals,2,1,2,2,2),1*Refinedweight(PreferGoals,1,2,2,1,0.8),2*Refinedweight(PreferGoals,1,2,2,2,0.5))\' ', 'protokoll_atpstr_my_8fe521b01b9230ea30e54ce145b8d2da7be7288c' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, hypos, 5.0,, , 100,1.0)\' --forward-context-sr -Ginvfreqconstmin -WSelectMaxLComplexAvoidPosPred --simul-paramod --split-aggressive --split-clauses=4 -tLPO4 -H\'(6*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*Clauseweight(ByCreationDate,2,1,0.8),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(ConstPrio),1*FIFOWeight(PreferProcessed),10*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Refinedweight(PreferNonGoals,2,1,2,2,2),1*Refinedweight(PreferGoals,1,2,2,1,0.8),1*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),4*Refinedweight(SimulateSOS,1,1,2,1.5,2))\' ', 'protokoll_atpstr_my_9988913949a09383c8314709e779dee99a7ac060' => ' --definitional-cnf=24 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -F1 --delete-bad-limit=150000000 --sine=\'GSinE(CountFormulas, , 1.5,, 3, 100,1.0)\' --forward-context-sr --presat-simplify -Garity -WSelectComplexG --oriented-simul-paramod --split-aggressive --split-clauses=4 --split-reuse-defs -tLPO4 -winvfreqranksquare -H\'(8*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),2*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),6*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),2*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),10*ClauseWeightAge(ConstPrio,1,1,1,3),1*Clauseweight(ByCreationDate,2,1,0.8),8*Clauseweight(ConstPrio,3,1,1),10*Clauseweight(ConstPrio,1,1,1),4*FIFOWeight(ByNegLitDist),2*FIFOWeight(PreferProcessed),1*FIFOWeight(SimulateSOS),4*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),8*RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1),10*RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1),1*rweight21_a,3*rweight21_g,3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferGoals,1,2,2,2,0.5),2*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),6*Refinedweight(SimulateSOS,1,1,2,1.5,2),1*Refinedweight(SimulateSOS,3,2,2,1.5,2))\' ', 'protokoll_X----_sauto_schedule' => ' --delete-bad-limit=1024000000 --auto-schedule ', 'protokoll_H----_042_B03_F1_AE_Q4_SP_S2S' => ' --definitional-cnf=24 -s --delete-bad-limit=1024000000 --split-reuse-defs --split-clauses=4 -F1 --simul-paramod -WSelectNewComplexAHP --destructive-er-aggressive --destructive-er -tLPO4 -Ginvarity --tstp-in -H\'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))\' ' ); my %gfeatnrstd = (); # for each feature, the number of times it appeared - if only once, we could treat it specially my %ggfeatnrnrm = (); # LoadTermTable($filename,$ref2trm_hash,$offset) # # Expects a file created by running fofshared, containing list of # shared term codes for references. Loads them into $ref2trm_hash, # shifting the features numbering by $offset. sub LoadTermTable { my ($filename,$ref2trm_hash,$offset) = @_; open(TRMSTD, "$filename") or die "Cannot read $filename file"; while($_=) { chop; m/^terms\( *([^ ,]+) *, *\[(.*)\] *\)\./ or die "Bad terms info: $_"; my ($ref, $trms) = ($1, $2); my @trms = split(/, */, $trms); die "Duplicate reference $ref in $_" if exists $$ref2trm_hash{$ref}; $$ref2trm_hash{$ref} = []; my ($sym); foreach $sym (@trms) { # $sym =~ m/^ *([0-9]+) */ or die "Bad term code $sym in $_"; push(@{$$ref2trm_hash{$ref}}, $sym); # $1 + $offset); } } close TRMSTD; } sub LoadTermTable1 { my ($filename,$ref2trm_hash,$offset) = @_; open(TRMSTD, "$filename") or die "Cannot read $filename file"; while($_=) { chop; m/^terms\( *([^ ,]+) *, *\[(.*)\] *\)\./ or die "Bad terms info: $_"; my ($ref, $trms) = ($1, $2); my @trms = split(/ +/, $trms); die "Duplicate reference $ref in $_" if exists $$ref2trm_hash{$ref}; $$ref2trm_hash{$ref} = []; my ($sym); foreach $sym (@trms) { # $sym =~ m/^ *([0-9]+) */ or die "Bad term code $sym in $_"; push(@{$$ref2trm_hash{$ref}}, $sym); # $1 + $offset); } } close TRMSTD; } # assumes that refsyms and trmnrm and stdtrm exist already, retutns # (\%grefnr, \%gsymnr, \%grefsyms, \@gnrref, \%greftrmstd, \%greftrmnrm); sub CreateTables { my ($filestem,$addsuffix) = @_; my ($ref,$sym,$trms,@syms,$psyms,$fsyms); my $sfx = (defined $addsuffix)? $addsuffix: ''; open(REFSYMS, "$MTMP/$filestem.refsyms$sfx") or die "Cannot read refsyms$sfx file"; open(REFNR, ">$MTMP/$filestem.refnr$sfx") or die "Cannot write refnr$sfx file"; open(SYMNR, ">$MTMP/$filestem.symnr$sfx") or die "Cannot write symnr$sfx file"; my %grefnr = (); my %gsymnr = (); my %grefsyms = (); my @gnrsym = (); my @gnrref = (); my %greftrmstd = (); my %greftrmnrm = (); while($_=) { chop; # if there is apostrophe, we are in trouble - just add equality if(m/^symbols\( *([^ ,]+) *,.*'.*/) { ($ref, $psyms, $fsyms) = ($1,'=/2/1',''); } else { m/^symbols\( *([^ ,]+) *, *\[(.*)\] *, *\[(.*)\] *\)\./ or die "Bad symbols info: $_"; ($ref, $psyms, $fsyms) = ($1, $2, $3); } my @psyms = split(/\,/, $psyms); my @fsyms = split(/\,/, $fsyms); die "Duplicate reference $ref in $_" if exists $grefnr{$ref}; $grefsyms{$ref} = []; push(@gnrref, $ref); $grefnr{$ref} = $#gnrref; print REFNR "$ref\n"; ## this now also remembers arity and symbol kind in %gsymarity foreach $sym (@psyms) { $sym =~ m/^ *([^\/]+)[\/]([^\/]+)[\/].*/ or die "Bad symbol $sym in $_"; push(@{$grefsyms{$ref}}, $1); } foreach $sym (@fsyms) { $sym =~ m/^ *([^\/]+)[\/]([^\/]+)[\/].*/ or die "Bad symbol $sym in $_"; push(@{$grefsyms{$ref}}, $1); } } close REFNR; close REFSYMS; LoadTermTable("$MTMP/$filestem.trmstd$sfx",\%greftrmstd,0); # if($gdotrmstd > 0); LoadTermTable1("$MTMP/$filestem.trmnrm$sfx",\%greftrmnrm,0); # if($gdotrmnrm > 0); return (\%grefnr, \%grefsyms, \@gnrref, \%greftrmstd, \%greftrmnrm); } sub PrepareTables { my ($filestem) = @_; system("cd $MTMP; $MBIN/e_axfilter -f$MBIN/00filter --tstp-format $filestem.p"); my $faxfilter = $filestem . '_axfilter_auto'; # allasax is the sine-filtered version system("cat $MTMP/$faxfilter* | sort -u > $MTMP/$filestem.allasax"); # create the refsyms file `cat $MTMP/$filestem.allasax | $MBIN/GetSymbols -- > $MTMP/$filestem.refsyms`; # create the trmstd and trmnrm files `sed -e 's/^cnf(/fof(/' $MTMP/$filestem.allasax | $gshgenfeatureprgstd - > $MTMP/$filestem.trmstd`; my %gref2fla = (); my %gconjectures = (); my $gprobkind = 'fof'; my $gconjstatus = 'conjecture'; # these are all empty if the problem is cnf my %gref2cnf = (); my %gcnfconjectures = (); my $gcnfconjstatus = 'negated_conjecture'; my @lines1 = `cat $MTMP/$filestem.allasax`; foreach $_ (@lines1) { if(m/^ *(cnf|fof)\( *([^, ]+) *, *([^, ]+) *,(.*)/) { $gprobkind = 'cnf' if('cnf' eq $1); my ($nm,$status,$rest)=($2,$3,$4); if(! (exists $gref2fla{$nm})) { $gref2fla{$nm} = $rest . "\n"; if($status =~ m/conjecture/) { $gconjectures{$nm} = (); $gconjstatus = $status; } } else { mywarn "Duplicate formula name: $nm\n"; } } } my $fofsh_pid = open(FOFSH,"|$gshgenfeatureprgnrm - > $MTMP/$filestem.trmnrm"); foreach my $line (@lines1) { if($gprobkind eq 'cnf') { $line =~ s/^cnf/fof/; } $line =~ s/([\(, ])[A-Z][a-zA-Z0-9_]*/$1A/g; if(length($line) < 5000) {print FOFSH $line}; } close(FOFSH); # make a cheaply cnf-ied version to run sine (and possibly other selectors) on # - this omits the 0-th 10k block - too big afeter cnf system("mv $MTMP/$faxfilter*0.p $MTMP/nocnfax0.p"); system("cat $MTMP/$faxfilter* | sort -u | $MBIN/eprover -R --tstp-format --free-numbers --cnf | perl -e 'while(<>) { if(length($_) < 5000) {print $_}}' > $MTMP/$filestem.cnf"); if($gprobkind eq 'cnf') { my %grefnrcnf = (); my %grefsymscnf = (); my @gnrrefcnf = (); my %greftrmstdcnf = (); my %greftrmnrmcnf = (); return (\%gref2fla, \%gconjectures, $gconjstatus, $gprobkind, \%gref2cnf, \%gcnfconjectures, $gcnfconjstatus, CreateTables($filestem), \%grefnrcnf, \%grefsymscnf, \@gnrrefcnf, \%greftrmstdcnf, \%greftrmnrmcnf); } else { # create the refsyms cnf file `cat $MTMP/$filestem.cnf | $MBIN/GetSymbols -- > $MTMP/$filestem.refsymscnf`; # create the trmstd and trmnrm files for cnf `sed -e 's/^cnf(/fof(/' $MTMP/$filestem.cnf | $gshgenfeatureprgstd - > $MTMP/$filestem.trmstdcnf`; my @lines2 = `cat $MTMP/$filestem.cnf`; foreach $_ (@lines2) { if(m/^ *(cnf|fof)\( *([^, ]+) *, *([^, ]+) *,(.*)/) { my ($nm,$status,$rest)=($2,$3,$4); if(! (exists $gref2cnf{$nm})) { $gref2cnf{$nm} = $rest . "\n"; if($status =~ m/conjecture/) { $gcnfconjectures{$nm} = (); $gcnfconjstatus = $status; } } else { mywarn "Duplicate formula name: $nm\n"; } } } my $cnfsh_pid = open(FOFSH,"|$gshgenfeatureprgnrm - > $MTMP/$filestem.trmnrmcnf"); foreach my $line (@lines2) { $line =~ s/^cnf/fof/; $line =~ s/([\(, ])[A-Z][a-zA-Z0-9_]*/$1A/g; if(length($line) < 5000) { print FOFSH $line }; } close(FOFSH); return (\%gref2fla, \%gconjectures, $gconjstatus, $gprobkind, \%gref2cnf, \%gcnfconjectures, $gcnfconjstatus, CreateTables($filestem), CreateTables($filestem,'cnf')); } } # there are no known references for flas in the file my %gminrefs = (); my $gprintfullseq = 1; # print the full sequence instead of just the # allowed formulas, things need to be filtered # afterwards - this corresponds to the original # CADE24 version ## test: time perl -e 'use AITP_Data; my ($gref2fla, $gconjectures, $gprobkind, $grefnr, $grefsyms, $gnrref, $greftrmstd, $greftrmnrm) = AITP_Data::PrepareTables("bla"); my %gminrefs = (); my $gprintfullseq = 1; my %gstdnr = (); my %gnrmnr = (); AITP_Data::PrepareKNNTrain("bla", 0, $gminrefs, $grefsyms, $greftrmstd, $greftrmnrm, \%gstdnr, \%gnrmnr); ' # prepare the files used by knn and lsi # in particular, merge the ref/feature info into just one line for each formula # minatprefs and minitprefs might be undefined sub PrepareKNNTrain { my ($filestem, $iter, $minrefs, $grefsyms, $greftrmstd, $greftrmnrm, $gstdnr, $gnrmnr, $minatprefs, $minitprefs) = @_; open(ALLFEATSYM,">$MTMP/$filestem.allfeatsym_$iter") or die; open(ALLFEATSTD,">$MTMP/$filestem.allfeatstd_$iter") or die; open(ALLFEATNRM,">$MTMP/$filestem.allfeatnrm_$iter") or die; # open(ALLFEATLSI,">$MTMP/$filestem.allfeatlsi_$iter") or die; open(ALLREFS,">$MTMP/$filestem.allminrefs_$iter") or die; if(defined $minatprefs) { open(ALLATPREFS,">$MTMP/$filestem.allatprefs_$iter") or die; } if(defined $minitprefs) { open(ALLITPREFS,">$MTMP/$filestem.allitprefs_$iter") or die; } if($gprintfullseq == 1) { open(ALLSEQ,">$MTMP/$filestem.allseq_$iter") or die; } my $s = scalar(keys %$gstdnr); my $n = scalar(keys %$gnrmnr); # print ALLFEATLSI scalar(keys %$grefsyms), "\n"; foreach my $k (sort keys %$grefsyms) { # my $syms = join(", ", @{$grefsyms->{$k}}); # my $trmstd = join(", ", @{$greftrmstd->{$k}}); # my $trmnr = join(", ", @{$greftrmstd->{$k}}); my $trmstd = join(", ", map {if(!exists($gstdnr->{$_})) {$gstdnr->{$_}=$s++}; '"' . $gstdnr->{$_} . '"'} @{$greftrmstd->{$k}}); my @trmnrmarr = map {if(!exists($gnrmnr->{$_})) {$gnrmnr->{$_}=$n++}; $gnrmnr->{$_} } @{$greftrmnrm->{$k}}; my $trmnrm = join(", ", map { '"' . $_ . '"'} @trmnrmarr); # print "here: $trmstd\n$trmnrm\n"; print ALLFEATSYM ($k,":",join(", ", map { '"' . $_ . '"'} @{$grefsyms->{$k}}),"\n"); print ALLFEATSTD ($k,":",join(", ", (map { '"' . $_ . '"'} @{$grefsyms->{$k}}), $trmstd),"\n"); print ALLFEATNRM ($k,":",join(", ", (map { '"' . $_ . '"'} @{$grefsyms->{$k}}), $trmnrm),"\n"); # print ALLFEATLSI (join(" ", (@{$grefsyms->{$k}}, @trmnrmarr)),"\n"); print ALLSEQ ($k,"\n") if($gprintfullseq = 1); } foreach my $k (sort keys %$grefsyms) { my @refs = exists($minrefs->{$k})? ($k, @{$minrefs->{$k}}) : ($k); print ALLREFS ($k,":",join(" ", @refs),"\n"); } if(defined $minatprefs) { foreach my $k (sort keys %$grefsyms) { my @refs = exists($minatprefs->{$k})? ($k, @{$minatprefs->{$k}}) : ($k); print ALLATPREFS ($k,":",join(" ", @refs),"\n"); } } if(defined $minitprefs) { foreach my $k (sort keys %$grefsyms) { my @refs = exists($minitprefs->{$k})? ($k, @{$minitprefs->{$k}}) : ($k); print ALLITPREFS ($k,":",join(" ", @refs),"\n"); } } close(ALLFEATSYM); close(ALLFEATSTD); close(ALLFEATNRM); # close(ALLFEATLSI); close(ALLREFS); close(ALLATPREFS) if(defined $minatprefs); close(ALLITPREFS) if(defined $minitprefs); if($gprintfullseq == 1) { close ALLSEQ; } } sub Method2Name { return join('-',@_); } sub Name2Method { return split('-',$_[0]); } my %MPTP1kPredSlices = (); # initialize %MPTP1kPredSlices foreach my $str (@gMizGreedStrats0) { my ($mnm,$slice,$prot) = @$str; if(exists $MPTP1kPredSlices{$mnm}{$slice}) { push(@{$MPTP1kPredSlices{$mnm}{$slice}}, $prot); } else { $MPTP1kPredSlices{$mnm}{$slice} = [$prot]; } } ## test: perl -e 'use AITP_ProblemIO; ($category, $training_directory, $batches) = AITP_ProblemIO::ReadLTBData("BatchSampleLTBHOL"); print "$category,$training_directory\n"; use AITP_Data; ($minrefs,$c)= AITP_Data::DirProofSummary("$training_directory/Solutions"); ($w,$c,)= AITP_Data::DirIncludeFiles("$training_directory/Axioms"); AITP_Data::PrepareTables("","bla");' # prepare the training data - features and refs, returns the global tables: # (\%gref2fla, \%grefnr, \%gsymnr, \%gsymarity, \%grefsyms, \@gnrsym, \@gnrref, \%greftrmstd, \%greftrmnrm); # AITP_Data::PrepareKNNTest("$MTMP/$conj/$conj.test", $iter, $conj, $grefsyms, $greftrmstd, $greftrmnrm, \%gstdnr, \%gnrmnr,\%allowed, $gmode, $gminrefs, $gatpminrefs, $gitprefs); # prepare the test files used by knn # now also the train files for the external predictors sub PrepareKNNTest { my ($filepath, $iter, $conj, $grefsyms, $greftrmstd, $greftrmnrm, $gstdnr, $gnrmnr, $mode, $minrefs, $minatprefs, $minitprefs) = @_; open(ALLFEATSYM,">$filepath.sym") or die; open(ALLFEATSTD,">$filepath.std") or die; open(ALLFEATNRM,">$filepath.nrm") or die; # open(SEQ,">$filepath.seq") or die; # open(MINREFS,">$filepath.minrefs") or die; # if(defined $minatprefs) { open(ATPREFS,">$filepath.atprefs") or die; } # if(defined $minitprefs) { open(ITPREFS,">$filepath.itprefs") or die; } my $s = scalar(keys %$gstdnr); my $n = scalar(keys %$gnrmnr); # my $syms = join(", ", @{$grefsyms->{$conj}}); # my $trmstd = join(", ", @{$greftrmstd->{$k}}); # my $trmnr = join(", ", @{$greftrmstd->{$k}}); my %conjsym = (); my %conjstd = (); my %conjnrm = (); foreach my $cj (keys %$conj) { @conjsym{ @{$grefsyms->{$cj}} } = (); @conjstd{ @{$greftrmstd->{$cj}} } = (); @conjnrm{ @{$greftrmnrm->{$cj}} } = (); } my $trmstd = join(", ", map {if(!exists($gstdnr->{$_})) {$gstdnr->{$_}=$s++}; '"' . $gstdnr->{$_} . '"' } (keys %conjstd)); my $trmnrm = join(", ", map {if(!exists($gnrmnr->{$_})) {$gnrmnr->{$_}=$n++}; '"' . $gnrmnr->{$_} . '"' } (keys %conjnrm)); # my $conjs = $conj . ":"; my $conjs = ''; if($mode eq 'MizGreed1') { $conjs = '';} print ALLFEATSYM ($conjs,join(", ", map { '"' . $_ . '"'} (keys %conjsym)),"\n"); print ALLFEATSTD ($conjs,join(", ", (map { '"' . $_ . '"'} (keys %conjsym)), $trmstd),"\n"); print ALLFEATNRM ($conjs,join(", ", (map { '"' . $_ . '"'} (keys %conjsym)), $trmnrm),"\n"); # print SEQ join("\n",sort keys %$allowed),"\n"; # foreach my $k (sort keys %$allowed) # { # print SEQ $k,"\n"; # my @refs0 = exists($minrefs->{$k})? ($k, @{$minrefs->{$k}}) : ($k); # print MINREFS ($k,":",join(" ", @refs0),"\n"); # if(defined $minatprefs) # { # my @refs = exists($minatprefs->{$k})? ($k, @{$minatprefs->{$k}}) : ($k); # print ATPREFS ($k,":",join(" ", @refs),"\n"); # } # if(defined $minitprefs) # { # my @refs = exists($minitprefs->{$k})? ($k, @{$minitprefs->{$k}}) : ($k); # print ITPREFS ($k,":",join(" ", @refs),"\n"); # } # } close(ALLFEATSYM); close(ALLFEATSTD); close(ALLFEATNRM); # close(SEQ); # close(MINREFS); # close(ATPREFS); # close(ITPREFS); } # \%MPTP1kPredSlices is passed as $predslices sub RunPredictionMethod { my ($conjectures,$probkind,$conjstatus, $filestem,$methodnm,$reflimit,$predslices,$iter,$ref2fla) = @_; my $conj = $filestem; # my $methodnm = Method2Name($predictor,$args,$featkind,$depkind); # my $allownr = scalar(keys %$allowed)-1; # my $reflimitm = min($allownr,$reflimit); my $reflimitm = min($reflimit, scalar(keys %$ref2fla)-1); my $seq = ($gprintfullseq == 1)? "$MTMP/$filestem.allseq_$iter" : "$MTMP/$conj.test.seq"; my @slices = keys %{$predslices->{$methodnm}}; die "Undefined method: $methodnm" unless $#slices > -1; my ($predictor,$args,$featkind,$depkind) = Name2Method($methodnm); $depkind = 'min'; # nothing else here return 1 if($predictor eq 'lsi'); my $rfs1; if($predictor eq 'comb') { $args =~ m/^([^:]*):([^:]*)$/ or die "Bad comb method: $args"; my ($maxv,$f1) = ($1, $2); $featkind =~ s/,/-/g; $depkind =~ s/,/-/g; my ($predictor1,$args1,$featkind1,$depkind1) = Name2Method($featkind); my ($predictor2,$args2,$featkind2,$depkind2) = Name2Method($depkind); $depkind1 = 'min'; # nothing else here $depkind2 = 'min'; # nothing else here my $features1 = "$MTMP/$filestem.allfeat" . $featkind1 . '_' . $iter; my $deps1 = ($gprintfullseq == 1)? "$MTMP/$filestem.all$depkind1" . 'refs_' . $iter : "$MTMP/$conj.test.$depkind1" . 'refs'; # my $deps1 = "$MTMP/$conj/$conj.test.$depkind1" . 'refs'; my $features2 = "$MTMP/$filestem.allfeat" . $featkind2 . '_' . $iter; my $deps2 = ($gprintfullseq == 1)? "$MTMP/$filestem.all$depkind2" . 'refs_' . $iter : "$MTMP/$conj.test.$depkind2" . 'refs'; # my $deps2 = "$MTMP/$conj/$conj.test.$depkind2" . 'refs'; my $argss1 = $args1; $argss1 =~ s/:/ /g; my $argss2 = $args2; $argss2 =~ s/:/ /g; my $prmsordered1 = ($predictor1 =~ m/(nbayes|lrnei)/)? "$features1 $deps1 $argss1" : "$argss1 $features1 $deps1"; my $prmsordered2 = ($predictor2 =~ m/(nbayes|lrnei)/)? "$features2 $deps2 $argss2" : "$argss2 $features2 $deps2"; $rfs1 = `cat $MTMP/$conj.test.$featkind1 | $MBIN/$predictor \"$MBIN/$predictor1 $prmsordered1 $reflimitm $seq\" $f1 \"$MBIN/$predictor2 $prmsordered2 $reflimitm $seq\" $maxv $reflimitm $seq | tee $MTMP/$conj.pred.$methodnm`; } else { my $features = "$MTMP/$filestem.allfeat" . $featkind . '_' . $iter; my $deps = ($gprintfullseq == 1)? "$MTMP/$filestem.all$depkind" . 'refs_' . $iter : "$MTMP/$conj/$conj.test.$depkind" . 'refs'; # my $deps = "$MTMP/$conj/$conj.test.$depkind" . 'refs'; # my $deps = "$MTMP/$filestem.all" . $depkind . 'refs_' . $iter; # the colon is used to avoid spaces in file names created by appending $methodnm my $argss = $args; $argss =~ s/:/ /g; my $prmsordered = ($predictor =~ m/(nbayes|lrnei)/)? "$features $deps $argss" : "$argss $features $deps"; $rfs1 = `cat $MTMP/$conj.test.$featkind | $MBIN/$predictor $prmsordered $reflimitm $seq 2>/dev/null | tee $MTMP/$conj.pred.$methodnm`; } my @refs1 = split(/ +/,$rfs1); foreach my $s (@slices) { open(F,">$MTMP/$conj.prob.$methodnm.s$s"); foreach my $cj (keys %$conjectures) { print F ($probkind, '(', $cj, ',', $conjstatus, ',', $ref2fla->{$cj}); } my $i = 0; my $j = -1; while(($i < $s) && ($j < $#refs1)) { $j++; if(!exists($conjectures->{$refs1[$j]})) { $i++; print F ($probkind, '(', $refs1[$j], ',axiom,', $ref2fla->{$refs1[$j]}); } } close(F); } } my $gmode = 'MizGreed1'; my $parallel = 1; my $greflimit = 800; # how many hints we want from the ranker before we do slicing (just for speed up) sub RunPredictions { my ($conjectures,$probkind,$conjstatus,$filestem,$iter,$ref2fla) = @_; my @childs = (); if($gmode eq 'MizGreed1') { my @methods = sort keys %MPTP1kPredSlices; my @chunks = (); # equal-sized chunks, make $parallel number of them foreach my $i (0 .. $parallel-1) { $chunks[$i] = []; } # the methods go into the chunks according to their modulo $parallel foreach my $j (0 .. scalar(@methods) -1) { my $mod = $j % $parallel; push( @{$chunks[$mod]}, $methods[$j]); } foreach my $chunk (@chunks) { my $pid = fork(); if ($pid) { # parent push(@childs, $pid); } elsif ($pid == 0) { foreach my $methodnm (@$chunk) { dprint "\n% Predicting with $methodnm\n"; RunPredictionMethod($conjectures,$probkind,$conjstatus,$filestem,$methodnm,$greflimit, \%MPTP1kPredSlices,$iter,$ref2fla); } exit(0); } else { die "couldn’t fork: $!\n"; } } } foreach (@childs) { waitpid($_, 0);} } sub RunStrategy { my ($strat,$filestem,$tl,$solutionfile) = @_; my $conj = $filestem; my $tl1 = $tl+1; my ($methodnm,$s,$estrat); if($gmode eq 'MizGreed1') { ($methodnm,$s,$estrat) = @$strat; } else { my ($kind,$weighting,$k); ($kind,$weighting,$k,$s,$estrat) = @$strat; $methodnm = "$kind.w$weighting.k$k"; } #my @bla = ($kind,$weighting,$k,$s,$estrat); #foreach my $ff (0..$#bla) { die "Undefined $ff" unless(defined($bla[$ff])) } my $file = "$MTMP/$conj.prob.$methodnm.s$s"; # my $file = "$MTMP/$conj/$conj.prob.$kind.w$weighting.k$k.s$s"; die "Cannot read problem file $file" unless(-r $file); #print "Command: ulimit -t $tl; $MBIN/eprover $sdef{$estrat} --tstp-format -R -s --cpu-limit=$tl $file 2>$file.err.$estrat | grep \"\\(User\\|SZS status\\)\" | tee $file.out.$estrat\n"; die "Unknown strategy: $estrat\n$sdef::\n" unless(exists($sdef{$estrat})); dprint "% Running ", join('.',@$strat), "for $tl s:\n"; my $eparams = $sdef{$estrat}; my @lines = `ulimit -t $tl1; $MBIN/eprover $eparams --free-numbers --tstp-format -R -s --proof-object --print-statistics --cpu-limit=$tl1 --soft-cpu-limit=$tl $file 2>$file.err.$estrat | tee $file.out.$estrat`; foreach $_ (@lines) { if(m/.*SZS status[ :]*(Theorem|Unsatisfiable)/) { mywarn "Proof found by slice ", join('.',@$strat), "\n"; print "# E.T. strategy is ",, join('.',@$strat), "\n"; print @lines; dprint "% Done:$strat\n"; # exit(0); } } dprint "Done:$strat\n"; return; } my @gMizGreedStrats = ( #["ful",0,"protokoll_atpstr_my_37be21ea059a2fcb865621e373a97f33a9d07b12"], #['knn-128-std-min',128,"protokoll_atpstr_my_88760aa43d575e84b7030b8a6188f74ba5f80dc7"], # ["lsi-400:48-nrm-min",160,"protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113"], ['ful',0,'protokoll_atpstr_my_b57035dec1c1e73fa888146ae569c7cc8f05e7a3'], ['ful',0,'protokoll_G-E--_208_C18_F1_SE_CS_SP_PS_S0Y'], ['ful',0,'protokoll_atpstr_my_eba37f91665fc364eeb63558058658ee9a149d9a'], @gMizGreedStrats0, ['ful',0,'protokoll_X----_sauto_schedule'], ['ful',0,'protokoll_atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a'], ['ful',0,'protokoll_atpstr_my_92168ebc2ef464a6f2d6a311a4fa90219fd0aa91'], ['cnf',0,'protokoll_atpstr_my_a3154f3180cc47331f1b05c36960c32e4805a7c5'], ['ful',0,'protokoll_atpstr_my_cfee9ff42189552c6557cda7d36f20820c827219'], ['cnf',0,'protokoll_X----_auto_sine03'], ['ful',0,'protokoll_atpstr_my_7cec1e0745ab65767d5d930d1f61b255ba334c2c'], ['ful',0,'protokoll_atpstr_my_a74b37f2d8b7e35be554fc999f671188cf40f113'], ['cnf',0,'protokoll_atpstr_my_2af8b399ea0b8c22c6fc1b13069ad80214f9fa8b'], ['ful',0,'protokoll_atpstr_my_669419966351e1ca0e0249835d78cd1d51901ee0'], ['ful',0,'protokoll_atpstr_my_788faa8a55fdc886d26091ff2d2d22d28e92cd18'], ['ful',0,'protokoll_atpstr_my_a3154f3180cc47331f1b05c36960c32e4805a7c5'], ['ful',0,'protokoll_atpstr_my_2d0c1ae7703dba890de879a4f4409a64f9856908'], ['ful',0,'protokoll_atpstr_my_e6ff24ca1a5013a612ccffc94da0b282477718de'], ['cnf',0,'protokoll_atpstr_my_edc94794a7d25c504761344c2a8b4afaac43a2d0'], ['ful',0,'protokoll_my8simple_sine13'], ['ful',0,'protokoll_atpstr_my_f40895a2c8bc7dc39944895b1017297da944cf26'], ['ful',0,'protokoll_atpstr_my_8fe521b01b9230ea30e54ce145b8d2da7be7288c'], ['ful',0,'protokoll_atpstr_my_9cb7c8ca63fd56afb053ade56353a3b00eee7e6a'], ['ful',0,'protokoll_atpstr_my_9f72062a403172caf26fbe878a32becf1403c276'], ['ful',0,'protokoll_atpstr_my_a473e2c35f909af4ba00d9f1a7a8a454a851ed9c'], ['ful',0,'protokoll_atpstr_my_1b33b681d9260087e24d422ea286498f4a4b92cf'], ['ful',0,'protokoll_atpstr_my_9988913949a09383c8314709e779dee99a7ac060'], ['cnf',0,'protokoll_atpstr_my_69856783cec8fab1acccfe08bb382ad42c8475df'], ['ful',0,'protokoll_my17simple_sine13'], ['ful',0,'protokoll_atpstr_my_a4a4da5778ba9bebf9bc5e616786c7ad501b1af5'], ['cnf',0,'protokoll_H----_042_B03_F1_AE_Q4_SP_S2S'], ['cnf',0,'protokoll_X----_sauto_300'], ['cnf',0,'protokoll_X----_sauto_schedule'] ); my $gstarttime = time(); my $conjexists = 0; my $gaxcount = 0; # nr of axs in the problem my $ginclude = 0; # this is a problem with included axioms my $gaxdonothinglimit = 15; # nr of axioms when we completely rely on E and do nothing # check that there is a conjecture; if not, just run E open(F,$gfilestem0) or die "bad filename $gfilestem0"; while($_=) # && ($conjexists == 0)) { if(m/^[^%]*, *(negated_)?conjecture\b/) { $conjexists = 1 } elsif(m/^ *(cnf|fof)/) {$gaxcount++} elsif(m/^ *include/) {$ginclude = 1} } close(F); if(($conjexists == 0) || (($gaxcount < $gaxdonothinglimit) && ($ginclude == 0))) { exec("$MBIN/eprover --tstp-format --delete-bad-limit=1024000000 --free-numbers --auto-schedule -R -s --proof-object --print-statistics --cpu-limit=$gtimelimit $gfilestem0"); } # prepare the training features and refs files, so we can run KNN on them # we use the new fofshared (fofshared1) so we can update the hashtable # (\%gref2fla, \%grefnr, \%gsymnr, \%gsymarity, \%grefsyms, \@gnrsym, \@gnrref, \%greftrmstd, \%greftrmnrm); my @gdata = PrepareTables($gfilestem); my ($gref2fla, $gconjectures, $gconjstatus, $gprobkind, $gref2cnf, $gcnfconjectures, $gcnfconjstatus, $grefnr, $grefsyms, $gnrref, $greftrmstd, $greftrmnrm, $grefnrcnf, $grefsymscnf, $gnrrefcnf, $greftrmstdcnf, $greftrmnrmcnf) = @gdata; my %gstdnr = (); my %gnrmnr = (); PrepareKNNTrain($gfilestem, 0, \%gminrefs, $grefsyms, $greftrmstd, $greftrmnrm, \%gstdnr, \%gnrmnr); my $time1 = time(); print "\nTime spent in data preparation:", $time1 - $gstarttime, "\n"; PrepareKNNTest("$MTMP/$gfilestem.test", 0, $gconjectures, $grefsyms, $greftrmstd, $greftrmnrm, \%gstdnr, \%gnrmnr, $gmode, \%gminrefs); RunPredictions($gconjectures,$gprobkind,$gconjstatus,$gfilestem,0,$gref2fla); if($gmode eq 'MizGreed1') { `cp $MTMP/$gfilestem.p $MTMP/$gfilestem.prob.ful.s0`; `cp $MTMP/$gfilestem.cnf $MTMP/$gfilestem.prob.cnf.s0`; } my $time2 = time(); print "\nTime used for predicting $gfilestem: ", $time2 - $gstarttime, "\n"; my $remaining_time = $gtimelimit - ($time2 - $gstarttime); #my $tl1 = max( 1, int( $remaining_time/(1+(scalar @gMizGreedStrats)) )); # it seems that 1+ can be safely removed, we just run the # auto_schedule strategy in the end again (on cnf) if we have time my $tl1 = max( 1, int( $remaining_time/(scalar @gMizGreedStrats)) ); $tl1=2; # if success, the child will exit in RunStrategy foreach my $strat (@gMizGreedStrats[0..$#gMizGreedStrats-1]) { # RunStrategy($strat,$gfilestem,5); RunStrategy($strat,$gfilestem,$tl1); } $remaining_time = int($gtimelimit - (time() - $gstarttime)); $remaining_time=2; RunStrategy($gMizGreedStrats[$#gMizGreedStrats],$gfilestem,$remaining_time); my $status = szs_GAVEUP; print "\n% SZS status $status for $gfilestem\n"; exit;