From d88fd4e939a9bce32192fa052039d83bccc1f309 Mon Sep 17 00:00:00 2001
From: CDC08x <cdc08x@gmail.com>
Date: Wed, 16 Feb 2022 09:12:17 +0100
Subject: [PATCH] Tyding up

---
 ...-plot-best-per-category_best_performer.pdf |  Bin 61537 -> 61537 bytes
 ...est-per-category_min_unsat_core_finder.pdf |  Bin 61820 -> 61820 bytes
 ...ot-best-performance-pie_best_performer.pdf |  Bin 58419 -> 58419 bytes
 ...lot-best-ucs-pie_min_unsat_core_finder.pdf |  Bin 58259 -> 58259 bytes
 ...J-analysis-results-plot-clauses_v_time.pdf |  Bin 123973 -> 123973 bytes
 ...re-cardinality-scatter_AALTAF-v-NuSMVB.pdf |  Bin 57992 -> 57992 bytes
 ...re-cardinality-scatter_AALTAF-v-NuSMVS.pdf |  Bin 57663 -> 57663 bytes
 ...ore-cardinality-scatter_AALTAF-v-TRPPP.pdf |  Bin 59643 -> 59643 bytes
 ...re-cardinality-scatter_NuSMVB-v-NuSMVS.pdf |  Bin 57601 -> 57601 bytes
 ...ore-cardinality-scatter_NuSMVB-v-TRPPP.pdf |  Bin 57857 -> 57857 bytes
 ...ore-cardinality-scatter_NuSMVS-v-TRPPP.pdf |  Bin 57589 -> 57589 bytes
 .../AIJ-results-virtual_best_info.csv         |   27 -
 .../AIJ-results_virtual-best_info.csv         | 1378 +++++++++++++++++
 ...lsx => AIJ-results_virtual-best_info.xlsx} |  Bin
 ...results_virtual-best_info_per-category.csv |   27 +
 .../run-AIJ-results-analysis.py               |   44 +-
 16 files changed, 1439 insertions(+), 37 deletions(-)
 delete mode 100644 etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results-virtual_best_info.csv
 create mode 100644 etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info.csv
 rename etc/AIJ-SAT-explorer/AIJ-analysis-plots/{AIJ-results-virtual_best_info.xlsx => AIJ-results_virtual-best_info.xlsx} (100%)
 create mode 100644 etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info_per-category.csv

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-per-category_best_performer.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-per-category_best_performer.pdf
index 7918781bd63b49f29b855ace7eaf923dfa7b740d..174d59a8d500495e219fdb506cd34ea0e9942bfe 100644
GIT binary patch
delta 22
ecmaF(fcfDA<_!k#*v$+q4U7%UHk-fGVgdkm1_;Uk

delta 22
ecmaF(fcfDA<_!k#*i8&gj7<#;Hk-fGVgdkl&IrQ*

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-per-category_min_unsat_core_finder.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-per-category_min_unsat_core_finder.pdf
index dbf4d4481a4b0a64e509089ee76f7cd9621f2983..8943afa48a003ed1a136e433c6077475b4078fc0 100644
GIT binary patch
delta 22
ecmezKi22VW<_+HO+06_r4U7%UHwV4fVgdkszX?46

delta 22
ecmezKi22VW<_+HO*-Z>hj7<#;HwV4fVgdkshY2<S

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-performance-pie_best_performer.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-performance-pie_best_performer.pdf
index a07cfbf4cd380c658b4cf46d2087dbdc5f2a649e..3ece5d071a7fea88c72d956d97e7bcf45c3576d8 100644
GIT binary patch
delta 22
ecmdmdf_d`^<_%1b*v$+q4U7#;Hgi7GVgdkWz6Zzv

delta 22
ecmdmdf_d`^<_%1b*i8&gj7>}}Hgi7GVgdkW-3QMA

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-ucs-pie_min_unsat_core_finder.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-best-ucs-pie_min_unsat_core_finder.pdf
index 11e75d7d3558518f53962f0b828184cd10950f31..ad3677a0f25a6b1f95130770139fcc06cb74aec1 100644
GIT binary patch
delta 22
ecmbPyoO$wb<_$>?+06_r4U7%UHfKK6VgdkYk_bis

delta 22
ecmbPyoO$wb<_$>?*-Z>hj7>}}H)lT7VgdkYs|ZX0

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-clauses_v_time.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-clauses_v_time.pdf
index a1424d1e268564c782dafdc5b8386a71fe3d1414..b4d2038344394be3172583690678380cdce71d0d 100644
GIT binary patch
delta 25
hcmX?lg8k?T_J%Et#Shud3@i<d4J@`-J!Cx11OSbK3IhND

delta 25
hcmX?lg8k?T_J%Et#Shs{3{8wp4UD!|J!Cx11OSag3H$&6

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_AALTAF-v-NuSMVB.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_AALTAF-v-NuSMVB.pdf
index 47519d5ce7b5599010ed42b6c20a54f9763fd4b0..13e9c2ce050b11dcfdb4336a67c03f2c407731f4 100644
GIT binary patch
delta 22
dcmeA;%G`03d4ux<b~6J@17icr&0Y`em;hv52m=5B

delta 22
dcmeA;%G`03d4ux<b`wJrV^af@&0Y`em;hue2mJs5

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_AALTAF-v-NuSMVS.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_AALTAF-v-NuSMVS.pdf
index acfc722368ad37030b754ce8b09a5de4464273b9..d70512a81b876fa7c82005c3c8e8e772022b154a 100644
GIT binary patch
delta 22
ecmdmgh<X1Z<_*8@v6~rK8W<Z`Zf3l1#{>X&EeO^C

delta 22
ecmdmgh<X1Z<_*8@v6~p07@HcHY-YS~#{>X%`v}kg

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_AALTAF-v-TRPPP.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_AALTAF-v-TRPPP.pdf
index e52c57d5b5ddbc1d9486afe51035cfdf692383d5..e4b4452ca9266e374594ad9412d21feda1c6d60b 100644
GIT binary patch
delta 22
ecmex;k@@#U<_+7Pv6~rK8W<Z`Zr=OMjtKyPiwW}p

delta 22
ecmex;k@@#U<_+7Pv6~p07@HaxZ{GXNjtKyPQwi(<

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_NuSMVB-v-NuSMVS.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_NuSMVB-v-NuSMVS.pdf
index 3bb62aea19405cbdc1d794ada9d053224de891d1..05e578d11040131bf7a913731e0bf2ddb3f4d48f 100644
GIT binary patch
delta 22
ecmZoX#N2p@dBdK2>}Cd*2F8X4n-AZ!V*&tca|qP{

delta 22
ecmZoX#N2p@dBdK2>?VdL#-;`)n-AZ!V*&tca0u4`

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_NuSMVB-v-TRPPP.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_NuSMVB-v-TRPPP.pdf
index dfbf56c7171b8401e6b2003c95a663b9201643d7..c9db51402a051294aa3c5c672497ba0787ccb2ba 100644
GIT binary patch
delta 22
ecmZoX!rXX-dBdLj>}Cd*2F8X4n-AZ&V*&tc(g@oC

delta 22
ecmZoX!rXX-dBdLj>?VdL#-;`)n-AZ&V*&tc&j{TB

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_NuSMVS-v-TRPPP.pdf b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-analysis-results-plot-unsat-core-cardinality-scatter_NuSMVS-v-TRPPP.pdf
index 294397db20dd688a119675bf3ba03f5552a51314..afb4e083321484e349cfa48d26e94e7eab6e7400 100644
GIT binary patch
delta 22
ecmex*kooID<_#O}v6~rK8W<Z`Zr*;+jtKyLD+#Lr

delta 22
ecmex*kooID<_#O}v6~p07@HcHY~Fs)jtKyK`3a=}

diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results-virtual_best_info.csv b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results-virtual_best_info.csv
deleted file mode 100644
index 2b6810d50..000000000
--- a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results-virtual_best_info.csv
+++ /dev/null
@@ -1,27 +0,0 @@
-category;total;AALTAF@min-UC;AALTAF@min-UC[%];AALTAF@min-timing;AALTAF@min-timing%;TRP++@min-UC;TRP++@min-UC[%];TRP++@min-timing;TRP++@min-timing%;NuSMV-S@min-UC;NuSMV-S@min-UC[%];NuSMV-S@min-timing;NuSMV-S@min-timing%;NuSMV-B@min-UC;NuSMV-B@min-UC[%];NuSMV-B@min-timing;NuSMV-B@min-timing%;None@min-UC;None@min-UC[%];None@min-timing;None@min-timing%
-;1377;690;50.11;1260;91.50;543;39.43;0;0.00;12;0.87;8;0.58;104;7.55;81;5.88;28;2.03;28;2.03
-LTL-as-LTLf/acacia/demo-v3/demo-v3:cl;11;7;63.64;11;100.00;4;36.36;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/alaska/lift/lift;17;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/alaska/lift/lift:b;17;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/alaska/lift/lift:b:f;17;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/alaska/lift/lift:b:f:l;17;15;88.24;16;94.12;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
-LTL-as-LTLf/alaska/lift/lift:b:l;17;14;82.35;17;100.00;3;17.65;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/alaska/lift/lift:f;17;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/alaska/lift/lift:f:l;17;15;88.24;16;94.12;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
-LTL-as-LTLf/alaska/lift/lift:l;17;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/anzu/amba/amba:c;17;15;88.24;15;88.24;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;2;11.76;2;11.76
-LTL-as-LTLf/anzu/amba/amba:cl;17;16;94.12;16;94.12;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
-LTL-as-LTLf/anzu/genbuf/genbuf;20;20;100.00;20;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/anzu/genbuf/genbuf:c;20;20;100.00;20;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/anzu/genbuf/genbuf:cl;20;18;90.00;18;90.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;2;10.00;2;10.00
-LTL-as-LTLf/forobots;38;38;100.00;38;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTL-as-LTLf/rozier/counter/counter;19;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;14;73.68;14;73.68;5;26.32;5;26.32
-LTL-as-LTLf/rozier/counter/counterCarry;19;0;0.00;0;0.00;6;31.58;0;0.00;0;0.00;0;0.00;12;63.16;18;94.74;1;5.26;1;5.26
-LTL-as-LTLf/rozier/counter/counterCarryLinear;19;0;0.00;0;0.00;6;31.58;0;0.00;0;0.00;0;0.00;13;68.42;19;100.00;0;0.00;0;0.00
-LTL-as-LTLf/rozier/counter/counterLinear;18;0;0.00;1;5.56;0;0.00;0;0.00;0;0.00;0;0.00;18;100.00;17;94.44;0;0.00;0;0.00
-LTL-as-LTLf/rozier/formulas/n;30;12;40.00;24;80.00;0;0.00;0;0.00;8;26.67;4;13.33;10;33.33;2;6.67;0;0.00;0;0.00
-LTL-as-LTLf/schuppan/O1formula;27;20;74.07;20;74.07;0;0.00;0;0.00;4;14.81;4;14.81;3;11.11;3;11.11;0;0.00;0;0.00
-LTL-as-LTLf/schuppan/O2formula;27;5;18.52;5;18.52;0;0.00;0;0.00;0;0.00;0;0.00;8;29.63;8;29.63;14;51.85;14;51.85
-LTL-as-LTLf/schuppan/phltl;13;12;92.31;12;92.31;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;7.69;1;7.69
-LTLf-specific/benchmarks:ltlf/LTLfRandomConjunction/C100;500;255;51.00;500;100.00;245;49.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
-LTLf-specific/benchmarks:ltlf/LTLfRandomConjunction/V20;425;127;29.88;425;100.00;272;64.00;0;0.00;0;0.00;0;0.00;26;6.12;0;0.00;0;0.00;0;0.00
diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info.csv b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info.csv
new file mode 100644
index 000000000..8f2efbb14
--- /dev/null
+++ b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info.csv
@@ -0,0 +1,1378 @@
+Test;Clauses;BestTime;BestPerformer;MinUnSATCore;MinUnSATFinder
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n4/P0.7/L50/P0.7N4L50_9;1;0.00058;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N30;95;0.048354;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N43;123;0.031601;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_s1;6;0.006031;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_8;28;0.023399;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_14;27;0.178951;aaltafuc;24;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N40;135;0.027096;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N6;116;0.021004;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N48;124;0.048939;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N5;130;0.019027;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_20_19;41;0.090356;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N13;104;0.019975;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N45;132;0.019442;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N4;132;0.034452;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N5;75;0.016335;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N25;83;0.045264;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N37;130;0.017589;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N5;44;0.007192;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_3;84;0.092677;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N24;110;0.028749;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_40_39;81;2.012413;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N21;133;0.029745;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N37;129;0.029525;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N37;138;0.025727;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N9;58;0.011717;aaltafuc;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear2;6;0.004239;aaltafuc;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec13.negated;1;0.081921;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N43;137;0.040915;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.3/L60/P0.333333333333333N2L60_4;1;0.000617;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_16;330;0.19756;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N12;128;0.10455;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N47;22;0.003308;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N34;100;0.026226;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N13;127;0.018636;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N12;120;0.069732;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N29;22;0.004354;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N24;121;0.017087;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N2;133;0.04401;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N43;109;0.019454;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N12;67;0.024491;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N22;122;0.018231;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N37;126;0.027946;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_11;231;0.141025;aaltafuc;29;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec2.negated;1;0.010559;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec11.negated;1;0.059554;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N14;49;0.011404;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N10;122;0.024673;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N4;99;0.023006;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_14;25;2.538195;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N14;137;0.043192;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N44;127;0.047709;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_l;6;0.007218;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula4;4;0.003907;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_h1;6;0.006839;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_9;31;0.022559;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N18;124;0.03067;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N3;138;0.030024;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N25;131;0.019791;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N17;122;0.018414;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_g;6;0.009623;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N3;96;0.014624;aaltafuc;8;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.5/L20/P0.5N2L20_2.negated;1;0.0;ltlfuc_sat;1;ltlfuc_sat
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_12;260;0.3091;aaltafuc;30;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N13;50;0.029205;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N46;126;0.020668;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N46;132;0.033194;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N13;137;0.066766;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N43;128;0.022728;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N34;140;0.031258;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_6;24;0.012713;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N33;78;0.021272;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N14;126;0.016251;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_4;19;0.073473;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N35;128;0.028878;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N9;142;0.020875;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear3;8;0.04;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula40;42;0.004192;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_14;39;0.029639;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_2;68;0.024704;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N20;53;0.006573;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N25;117;0.019268;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N35;129;0.018369;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N2;102;0.021024;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N27;113;0.030086;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N21;38;0.00707;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N9;130;0.036162;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N29;132;0.018487;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N6;129;0.086361;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N33;138;0.271472;aaltafuc;19;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N42;139;0.039242;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N49;122;0.018351;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N31;140;0.022905;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N32;98;0.012785;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N28;122;0.016149;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula6;6;0.010599;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N30;108;0.024;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_19;431;0.385668;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N7;39;0.01251;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N4;131;0.041102;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N25;130;0.03901;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_13;271;0.171801;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N19;126;0.090311;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N2;125;0.023059;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N31;129;0.040863;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N11;65;0.010203;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N9;77;0.014424;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear4;8;0.06;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_9;22;0.015916;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_mf;6;0.009439;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N9;108;0.017342;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula3;3;0.0;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N50;116;0.016688;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N4;147;0.024673;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N32;134;0.021552;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N10;129;0.055471;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N40;127;0.088328;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N23;95;0.163618;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N48;98;0.01441;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N20;139;0.051362;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N17;66;0.014659;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N29;123;0.05905;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N40;129;0.018997;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N18;144;0.560237;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.3/L10/P0.333333333333333N2L10_6;4;0.0;ltlfuc_sat;2;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N42;135;0.019184;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_4;94;0.077943;aaltafuc;19;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N29;112;0.021917;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N38;88;0.011983;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N13;134;0.05149;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N48;77;0.017389;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N28;142;0.103058;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N39;127;0.064884;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N28;90;0.019979;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_17;31;0.040269;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_18;47;126.698653;aaltafuc;32;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_s1;6;0.007206;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N43;137;0.02673;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N39;34;0.007772;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N32;79;0.024182;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N12;39;0.048857;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N7;93;0.019463;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N15;133;0.038973;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_4;15;0.018216;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N13;139;0.048526;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N29;41;0.008109;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N36;129;0.026333;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N37;119;0.040906;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_16;43;112.525845;aaltafuc;30;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N39;126;0.0326;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N49;135;0.038354;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N34;128;0.037342;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_2;77;0.025856;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N19;56;0.017089;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.5/L100/P0.5N3L100_4.negated;1;0.000772;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N45;133;0.046813;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_9;206;0.115562;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N15;125;0.234247;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N27;101;0.018041;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N3;126;0.042722;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N38;41;0.015353;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_14;281;0.156921;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_17;357;0.263613;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N16;131;0.05015;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N27;42;0.009654;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N26;137;0.097203;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N18;96;0.045835;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N12;54;0.011655;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N43;131;0.142689;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N21;113;0.0205;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N9;63;0.010291;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N38;135;0.028062;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N19;129;0.038129;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N4;131;0.01874;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula300;302;0.050044;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N43;116;0.019637;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N29;133;0.064175;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N37;108;0.032712;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula600;602;0.170966;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N17;41;0.008697;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N45;108;0.017933;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N28;27;0.015685;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N5;134;0.03909;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N2;137;0.033234;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N27;77;0.019785;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_6;151;0.633173;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_13;265;0.144755;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N26;95;0.026196;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N12;134;0.018791;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N33;123;0.014042;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N5;133;0.021343;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_5;128;0.087133;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N10;44;0.006722;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N43;61;0.01104;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N36;72;0.016863;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N44;144;0.153274;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_7;162;0.121576;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_9_8;19;0.010261;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N42;130;0.031339;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N50;142;0.028136;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_10;33;0.031522;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N1;132;0.022884;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N48;127;0.053565;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N11;83;0.019086;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_3;13;0.008012;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N33;92;0.029546;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N1;133;0.056029;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N48;138;0.942277;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N13;145;0.292798;aaltafuc;7;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_13;39;0.029283;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N7;134;0.8808;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula7;7;0.017174;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_16;45;0.087723;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_4;114;0.044065;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N20;135;1.496567;aaltafuc;27;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry5;11;0.48;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N12;93;0.028713;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N38;53;0.008679;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N32;134;0.103417;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_4_3;9;0.003261;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N18;130;0.081185;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N1;108;0.021015;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N21;126;0.018238;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N46;121;0.565797;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_16;27;0.024236;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N44;77;0.014391;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N15;111;0.01624;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N31;128;20.618939;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N44;123;0.031527;aaltafuc;8;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_19;412;0.327109;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N35;47;0.007957;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N21;56;0.011256;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_16;29;0.032457;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/10/N4;13;0.002003;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N24;94;0.014111;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N48;119;0.019454;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N42;146;0.033419;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula6;8;0.0;ltlfuc_bdd;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N4;131;0.03995;aaltafuc;9;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N38;22;0.0057;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N30;146;0.023297;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N2;41;0.00763;aaltafuc;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N26;74;0.071077;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N47;127;0.042482;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N11;141;0.024638;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_12;23;0.017145;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_4;19;0.010975;aaltafuc;7;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula90;92;0.010889;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N32;125;0.023674;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N26;66;0.013098;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N30;132;0.018298;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_4;15;0.005701;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N1;71;0.012522;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N10;71;0.010633;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_17;334;0.32789;aaltafuc;33;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_9;20;0.326975;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N46;53;0.01364;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N36;129;0.021096;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N11;136;0.039376;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N49;138;0.039186;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_8;28;0.91508;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_7;147;0.148524;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N8;106;0.016507;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N9;142;0.023326;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N23;66;0.014762;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N48;64;0.011584;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N36;41;0.006272;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_14;296;2.434876;aaltafuc;40;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N43;129;0.018311;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N10;143;0.058368;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N33;53;0.032213;aaltafuc;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N46;137;0.028821;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N5;122;0.022822;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N43;90;0.017454;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N42;65;0.015787;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N17;131;0.028532;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter5;9;0.21;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N7;56;0.142531;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N43;118;0.021302;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_8;19;0.011509;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N12;126;0.030476;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N44;146;0.054108;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_mh;6;0.007912;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N25;131;0.023127;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N17;132;0.062315;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N33;130;0.034848;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N39;93;0.056837;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.5/L60/P0.5N3L60_4.negated;1;0.000624;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_3_2;7;0.00134;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N17;81;0.013173;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N28;120;0.024053;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N49;132;0.02058;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N13;140;0.036874;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N26;134;0.022511;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec10.negated;1;0.034242;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N15;142;0.047054;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_mf;6;0.006655;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N20;128;0.01699;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N23;126;0.162831;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N41;134;0.095779;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_13;37;1.989452;aaltafuc;24;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N50;119;0.01752;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N27;126;0.138249;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_2;12;0.007951;aaltafuc;1;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N8;94;0.026133;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N50;127;0.063915;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N48;126;0.052187;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N13;128;0.034463;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_5;21;0.007879;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N17;107;0.020242;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N4;133;0.113074;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N46;128;0.019433;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N45;138;0.058863;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_9;20;0.011777;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N29;136;0.02193;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N35;127;0.033846;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_d;6;0.007143;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N9;134;0.023456;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_7_6;15;0.011541;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_7;19;0.010864;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_13;26;0.025142;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_10;23;4.822434;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry2;8;0.03;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_10;33;8.018358;aaltafuc;25;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter3;7;0.02;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N49;25;0.004458;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear2;8;0.02;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula100;102;0.012177;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_10;214;0.123549;aaltafuc;33;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N16;130;0.024379;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N14;139;0.035898;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N6;128;0.019907;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N39;117;0.024151;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N1;114;0.034073;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N9;126;0.031118;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N42;113;0.015862;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N41;130;0.039067;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N46;132;0.028908;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N40;111;0.021211;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec14.negated;1;0.084464;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_17;351;182.597998;aaltafuc;74;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_17;28;0.027458;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N10;130;0.032698;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_10;21;0.508484;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_2;12;0.003191;aaltafuc;1;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N9;128;0.053401;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N49;132;0.0776;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N6;124;0.053754;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N47;53;0.019736;aaltafuc;4;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N22;68;0.013193;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_8;27;5.056951;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_ra;6;0.006821;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N37;37;0.007572;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.5/L60/P0.5N2L60_6.negated;1;0.000526;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N41;93;0.012686;aaltafuc;7;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_8;20;2.251959;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_mf;6;0.007782;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_14;39;36.945375;aaltafuc;27;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N29;114;0.028667;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_8;27;0.032235;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_7;29;0.007531;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_2;15;0.005246;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_2_1;5;0.001208;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N3;113;0.016846;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N3;57;0.015887;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_3;17;0.074482;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N44;66;0.019181;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N8;133;0.047093;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N7;148;0.027679;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N50;92;0.021087;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_6;25;0.012444;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N31;130;0.023386;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N7;108;0.032643;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N47;133;0.036115;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_3;14;0.005003;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/10/N14;16;0.002556;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N8;76;0.013128;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N36;120;0.02423;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N25;129;0.06299;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N10;102;0.032253;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N12;106;0.019356;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N17;142;0.047037;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N11;82;0.013825;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.3/L100/P0.333333333333333N2L100_5.negated;1;0.000734;aaltafuc;1;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N15;102;0.017171;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N46;127;0.07149;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N31;102;0.019857;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N31;51;0.016846;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_17;28;10.059007;aaltafuc;25;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N35;125;0.019823;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N24;85;0.025289;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N40;131;0.023688;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N24;137;0.030173;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec7.negated;1;0.042593;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_s1;6;0.005749;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_mh;6;0.00635;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N2;111;0.016015;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N47;69;0.015284;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_d;6;0.006085;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N5;86;0.019205;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N3;129;0.040861;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N14;139;0.103898;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.7/L80/P0.7N2L80_7.negated;1;0.000816;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_18;351;0.506485;aaltafuc;32;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_4;110;0.063453;aaltafuc;27;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N37;129;0.035197;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N4;132;0.032861;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N5;132;0.032122;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec18.negated;1;0.117514;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_18;47;0.073239;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N18;144;0.434358;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N10;123;0.017072;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N5;27;0.00377;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_10;23;0.019527;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_9;176;1.614383;aaltafuc;39;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N10;133;0.020168;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N1;123;0.041938;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N22;131;0.288811;aaltafuc;32;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N45;139;0.042112;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_3;17;0.005433;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula70;72;0.008238;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec12.negated;1;0.044868;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N49;77;0.016085;aaltafuc;9;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N27;133;0.025482;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N15;125;0.021048;aaltafuc;9;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_F_mhandra;6;0.006864;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N22;128;0.030901;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_15;314;92.571336;aaltafuc;64;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N1;134;0.02527;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_mh;6;0.007436;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N24;135;0.023653;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_11;33;1.132946;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N16;130;0.043407;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N26;37;0.014536;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N5;69;0.010221;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N22;125;0.141484;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n5/P0.5/L40/P0.5N5L40_7.negated;1;0.00054;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N8;138;0.022462;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N3;127;0.046698;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_15;28;0.028819;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N33;111;0.017624;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N23;126;0.037372;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N38;129;0.161127;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N3;128;0.051633;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.5/L10/P0.5N3L10_10;1;0.0;ltlfuc_bdd;1;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N1;94;0.022377;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N43;138;0.049249;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N14;92;0.016402;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_15;299;0.362799;aaltafuc;27;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N34;129;0.017638;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N50;131;0.07094;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N39;127;0.020819;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N7;126;0.081803;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_17;31;0.432022;aaltafuc;28;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N33;135;0.059458;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_12;37;1.116298;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N14;130;0.019475;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N21;120;0.100732;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N38;138;0.034296;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N44;127;0.019487;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec16.negated;1;0.143498;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_11;35;0.057336;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/10/N7;16;0.003341;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N29;136;0.056813;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N14;126;0.041002;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N18;62;0.010828;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N13;71;0.020368;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N35;154;0.063169;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N7;134;0.040641;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_8;165;0.195802;aaltafuc;46;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.3/L80/P0.333333333333333N2L80_3;1;0.000707;aaltafuc;1;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N49;95;0.029287;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N26;61;0.049287;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula500;502;0.120576;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N22;129;0.042653;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N12;126;0.026565;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_16;332;22.659621;aaltafuc;56;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_18;50;0.065954;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N21;132;0.059551;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N47;133;0.058107;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N34;130;0.03085;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N38;122;0.025921;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N7;130;0.02992;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_6;24;0.464259;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N16;122;0.028424;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N1;134;0.022685;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N26;129;0.048572;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N27;131;0.029816;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N12;141;0.042464;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N35;126;0.045993;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N6;40;0.007095;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N30;127;0.075078;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N10;135;0.031656;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N33;127;0.022064;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N3;129;0.034533;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N6;105;0.017025;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N35;73;0.012863;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula2;2;0.0;ltlfuc_bdd;2;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula60;62;0.007169;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N41;125;0.0193;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N31;130;0.026602;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N36;23;0.005356;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_6;18;0.209022;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N44;84;0.01755;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N2;126;0.026086;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N19;106;0.032581;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N4;137;0.033707;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N47;128;0.025027;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N34;87;0.012262;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N5;133;0.021919;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N40;99;0.017144;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N47;134;0.035502;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N6;68;0.030068;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N28;133;0.035829;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N33;26;0.004306;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N18;36;0.006668;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N6;129;0.035168;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N19;60;0.010829;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N38;129;0.032546;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N44;133;0.03705;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N24;132;0.06619;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N40;43;0.007881;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_17;374;0.556959;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N40;139;0.04354;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N9;119;0.04943;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N3;38;0.005975;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N28;54;0.007561;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_5;16;0.007925;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N29;128;0.041283;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N35;122;0.024863;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N48;136;0.034868;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N1;147;0.157452;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N35;140;0.026364;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N44;111;0.019291;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N5;135;0.023049;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N34;128;0.026537;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_ra;6;0.006262;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.5/L70/P0.5N2L70_1.negated;1;0.000691;aaltafuc;1;ltlfuc_sat
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_6;23;0.010942;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N25;92;0.01238;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N37;52;0.007839;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_12;35;0.045596;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N48;55;0.036293;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N28;133;0.094673;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N24;71;0.016036;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_13;39;16.01738;aaltafuc;28;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.5/L80/P0.5N3L80_7;4;0.001162;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_6;145;0.100127;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N17;55;0.014475;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N15;48;0.009985;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N29;132;0.058168;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N43;121;0.094041;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula9;11;0.0;ltlfuc_bdd;2;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_5;16;0.044663;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n4/P0.3/L70/P0.333333333333333N4L70_10.negated;1;0.000402;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula800;802;0.289745;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_3;81;0.030483;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_14;282;0.321352;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N37;102;0.050395;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/10/N33;13;0.001992;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N31;135;0.032538;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N38;135;1.438689;aaltafuc;23;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N30;117;0.018454;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N30;136;0.977531;aaltafuc;35;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_18;32;0.044129;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N4;123;0.653964;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N18;74;0.049971;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N46;68;0.011614;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N19;131;0.020005;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N2;78;0.024777;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_l;6;0.006018;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_15;305;0.192429;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N34;122;0.036302;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N18;135;0.020579;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N15;140;0.040281;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_15;28;0.329797;aaltafuc;25;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N42;135;0.033637;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N35;137;0.034172;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N7;128;0.017264;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N21;134;0.021945;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_5;21;0.017934;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula1000;1002;0.440226;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_g;6;0.007463;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N48;139;0.049646;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N41;50;0.014223;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N10;82;0.022769;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N19;134;0.078129;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_17;45;6.259105;aaltafuc;29;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N1;131;0.022575;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N49;133;0.065217;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_7;18;0.09811;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n4/P0.3/L10/P0.333333333333333N4L10_8;2;0.0;ltlfuc_sat;1;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N24;54;0.01031;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_re;6;0.006433;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N21;134;0.030637;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N8;61;0.012653;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N14;136;0.052502;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N29;132;0.046126;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N29;139;0.041208;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N32;125;0.043446;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N11;130;0.032282;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N20;70;0.047044;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N44;31;0.006555;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula80;82;0.00766;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N24;135;0.129926;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N39;139;0.023686;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N24;125;0.029554;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N10;132;0.062979;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N31;124;0.022983;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N12;126;0.047651;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n5/P0.5/L40/P0.5N5L40_6.negated;1;0.000512;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_10;31;198.505362;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N41;132;0.043556;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_16;29;0.248383;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_8;33;0.011736;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N13;97;0.016682;aaltafuc;8;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_2;14;0.007561;aaltafuc;1;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N22;136;0.021855;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N49;138;0.028232;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N39;137;0.053435;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N42;122;0.025243;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n4/P0.7/L100/P0.7N4L100_9;1;0.000409;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_2;9;0.001733;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_11;22;0.016312;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_9;197;0.097324;aaltafuc;25;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_12;37;0.041101;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec19.negated;1;0.19448;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N39;50;0.01168;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N14;132;0.058016;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N28;131;0.031824;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_11;35;4.976524;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N16;132;0.021935;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.3/L60/P0.333333333333333N2L60_3;1;0.000586;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N47;94;0.058335;aaltafuc;19;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N19;27;0.006218;aaltafuc;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_7;19;0.064639;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N36;121;0.023746;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N27;135;0.057134;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N34;71;0.018101;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N27;124;0.017589;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_4;98;0.041471;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N40;139;0.020724;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N29;129;0.02247;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_11;33;0.054964;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N49;107;0.019068;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N15;123;0.028295;aaltafuc;7;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_12;25;0.116802;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_5;22;0.181555;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N11;110;0.029555;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N8;129;0.029221;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N9;93;0.014669;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N23;104;0.020977;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N37;130;0.040241;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry3;9;0.06;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N50;136;0.021237;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N23;131;0.031269;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N44;141;0.053918;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_16;346;0.640441;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N12;134;0.023503;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N32;132;0.030052;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N26;89;0.017793;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_9;31;2.262706;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N31;127;0.020009;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N25;110;0.067024;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N34;76;0.017782;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N49;132;0.034848;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_18;29;7.441855;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N45;126;0.042633;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n5/P0.7/L60/P0.7N5L60_1;2;0.000967;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N42;126;0.046601;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N17;129;0.033211;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N16;116;0.015892;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N31;43;0.008696;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N40;127;0.059548;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N48;137;0.02233;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N18;143;0.077011;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N11;132;0.060451;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N3;127;0.018023;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N43;56;0.013924;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N45;122;0.01949;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N19;134;0.022272;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N48;128;0.029022;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec20.negated;1;0.243919;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N11;135;0.041098;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N49;51;0.012994;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula900;902;0.362161;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N47;128;0.394877;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_7;140;0.062461;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N32;132;0.190533;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_3;14;0.005038;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N45;65;0.03559;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N7;136;0.068641;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula7;9;0.001189;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.3/L70/P0.333333333333333N2L70_3;1;0.000655;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N44;98;0.018427;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N47;125;0.019448;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N42;137;0.022648;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N25;129;0.019893;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula8;10;0.0;ltlfuc_sat;2;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N15;57;0.016073;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_re;6;0.006067;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N3;126;0.028982;aaltafuc;9;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N21;127;0.3382;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N34;144;0.294863;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N39;135;0.10686;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N17;137;0.497936;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N36;133;0.029437;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N20;137;0.044922;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_d;6;0.007692;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N26;123;0.019743;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_20;461;1.376427;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula3;5;0.0;ltlfuc_sat;2;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N33;127;0.020272;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N12;135;0.0321;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_12;25;0.021919;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N6;92;0.013316;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N36;109;0.022541;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N4;63;0.016764;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N39;28;0.014191;aaltafuc;7;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_3;93;0.032184;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_6;130;0.053738;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N13;121;0.023578;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N38;77;0.010689;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N47;125;0.057524;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N13;131;0.019698;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N30;139;0.024816;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N36;137;0.020809;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N7;133;0.125384;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N33;136;0.028813;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_4;19;0.031546;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N27;45;0.009768;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N2;144;0.041777;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N20;130;0.0285;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N38;123;0.02028;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N46;124;0.020797;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N39;131;0.018135;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_16;45;21.416606;aaltafuc;30;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_g;6;0.005252;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N16;49;0.015603;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N40;61;0.010596;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N20;78;0.01554;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N9;106;0.016783;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N5;138;0.42933;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N23;127;0.036346;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N3;132;0.023792;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula5;7;0.0;ltlfuc_bdd;2;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec4.negated;1;0.0217;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N27;28;0.004136;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_30_29;61;0.529229;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_11;45;0.0132;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N47;131;0.020977;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N22;120;0.021314;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N47;128;0.037974;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N6;124;0.035384;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N16;126;0.024698;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N30;133;0.053782;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n4/P0.3/L90/P0.333333333333333N4L90_10;1;0.000697;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N40;124;0.020657;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_18;369;3.632856;aaltafuc;34;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N17;98;0.019591;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N32;118;0.266749;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N37;132;0.030996;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_7;18;0.01056;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N31;132;0.043364;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear5;6;0.12;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_5_4;11;0.004707;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_8_7;17;0.006714;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N48;90;0.017493;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N18;102;0.015329;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N45;136;0.022799;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_7;169;0.288903;aaltafuc;37;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N16;130;0.020617;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N32;121;0.015612;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N12;131;0.04712;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N19;131;0.05468;aaltafuc;8;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n4/P0.5/L20/P0.5N4L20_8;3;0.0;ltlfuc_sat;2;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N27;129;0.025342;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N22;134;0.020485;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N22;98;0.023218;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_6;17;0.009758;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N41;45;0.035222;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N30;72;0.033589;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N9;25;0.00319;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N14;36;0.00871;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N46;131;0.021516;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_12;23;0.531246;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N39;63;0.014453;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N11;134;0.03315;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N11;40;0.014654;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_15;43;0.042663;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_h1;6;0.006523;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula2;4;0.0;ltlfuc_sat;2;ltlfuc_sat
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec3.negated;1;0.012272;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N22;59;0.012154;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N47;43;0.032456;aaltafuc;4;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N29;75;0.013891;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N36;53;0.011316;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_11;226;0.333103;aaltafuc;23;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N45;116;0.022375;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter2;6;0.01;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N43;119;0.019032;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N31;132;0.027333;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_10;195;0.096111;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N33;132;0.032926;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N35;114;0.016517;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter4;8;0.07;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_8;19;0.185429;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N31;135;0.229775;aaltafuc;7;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_5;21;0.103618;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_18;29;0.030392;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N8;23;0.003516;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_9;29;0.419355;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.5/L100/P0.5N2L100_4;1;0.00079;aaltafuc;1;ltlfuc_sat
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_11;242;0.173805;aaltafuc;24;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N23;140;0.177717;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N30;53;0.01122;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N41;89;0.034707;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N36;138;0.279633;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N24;127;0.028545;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N14;68;0.020295;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N33;138;0.081151;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N21;87;0.013658;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N36;128;0.022151;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N15;81;0.01322;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_2;13;0.00268;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N41;64;0.014851;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N30;127;0.405604;aaltafuc;25;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N9;129;0.061667;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.7/L100/P0.7N3L100_5.negated;1;0.000781;aaltafuc;1;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N44;123;0.042265;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N42;53;0.009005;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N23;78;0.011215;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N40;79;0.013907;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec9.negated;1;0.04088;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_ra;6;0.006632;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N45;31;0.008873;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N13;130;0.022597;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula30;32;0.003283;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N38;127;0.033714;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N39;140;0.04212;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N50;132;0.042414;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_12;248;0.155074;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N23;128;0.987115;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N18;132;0.254133;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N42;99;0.018435;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N6;77;0.033997;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N7;127;0.027587;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N13;123;0.027669;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N20;125;0.02224;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N39;122;0.031564;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N29;54;0.012732;aaltafuc;4;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N18;51;0.011825;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N46;105;0.015417;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N46;73;0.01241;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N8;127;0.065091;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N45;146;0.036824;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N40;57;0.080283;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N23;38;0.006496;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N42;127;0.034768;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N15;133;0.052847;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N43;26;0.008072;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N38;135;0.041221;aaltafuc;8;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_2;14;0.005468;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N29;134;0.027369;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_10;21;0.015432;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N46;102;0.021686;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N12;111;0.016067;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N41;143;0.051142;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N8;120;0.03163;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N34;141;0.030796;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_10;31;0.037225;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N11;136;0.052059;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N15;144;0.037706;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_14;41;0.046507;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_11;215;0.113762;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N32;26;0.009118;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula10;12;0.001341;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula400;402;0.081151;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N11;50;0.012656;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N20;137;0.071376;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_6_5;13;0.007235;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N40;121;0.020067;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_8;20;0.014187;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N32;66;0.011239;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N7;116;0.019062;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N23;130;0.025081;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_3;17;0.008083;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N24;126;0.031016;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N15;127;0.018147;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N18;137;0.022131;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N32;134;0.100328;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N16;95;0.013663;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N49;40;0.005371;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N5;55;0.013065;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N34;25;0.005495;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N28;133;0.060841;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N16;136;0.03799;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_6;18;0.010793;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N31;92;0.013807;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N26;124;0.025431;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N32;127;0.027548;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N25;132;0.047643;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N3;66;0.015793;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula5;5;0.005178;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N44;125;0.020332;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N32;49;0.008566;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N35;31;0.004147;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_20;441;0.371179;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N27;137;0.071224;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_2;75;0.904864;aaltafuc;45;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_18;50;2.442664;aaltafuc;31;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N42;100;0.015845;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N15;130;0.0349;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N32;117;0.019315;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N38;138;0.022151;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_7;25;0.014065;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N23;130;0.798923;aaltafuc;31;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N34;134;0.023957;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N46;24;0.003924;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N17;125;0.050545;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N34;42;0.028892;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_15;43;1.734278;aaltafuc;29;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N28;103;0.017806;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N2;76;0.011392;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N2;103;0.03403;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N38;67;0.03419;aaltafuc;19;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N25;128;0.021115;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N34;134;0.042588;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N9;136;0.020285;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N39;127;0.018823;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N11;128;0.021235;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N5;135;0.069469;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N21;126;0.02279;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N28;130;0.064212;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N40;127;0.022471;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N44;60;0.031543;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N37;75;0.014732;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N13;62;0.021376;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N2;137;0.029442;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N17;123;0.037537;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_18;384;0.292639;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_l;6;0.004756;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N24;126;0.035285;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N45;104;0.016812;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N20;127;0.01968;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N42;129;0.058965;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N1;50;0.014847;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec15.negated;1;0.180676;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N30;66;0.012778;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N1;130;0.033018;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N44;126;0.019015;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N30;128;0.026269;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N8;137;0.065459;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N48;38;0.006741;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N2;135;0.019896;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N26;134;0.021505;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N6;49;0.020233;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N10;126;0.028392;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N34;128;0.045538;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N2;139;0.020231;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N14;129;0.030388;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N7;132;0.021329;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N34;52;0.014832;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_7;26;0.015673;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N16;131;0.063101;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N40;131;0.052637;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_13;24;0.020032;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N37;129;0.061749;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_g;6;0.006637;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N36;83;0.012679;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N15;41;0.005193;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/10/N45;13;0.00277;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N24;113;0.017482;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N49;126;0.01688;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_5;17;0.009687;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N22;37;0.004528;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula50;52;0.00588;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_13;278;0.609451;aaltafuc;41;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N21;124;0.022589;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N17;132;0.018013;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N26;128;0.029795;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N47;133;0.019651;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N5;95;0.069801;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N23;125;0.019547;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N8;123;0.028526;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N39;131;0.051115;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_5;114;0.05033;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N19;39;0.016252;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N9;133;0.051139;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N20;138;0.082605;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_15;41;0.098726;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N1;124;0.03831;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_3;96;0.060471;aaltafuc;30;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N24;132;0.065138;aaltafuc;25;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N24;38;0.014585;aaltafuc;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_1;57;0.1261;aaltafuc;37;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_8;157;0.070604;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_ff;6;0.005871;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec8.negated;1;0.033832;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N3;121;0.0299;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_12;49;0.011329;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N3;125;0.020767;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N23;125;0.019927;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N5;129;0.040113;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N28;135;0.047184;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N50;37;0.026745;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N44;141;0.034967;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_15;26;0.024932;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N18;132;0.021964;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N24;30;0.020371;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N10;122;0.038654;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_2;15;0.010721;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N41;133;0.040771;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_5;17;0.029145;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N10;117;0.022414;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N35;125;0.023411;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N50;138;1.315519;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N25;26;0.00402;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N23;45;0.009836;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N50;136;0.382577;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N25;128;0.031479;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N37;144;0.055565;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N50;63;0.010166;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_12;248;0.141348;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N4;76;0.020499;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N37;126;0.027636;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N33;130;0.037617;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N19;133;0.028399;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N13;40;0.010715;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/10/N3;15;0.002215;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N4;40;0.023997;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_10;205;0.113771;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_9;185;0.081329;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N46;134;1.210085;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N35;56;0.013952;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N49;128;0.02082;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N41;131;0.018654;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N4;118;0.038752;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N30;143;0.074589;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_10_9;21;0.013259;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_8;187;2.142724;aaltafuc;34;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N27;132;0.022219;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N42;131;0.033516;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N8;128;0.036286;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_17;45;0.057433;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_h1;6;0.008317;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.3/L50/P0.333333333333333N3L50_2;1;0.000522;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula4;6;0.0;ltlfuc_sat;2;ltlfuc_sat
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N7;78;0.042116;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.3/L50/P0.333333333333333N3L50_7;1;0.0;ltlfuc_bdd;1;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N35;130;0.038379;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N31;123;0.020217;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N46;139;0.052288;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N35;102;0.014565;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N20;136;0.090961;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N1;131;0.020213;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N7;149;0.039294;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N30;120;0.055764;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N16;36;0.012016;aaltafuc;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_mf;6;0.006032;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N4;61;0.016277;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N2;56;0.035566;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_13;258;0.213243;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N27;88;0.015948;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N12;86;0.055054;aaltafuc;16;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N50;82;0.028243;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N27;128;0.019872;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N49;135;0.13949;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N37;123;0.019985;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N1;134;0.022466;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N10;133;0.064121;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N6;123;0.040152;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N9;43;0.009893;aaltafuc;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N2;24;0.004155;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_2;70;0.02863;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_18;32;0.506874;aaltafuc;29;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N50;106;0.032075;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N18;127;0.01856;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N36;129;0.025904;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N26;116;0.019061;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N4;125;0.045803;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N17;141;0.021607;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N12;133;0.493238;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_14;41;0.27072;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N20;122;0.019915;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N48;136;1.708461;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_10;224;0.209298;aaltafuc;27;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N22;137;0.058298;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N38;136;0.043391;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N28;38;0.006536;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N45;70;0.02926;aaltafuc;9;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_18;402;0.918627;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N50;55;0.010405;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N26;132;0.680919;aaltafuc;26;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N6;122;0.019717;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_9;29;0.028428;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N20;93;0.014303;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N33;132;0.100056;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N26;137;0.044529;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N19;129;0.019859;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N23;131;0.020448;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_13;37;0.04815;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N8;131;0.019909;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear3;6;0.01;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N32;98;0.017163;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_s1;6;0.004577;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_h1;6;0.00719;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_11;22;0.580662;aaltafuc;19;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N14;120;0.027019;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N49;64;0.045754;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/10/N11;132;0.021139;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry4;10;0.14;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N16;108;0.014757;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_11;24;0.022179;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N10;97;0.013953;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N46;131;0.027012;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N41;118;0.016571;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N21;78;0.016639;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N47;133;0.065476;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N19;129;0.049597;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula8;8;0.044686;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N8;139;0.235127;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N50;128;0.033959;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N16;135;0.02606;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N15;88;0.014153;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N28;88;0.020611;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N25;143;0.023528;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_5;109;0.040759;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N39;80;0.014501;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_1;58;0.023383;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N36;130;0.029845;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula9;9;0.08;ltlfuc_bdd;9;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N11;125;0.021206;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N19;135;0.034009;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_11;24;0.156901;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N19;116;0.061332;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N19;77;0.013947;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N8;138;0.068577;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N39;132;0.032501;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N5;123;0.05111;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N18;133;0.064607;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.5/L30/P0.5N3L30_8.negated;1;0.00042;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N33;69;0.009586;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N38;104;0.018145;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N25;131;0.090889;aaltafuc;11;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_12;35;0.775472;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N41;130;0.064001;aaltafuc;6;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_FGn_re;6;0.005023;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N28;65;0.014327;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N2;129;0.054123;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_7;26;0.056468;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N7;64;0.02301;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N18;112;0.015854;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N49;127;0.03424;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N50;127;0.023197;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N4;104;0.021413;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N16;78;0.014036;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N36;136;0.037912;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N20;127;0.018366;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N8;58;0.015848;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N25;51;0.013184;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_5;22;0.020429;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N21;139;0.1751;aaltafuc;13;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N6;138;0.021896;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N2;132;0.043333;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N31;66;0.040089;aaltafuc;10;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N41;103;0.014954;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N38;119;0.018334;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_mh;6;0.009406;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N15;133;0.026866;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_9;37;0.015174;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N20;42;0.013328;aaltafuc;3;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N32;139;0.037605;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N35;88;0.012874;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N48;130;0.026444;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N2;135;0.024709;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_12;236;0.142223;aaltafuc;11;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N6;136;0.042081;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula20;22;0.002513;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N16;123;0.018916;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N6;143;0.037793;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula10;10;0.1;ltlfuc_bdd;10;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula200;202;0.028695;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N29;92;0.022623;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N27;140;0.084582;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_16;43;0.038154;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_c/spec_c_6;124;0.051999;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N33;95;0.014268;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N41;27;0.009789;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N28;114;0.026772;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N3;76;0.013764;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N1;84;0.021615;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_d;6;0.005063;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec5.negated;1;0.015974;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/100/N26;128;0.097189;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N25;130;0.028714;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_7;25;0.313846;aaltafuc;18;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N50;131;0.020351;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N31;81;0.016943;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_6;23;0.130335;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_13;24;1.092968;aaltafuc;21;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N28;122;0.029601;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N40;129;0.039117;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N22;109;0.018485;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N17;135;0.021001;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec1.negated;1;0.009444;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_l/lift_b_l_17;48;0.060008;aaltafuc;17;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N14;129;0.034164;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N21;133;0.025832;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N11;130;0.0686;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N41;127;0.046102;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_6;17;0.084056;aaltafuc;14;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N17;134;0.056429;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N20;111;0.017408;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N29;58;0.016501;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N28;129;0.021464;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N27;146;0.066545;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_3;17;0.211392;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/example/demo-v20.negated;1;0.001877;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N14;76;0.011234;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N45;131;0.070802;aaltafuc;8;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N22;145;0.041856;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_10;41;0.0096;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N43;82;0.045204;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift/lift_14;25;0.022161;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N24;133;0.056214;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_2;13;0.011478;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N8;35;0.005713;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N14;135;0.029025;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N47;81;0.017553;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N45;132;0.030232;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec17.negated;1;0.159326;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N26;137;0.493885;aaltafuc;15;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N42;37;0.008737;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N42;82;0.016832;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N19;134;0.028215;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N26;24;0.010861;aaltafuc;8;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_4;15;0.006517;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_GF_ra;6;0.007193;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O1formula/O1formula700;702;0.226973;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_l/lift_l_4;19;0.008506;aaltafuc;8;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N11;120;0.094567;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_16;27;3.261904;aaltafuc;24;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N32;37;0.005224;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N45;132;0.026517;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N9;128;0.128982;aaltafuc;9;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N33;39;0.006157;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_Gn_re;6;0.009593;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N41;136;0.164032;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_15;26;43.756009;aaltafuc;23;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N45;44;0.015457;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N25;39;0.005072;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f/lift_f_3;14;0.016652;aaltafuc;10;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/acacia/demo-v3/demo-v3_cl/demo-v3_cl_4;17;0.006215;aaltafuc;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N25;62;0.035727;aaltafuc;9;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/20/N3;124;0.023718;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N22;130;0.034054;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/70/N13;143;0.049147;aaltafuc;5;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/100/N4;132;0.02178;aaltafuc;5;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_9;22;4.276931;aaltafuc;20;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear4;6;0.05;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N30;128;0.0711;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b/lift_b_14;27;0.026371;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N47;100;0.022862;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/80/N14;106;0.017661;aaltafuc;3;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N48;136;0.04272;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N36;80;0.01215;aaltafuc;6;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N5;115;0.022151;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N37;62;0.014392;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/60/N36;121;0.097245;aaltafuc;8;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/forobots/forobotsr1f0_G_l;6;0.004715;aaltafuc;4;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/30/N41;132;0.022943;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/40/N6;139;0.029418;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N21;59;0.016267;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf/spec6.negated;1;0.025723;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_3;14;0.044466;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N34;119;0.020263;aaltafuc;5;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/50/N27;60;0.009784;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/90/N23;124;0.026068;aaltafuc;4;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n2/P0.5/L40/P0.5N2L40_8.negated;1;0.000823;aaltafuc;1;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/70/N19;101;0.473203;aaltafuc;22;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/formulas/n3/P0.3/L80/P0.333333333333333N3L80_5.negated;1;0.000765;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/80/N43;135;0.071353;aaltafuc;7;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/20/N11;25;0.003679;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_13;26;0.274458;aaltafuc;23;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N21;137;0.039538;aaltafuc;4;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/50/N22;136;0.035719;aaltafuc;7;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/30/N30;38;0.007077;aaltafuc;2;ltlfuc_bdd
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/40/N45;55;0.011395;aaltafuc;2;aaltafuc
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/V20/60/N22;69;0.01222;aaltafuc;3;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear5;8;0.12;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTLf-specific/benchmarks/benchmarks_ltlf/LTLfRandomConjunction/C100/90/N8;140;0.068384;aaltafuc;6;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f/lift_b_f_4;15;0.018317;aaltafuc;12;aaltafuc
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear15;8;9.67;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear12;6;3.6;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula40;40;103.38;ltlfuc_bdd;40;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear10;8;1.78;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry7;13;2.52;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula80;80;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula100;100;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear13;8;4.8;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_cl/spec_cl_5;133;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter14;18;33.77;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter8;12;2.5;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/phltl/phltl_50_49;101;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula30;30;12.88;ltlfuc_bdd;30;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter17;21;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry9;15;1.91;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry15;21;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula600;600;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter10;14;25.11;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula70;70;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula20;20;0.88;ltlfuc_bdd;20;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_b_f_l/lift_b_f_l_17;48;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter20;24;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear14;8;12.62;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter11;15;27.01;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear18;6;5.27;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter9;13;29.02;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula400;400;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula200;200;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear8;8;0.41;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear20;6;16.43;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter19;23;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter6;10;0.49;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear19;6;17.36;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter12;16;6.38;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula60;60;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_16;316;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula800;800;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear7;6;0.42;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula1000;1000;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula700;700;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula500;500;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear11;8;2.31;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear9;8;0.71;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter15;19;14.94;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear16;6;12.21;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter18;22;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear6;6;0.24;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry16;22;29.36;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry12;18;5.03;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear11;6;2.8;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry14;20;8.52;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear19;8;24.43;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_14;295;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula300;300;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear10;6;0.85;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/amba/amba_c/spec_c_8;179;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear14;6;3.53;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear12;8;5.59;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula900;900;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter7;11;2.33;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry20;26;114.28;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula90;90;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry10;16;6.88;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry11;17;37.5;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear15;6;3.66;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/schuppan/O2formula/O2formula50;50;80.81;ltlfuc_bdd;50;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear6;8;0.2;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter13;17;9.96;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear8;6;0.79;ltlfuc_bdd;4;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear20;8;13.05;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counter/counter16;20;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry18;24;41.47;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry17;23;63.6;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry8;14;9.94;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/alaska/lift/lift_f_l/lift_f_l_15;41;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear13;6;5.54;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterLinear/counterLinear9;6;1.04;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry13;19;13.14;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear7;8;0.27;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear18;8;18.66;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry6;12;0.75;ltlfuc_bdd;2;trppp
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear16;8;13.45;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/anzu/genbuf/genbuf_cl/spec_cl_15;320;10000;;None;
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarry/counterCarry19;25;55.03;ltlfuc_bdd;3;ltlfuc_bdd
+/AIJ-artifact/LTL-as-LTLf/benchmarks/benchmarks/rozier/counter/counterCarryLinear/counterCarryLinear17;8;32.88;ltlfuc_bdd;3;ltlfuc_bdd
diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results-virtual_best_info.xlsx b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info.xlsx
similarity index 100%
rename from etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results-virtual_best_info.xlsx
rename to etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info.xlsx
diff --git a/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info_per-category.csv b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info_per-category.csv
new file mode 100644
index 000000000..6f52ae6fd
--- /dev/null
+++ b/etc/AIJ-SAT-explorer/AIJ-analysis-plots/AIJ-results_virtual-best_info_per-category.csv
@@ -0,0 +1,27 @@
+category;total;min-clauses;max-clauses;avg-clauses;AALTAF@min-UC;AALTAF@min-UC[%];AALTAF@min-timing;AALTAF@min-timing%;TRP++@min-UC;TRP++@min-UC[%];TRP++@min-timing;TRP++@min-timing%;NuSMV-S@min-UC;NuSMV-S@min-UC[%];NuSMV-S@min-timing;NuSMV-S@min-timing%;NuSMV-B@min-UC;NuSMV-B@min-UC[%];NuSMV-B@min-timing;NuSMV-B@min-timing%;None@min-UC;None@min-UC[%];None@min-timing;None@min-timing%
+;1377;1;1002;97.63;690;50.11;1260;91.50;543;39.43;0;0.00;12;0.87;8;0.58;104;7.55;81;5.88;28;2.03;28;2.03
+LTL-as-LTLf/acacia/demo-v3/demo-v3:cl;11;9;49;29.00;7;63.64;11;100.00;4;36.36;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift;17;13;29;21.00;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:b;17;12;32;22.47;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:b:f;17;12;32;22.47;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:b:f:l;17;14;50;32.47;15;88.24;16;94.12;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
+LTL-as-LTLf/alaska/lift/lift:b:l;17;14;50;32.47;14;82.35;17;100.00;3;17.65;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:f;17;13;29;21.00;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/alaska/lift/lift:f:l;17;15;47;31.00;15;88.24;16;94.12;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
+LTL-as-LTLf/alaska/lift/lift:l;17;15;47;31.00;16;94.12;17;100.00;1;5.88;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/anzu/amba/amba:c;17;75;351;213.47;15;88.24;15;88.24;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;2;11.76;2;11.76
+LTL-as-LTLf/anzu/amba/amba:cl;17;77;369;223.47;16;94.12;16;94.12;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;5.88;1;5.88
+LTL-as-LTLf/anzu/genbuf/genbuf;20;1;1;1.00;20;100.00;20;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/anzu/genbuf/genbuf:c;20;57;441;221.00;20;100.00;20;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/anzu/genbuf/genbuf:cl;20;58;461;231.50;18;90.00;18;90.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;2;10.00;2;10.00
+LTL-as-LTLf/forobots;38;6;6;6.00;38;100.00;38;100.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTL-as-LTLf/rozier/counter/counter;19;6;24;15.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;14;73.68;14;73.68;5;26.32;5;26.32
+LTL-as-LTLf/rozier/counter/counterCarry;19;8;26;17.00;0;0.00;0;0.00;6;31.58;0;0.00;0;0.00;0;0.00;12;63.16;18;94.74;1;5.26;1;5.26
+LTL-as-LTLf/rozier/counter/counterCarryLinear;19;8;8;8.00;0;0.00;0;0.00;6;31.58;0;0.00;0;0.00;0;0.00;13;68.42;19;100.00;0;0.00;0;0.00
+LTL-as-LTLf/rozier/counter/counterLinear;18;6;6;6.00;0;0.00;1;5.56;0;0.00;0;0.00;0;0.00;0;0.00;18;100.00;17;94.44;0;0.00;0;0.00
+LTL-as-LTLf/rozier/formulas/n;30;1;4;1.33;12;40.00;24;80.00;0;0.00;0;0.00;8;26.67;4;13.33;10;33.33;2;6.67;0;0.00;0;0.00
+LTL-as-LTLf/schuppan/O1formula;27;4;1002;224.00;20;74.07;20;74.07;0;0.00;0;0.00;4;14.81;4;14.81;3;11.11;3;11.11;0;0.00;0;0.00
+LTL-as-LTLf/schuppan/O2formula;27;2;1000;222.00;5;18.52;5;18.52;0;0.00;0;0.00;0;0.00;0;0.00;8;29.63;8;29.63;14;51.85;14;51.85
+LTL-as-LTLf/schuppan/phltl;13;5;101;30.85;12;92.31;12;92.31;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;1;7.69;1;7.69
+LTLf-specific/benchmarks:ltlf/LTLfRandomConjunction/C100;500;118;154;131.50;255;51.00;500;100.00;245;49.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00;0;0.00
+LTLf-specific/benchmarks:ltlf/LTLfRandomConjunction/V20;425;13;146;81.54;127;29.88;425;100.00;272;64.00;0;0.00;0;0.00;0;0.00;26;6.12;0;0.00;0;0.00;0;0.00
diff --git a/etc/AIJ-SAT-explorer/run-AIJ-results-analysis.py b/etc/AIJ-SAT-explorer/run-AIJ-results-analysis.py
index afdaae12b..88b7711a2 100644
--- a/etc/AIJ-SAT-explorer/run-AIJ-results-analysis.py
+++ b/etc/AIJ-SAT-explorer/run-AIJ-results-analysis.py
@@ -301,7 +301,7 @@ def compute_stats(results={}, tool='aaltafuc',
     return (results, pre_parsing_solutions, timeouts, unknowns)
 
 
-def compute_virtual_best(results, vbest_tool_name=V_BEST_TOOL.tool_codename, csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results-virtual_best_info.csv'):
+def compute_virtual_best(results, vbest_tool_name=V_BEST_TOOL.tool_codename, csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results_virtual-best_info.csv'):
     csv_f = open(csv_outfile, 'w')
     csv_f.write('Test;Clauses;BestTime;BestPerformer;MinUnSATCore;MinUnSATFinder\n')
     absolute_minimum_timing = TIMEOUT
@@ -496,11 +496,13 @@ def create_csv(results, output_file):
         csv_f.write("\n")
 
 
-def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbest_tool_name=V_BEST_TOOL.tool_codename, criteria=['best_performer', 'min_unsat_core_finder'], csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results-virtual_best_info.csv'):
+def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbest_tool_name=V_BEST_TOOL.tool_codename, criteria=['best_performer', 'min_unsat_core_finder'], csv_outfile=ANALYSIS_PLOTS_DIR+'/AIJ-results_virtual-best_info_per-category.csv'):
     all_tools = [x for x in TOOLS.keys()] + [NO_TOOL.tool_codename]  # Including the “None” tool
+    min_cl = max_cl = avg_cl = 0
 
     test_filename_prefixes = [''] + test_filename_prefixes  # Including the “catch-all” category
     total_tests_counter = {x: 0 for x in test_filename_prefixes}
+    clauses_stats = {x: {'min': 0, 'max': 0, 'avg': 0} for x in test_filename_prefixes}
 
     tool_best_counters = {x: {} for x in test_filename_prefixes}
     for test_filename_prefix in test_filename_prefixes:
@@ -510,17 +512,22 @@ def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbe
                 tool_best_counters[test_filename_prefix][tool][criterion] = 0
                 tool_best_counters[test_filename_prefix][tool][criterion] = 0
 
+    retrieve_stats = True
     for criterion in criteria:
         for test_filename_prefix in test_filename_prefixes:  # Computational complexity is definitely improvable. I know
-            (best_performances_per_tool, total) = \
-                get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
+            (best_performances_per_tool, total, min_cl, max_cl, avg_cl) = \
+                get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name, retrieve_stats)
             for tool in best_performances_per_tool:  # Write
                 tool_best_counters[test_filename_prefix][tool][criterion] = best_performances_per_tool[tool]
             total_tests_counter[test_filename_prefix] = total
-
+            if retrieve_stats:
+                clauses_stats[test_filename_prefix]['min'] = min_cl
+                clauses_stats[test_filename_prefix]['max'] = max_cl
+                clauses_stats[test_filename_prefix]['avg'] = avg_cl
+        retrieve_stats = False
 
     csv_f = open(csv_outfile, 'w')
-    csv_f.write("category;total")
+    csv_f.write("category;total;min-clauses;max-clauses;avg-clauses")
     # Write the header
     for tool in all_tools:
         tool_label = NO_TOOL.tool_label if tool not in TOOLS else TOOLS[tool].tool_label
@@ -533,6 +540,12 @@ def create_csv_best_per_category(results, test_filename_prefixes=CATEGORIES, vbe
         csv_f.write(build_category_label_from_path_prefix(test_filename_prefix))
         csv_f.write(';')
         csv_f.write(str(total_tests_counter[test_filename_prefix]))
+        csv_f.write(';')
+        csv_f.write(str(clauses_stats[test_filename_prefix]['min']))
+        csv_f.write(';')
+        csv_f.write(str(clauses_stats[test_filename_prefix]['max']))
+        csv_f.write(';')
+        csv_f.write("%0.2f" % clauses_stats[test_filename_prefix]['avg'])
         for tool in all_tools:
             csv_f.write(";" + str(tool_best_counters[test_filename_prefix][tool]['min_unsat_core_finder']) +
                         ";%0.2f" % (tool_best_counters[test_filename_prefix][tool]['min_unsat_core_finder'] / total_tests_counter[test_filename_prefix] * 100.0) +
@@ -872,7 +885,7 @@ def plot_unsat_core_cardinality_scatter(figure_seq_num, results, tool_0, tool_1,
 def plot_best_piechart(figure_seq_num, results, best_piechart_filename_template, test_filename_prefix='',
                        vbest_tool_name=V_BEST_TOOL.tool_codename, criterion='best_performer'):
     plt.figure(figure_seq_num)
-    (best_performances_per_tool, total) = get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
+    (best_performances_per_tool, total, _, _, _) = get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
 
     labels = [TOOLS[tool].tool_label for tool in best_performances_per_tool.keys() if tool != NO_TOOL.tool_codename]
     labels.append(NO_TOOL.tool_label)
@@ -893,9 +906,12 @@ def show_total_in_place_of_percentage(p):
     plt.close(figure_seq_num)
 
 
-def get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name):
+def get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name, retrieve_stats=False):
     best_performances_per_tool = {}
     total = 0
+    min_cl = -1
+    max_cl = avg_cl = tot_clauses = 0
+
     for test in results.keys():
         if test.startswith(test_filename_prefix):
             total += 1
@@ -906,7 +922,15 @@ def get_best_performers(criterion, results, test_filename_prefix, vbest_tool_nam
                 best_performances_per_tool[best_tool] = 1
             else:
                 best_performances_per_tool[best_tool] += 1
-    return (best_performances_per_tool, total)
+            if retrieve_stats:
+                clauses = results[test][vbest_tool_name]['clauses']
+                tot_clauses += clauses
+                if min_cl < 0 or clauses < min_cl:
+                    min_cl = clauses
+                if max_cl < clauses:
+                    max_cl = clauses
+    avg_cl = tot_clauses * 1.0 / total
+    return (best_performances_per_tool, total, min_cl, max_cl, avg_cl)
 
 
 def plot_best_stacked_bar_per_category(figure_seq_num, results, best_stacked_bar_per_category_filename_template, test_filename_prefixes=[''],
@@ -918,7 +942,7 @@ def plot_best_stacked_bar_per_category(figure_seq_num, results, best_stacked_bar
     tool_best_counters[NO_TOOL.tool_codename] = []
     i = 0
     for test_filename_prefix in test_filename_prefixes:  # Computational complexity is definitely improvable. I know
-        (best_performances_per_tool, total) = \
+        (best_performances_per_tool, total, _, _, _) = \
             get_best_performers(criterion, results, test_filename_prefix, vbest_tool_name)
         for tool in tool_best_counters:  # Init
             tool_best_counters[tool].append(0)