Skip to content
Snippets Groups Projects
Commit b9636505 authored by Janis Daniel Dähne's avatar Janis Daniel Dähne
Browse files

- added imac table backup

parent 3cffa868
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
backupDb/config_imac_janis.sql 0 → 100644
+ 148
− 0
View file @ b9636505
-- 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;
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment