From b963650558b7cea08beb6b93f849ee96904b604b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Da=CC=88hne?= <janis.daehne@informatik.uni-halle.de>
Date: Mon, 16 Oct 2023 17:25:26 +0200
Subject: [PATCH] - added imac table backup
---
backupDb/config_imac_janis.sql | 148 +++++++++++++++++++++++++++++++++
1 file changed, 148 insertions(+)
create mode 100644 backupDb/config_imac_janis.sql
diff --git a/backupDb/config_imac_janis.sql b/backupDb/config_imac_janis.sql
new file mode 100644
index 0000000..63c1bab
--- /dev/null
+++ b/backupDb/config_imac_janis.sql
@@ -0,0 +1,148 @@
+-- phpMyAdmin SQL Dump
+-- version 4.9.3
+-- https://www.phpmyadmin.net/
+--
+-- Host: localhost:8889
+-- Erstellungszeit: 16. Okt 2023 um 15:23
+-- Server-Version: 5.7.26
+-- PHP-Version: 7.4.2
+
+SET SQL_MODE = "NO_AUTO_VALUE_ON_ZERO";
+SET time_zone = "+00:00";
+
+--
+-- Datenbank: `yapextestdb`
+--
+
+-- --------------------------------------------------------
+
+--
+-- Tabellenstruktur für Tabelle `config`
+--
+
+CREATE TABLE `config` (
+ `id` int(11) NOT NULL,
+ `workingDirFullPath` text NOT NULL,
+ `hardTimeoutInMs` int(11) NOT NULL,
+ `hardCompileTimeoutInMs` int(11) NOT NULL,
+ `hardMemoryLimitInKb` int(11) NOT NULL,
+ `hardDiskSpaceLimitInKb` int(11) NOT NULL,
+ `maxNumberOfTestsWithOneRequest` int(11) NOT NULL,
+ `runner` text NOT NULL,
+ `showTestRunnerDebugOutput` tinyint(1) NOT NULL DEFAULT '0',
+ `insertTraceLogs` tinyint(1) NOT NULL DEFAULT '1',
+ `environmentVars` text
+) ENGINE=InnoDB DEFAULT CHARSET=latin1;
+
+--
+-- Daten für Tabelle `config`
+--
+
+INSERT INTO `config` (`id`, `workingDirFullPath`, `hardTimeoutInMs`, `hardCompileTimeoutInMs`, `hardMemoryLimitInKb`, `hardDiskSpaceLimitInKb`, `maxNumberOfTestsWithOneRequest`, `runner`, `showTestRunnerDebugOutput`, `insertTraceLogs`, `environmentVars`) VALUES
+ (1, '/Users/janis/Documents/Test/', 4000, 2000, 2000, 2000, 15, '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main', 1, 1, NULL);
+
+-- --------------------------------------------------------
+
+--
+-- Tabellenstruktur für Tabelle `plangs`
+--
+
+CREATE TABLE `plangs` (
+ `internalName` varchar(100) NOT NULL,
+ `compile` text NOT NULL,
+ `exec` text NOT NULL,
+ `extensions` text NOT NULL
+) ENGINE=InnoDB DEFAULT CHARSET=latin1;
+
+--
+-- Daten für Tabelle `plangs`
+--
+
+INSERT INTO `plangs` (`internalName`, `compile`, `exec`, `extensions`) VALUES
+ ('adt_bewerter', 'dotnet \"/Users/janis/uni/projects/adt-bewertung/bin/Debug/netcoreapp3.1/BaumtransformationBewerter.dll\" \"#5\" \"false\" \"#10\"', 'dotnet \"/Users/janis/uni/projects/adt-bewertung/bin/Debug/netcoreapp3.1/BaumtransformationBewerter.dll\" \"#5\" \"#11\" \"#10\"', '[\"txt\"]'),
+ ('adt_induction', '', 'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" ', '[\"adt\", \"proof\", \"task\"]'),
+ ('java', 'javac -encoding UTF8 \"#5\"', 'java -Dfile.encoding=UTF8 -cp \"#1\" \"#2\"', '[\"java\"]'),
+ ('python', '\"python\" \"-m\" \"py_compile\" \"#5\"', '\"python\" \"#5\"', '[\"py\"]');
+
+-- --------------------------------------------------------
+
+--
+-- Tabellenstruktur für Tabelle `traceLog`
+--
+
+CREATE TABLE `traceLog` (
+ `id` int(11) NOT NULL,
+ `dateTime` datetime NOT NULL DEFAULT CURRENT_TIMESTAMP,
+ `traceString` text NOT NULL,
+ `processString` text NOT NULL,
+ `sourceCode` mediumtext NOT NULL
+) ENGINE=InnoDB DEFAULT CHARSET=utf8;
+
+--
+-- Daten für Tabelle `traceLog`
+--
+
+INSERT INTO `traceLog` (`id`, `dateTime`, `traceString`, `processString`, `sourceCode`) VALUES
+ (106, '2023-06-15 16:21:47', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686838907_0-61719800-1_2-04FE9D40-CF35-41D3-BC6D-7EA6E85DD624\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_2\' \'1\' \'-checkSyntaxOnly\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(107, '2023-06-15 16:22:27', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4006_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686838947_0-43564400-1_3-43B782EE-60BA-433D-895A-B562FE4847AD\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_3\' \'1\' \'\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(108, '2023-06-15 16:24:31', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686839071_0-00110700-1_4-3000F551-0287-4325-9D5A-F89564B8F875\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_4\' \'1\' \'-checkSyntaxOnly\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(109, '2023-06-15 16:24:58', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686839098_0-32775900-1_5-07225248-0EEE-4E64-9377-CA2AF77B0A12\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_5\' \'1\' \'-checkSyntaxOnly\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(110, '2023-06-15 16:28:20', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686839300_0-96462400-1_6-024B3F32-B82B-46FE-B669-AA2AF3420605\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_6\' \'1\' \'-checkSyntaxOnly\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(111, '2023-06-15 16:32:05', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686839525_0-95906400-1_7-1805D23C-9401-4FFF-9339-C979977C55F3\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_7\' \'1\' \'-checkSyntaxOnly\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(112, '2023-06-15 16:32:22', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'blackBoxTest\' \'/Users/janis/Documents/Test/work/1686839542_0-03519000-1_8-C2F06A15-D554-4C92-80BA-B391AB092F77\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'2000\' \'1000\' \'1000\' \'adt,proof,task\' \'true\' \'1_8\' \'1\' \'-checkSyntaxOnly\' \'160100\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(113, '2023-06-15 16:35:39', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4004_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839739_0-52795600-1_9-AC4D5FEB-8F3C-4BA6-979A-F8E91AD76E8B\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'1_9\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(114, '2023-06-15 16:35:42', 'runNormalOrSubmitTest_executingUser:1_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_tests_4006_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839742_0-59542000-1_10-705A8611-57A1-478F-AD26-9BF463B9474F\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'1_10\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(115, '2023-06-15 16:37:06', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839826_0-36118900-1_11-3CFF0FA9-A046-4ACD-89F8-170C050E37E3\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'1_11\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(116, '2023-06-15 16:37:06', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839826_0-36118900-1_11-3CFF0FA9-A046-4ACD-89F8-170C050E37E3\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'1_11\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(117, '2023-06-15 16:37:07', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839827_0-13739600-1_12-FB7615F5-C1EC-423D-92CE-707AA50441ED\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'1_12\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(118, '2023-06-15 16:38:54', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839934_0-45737200-2_13-DB6D1785-CD0D-4519-A07C-D07173360B95\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'2_13\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(119, '2023-06-15 16:38:54', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839934_0-45737200-2_13-DB6D1785-CD0D-4519-A07C-D07173360B95\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'2_13\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(120, '2023-06-15 16:38:55', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839935_0-32902000-2_14-C3A6B7FA-ADB1-4951-BBFD-2BC847670278\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'2_14\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(121, '2023-06-15 16:39:13', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839953_0-04252600-3_15-E51C06EC-75B4-415D-AF6A-95932514F139\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'3_15\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(122, '2023-06-15 16:39:13', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839953_0-04252600-3_15-E51C06EC-75B4-415D-AF6A-95932514F139\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'3_15\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(123, '2023-06-15 16:39:13', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686839953_0-94371700-3_16-83C537DD-E668-4638-B0F6-1069B9D01FA3\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'3_16\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(124, '2023-06-15 16:40:51', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840051_0-56783700-4_17-179929C0-4EE9-4F92-8AD9-64BB398EDCB1\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'4_17\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(125, '2023-06-15 16:40:51', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840051_0-56783700-4_17-179929C0-4EE9-4F92-8AD9-64BB398EDCB1\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'4_17\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(126, '2023-06-15 16:40:52', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840052_0-48317100-4_18-0D54E3F8-6643-417C-90CF-F1C62CE05902\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'4_18\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(127, '2023-06-15 16:42:21', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840141_0-80384600-5_19-90BE613D-9BC2-4589-8075-9EA30F4888A5\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'5_19\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(128, '2023-06-15 16:42:22', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840141_0-80384600-5_19-90BE613D-9BC2-4589-8075-9EA30F4888A5\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'5_19\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(129, '2023-06-15 16:44:09', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840249_0-22694100-5_20-C5E677E6-0828-492B-9BEC-A0C53130F7C0\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'5_20\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(130, '2023-06-15 16:45:33', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840333_0-67433600-6_21-A0A759B4-CD6C-44D8-85A8-A234972B1F41\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'6_21\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(131, '2023-06-15 16:45:34', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840333_0-67433600-6_21-A0A759B4-CD6C-44D8-85A8-A234972B1F41\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'6_21\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n');
+INSERT INTO `traceLog` (`id`, `dateTime`, `traceString`, `processString`, `sourceCode`) VALUES
+(132, '2023-06-15 16:45:57', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840357_0-53606700-6_22-688077AB-A7F7-4DC5-9CAF-87C480BDC466\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'6_22\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(133, '2023-06-15 16:47:30', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840450_0-28876500-1_1-EF5F5011-FD4D-4165-A8E0-5173B09A877C\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'-checkSyntaxOnly\' \'1\' \'1\' \'1_1\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(134, '2023-06-15 16:47:30', 'SubmissionAssessmentWorker_normalTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_normalTests:tests_4004_2', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840450_0-28876500-1_1-EF5F5011-FD4D-4165-A8E0-5173B09A877C\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'1_1\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n'),
+(135, '2023-06-15 16:47:31', 'SubmissionAssessmentWorker_submitTests_solution::userId:1_releaseId:1556_plangId:6_mainFileId:166193_submitTests:tests_4005_1', '\"/usr/local/opt/openjdk/bin/java\" -Dfile.encoding=UTF8 -cp \"/Users/janis/uni/projects/yapex/DefaultTestRunnerFullThreaded/out/production/DefaultTestRunnerFullThreaded\" Main \'externalCheckerStructuralInductionTest\' \'/Users/janis/Documents/Test/work/1686840451_0-51074500-1_2-4D29D9A8-9755-48A6-9581-8A36672AAF4F\' \'term.adt\' \'\' \'dotnet \"/Users/janis/uni/projects/adt_bewerter-struktureller-induktion/BaumtransformationBewerter/bin/Debug/netcoreapp3.1/BaumtransformationBewerterYapex.dll\" \"#5\" \"#9\" \"#49\" \' \'1000\' \'1000\' \'1000\' \'adt,proof,task\' \'160100\' \'\' \'1\' \'1\' \'1_2\'', '---term.adt---\nname Rollenspiel\nsorts P,L\nconstructors player: P\n attack: P -> P\n spell : P -> P\n one: L\n up: L -> L\noperations fusion: P >< P -> P\n level: P -> L\n both: L >< L -> L\nvars p : P, q : P, x : L, y : L\naxioms F0: fusion(p,player) = p\n F1: fusion(p,attack(q)) = attack(fusion(p,q))\n F2 : fusion(p,spell(q)) = spell(fusion(p,q))\n L0 : level(player) = one\n L1 : level(attack(p)) = up(level(p))\n L2 : level(spell(p)) = up(up(level(p)))\n B0 : both(x,one) = x\n B1 : both(x,up(y)) = up(both(x,y))\n\n\n---term.task---\ntask forall q:P : both(level(q),level(attack(player))) = up(level(q)) maxpt 8 minsteps 4 maxsteps 100\n\n---term.proof---\nproof\nboth(level(q),level(attack(player)))\n {L1, lr, level(attack(player)), [player/p]}\n= both(level(q),up(level(player)))\n {L0, lr, level(player), []}\n= both(level(q),up(one))\n {B1, lr, both(level(q),up(one)), [level(q)/x,one/y]}\n= up(both(level(q),one))\n {B0, lr, both(level(q),one), [level(q)/x]}\n= up(level(q))\n\n');
+
+--
+-- Indizes der exportierten Tabellen
+--
+
+--
+-- Indizes für die Tabelle `config`
+--
+ALTER TABLE `config`
+ ADD PRIMARY KEY (`id`);
+
+--
+-- Indizes für die Tabelle `plangs`
+--
+ALTER TABLE `plangs`
+ ADD PRIMARY KEY (`internalName`);
+
+--
+-- Indizes für die Tabelle `traceLog`
+--
+ALTER TABLE `traceLog`
+ ADD PRIMARY KEY (`id`);
+
+--
+-- AUTO_INCREMENT für exportierte Tabellen
+--
+
+--
+-- AUTO_INCREMENT für Tabelle `traceLog`
+--
+ALTER TABLE `traceLog`
+ MODIFY `id` int(11) NOT NULL AUTO_INCREMENT, AUTO_INCREMENT=136;
--
GitLab