From 4b2076e6016901cf55ba20cf68b344473ca26f56 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 31 Mar 2024 18:59:35 +0200
Subject: Report_in_text_file

Txt File Error.txt has been filled
---
 Error.txt | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Error.txt b/Error.txt
index e69de29..7aa836a 100644
--- a/Error.txt
+++ b/Error.txt
@@ -0,0 +1,16 @@
+stack exec zf -- library/test.tex 
+Verification failed: prover found countermodel
+fof(leftinverse_eq_rightinverse,conjecture,fa=fc).
+fof(monoid_right,axiom,![XA]:(monoid(XA)=>![Xa]:(elem(Xa,s__carrier(XA))=>apply(s__mul(XA),pair(Xa,s__neutral(XA)))=Xa))).
+fof(leftinverse_eq_rightinverse1,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=fc).
+fof(leftinverse_eq_rightinverse2,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(fc,s__neutral(fG)))).
+fof(leftinverse_eq_rightinverse3,axiom,fc=apply(s__mul(fG),pair(s__neutral(fG),fc))).
+fof(leftinverse_eq_rightinverse4,axiom,fc=apply(s__mul(fG),pair(fc,s__neutral(fG)))).
+fof(leftinverse_eq_rightinverse5,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(s__neutral(fG),fc))).
+fof(leftinverse_eq_rightinverse6,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(fa,apply(s__mul(fG),pair(fb,fc))))).
+fof(leftinverse_eq_rightinverse7,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(s__neutral(fG),fc))).
+fof(leftinverse_eq_rightinverse8,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)).
+fof(leftinverse_eq_rightinverse9,axiom,apply(s__mul(fG),pair(fb,fc))=s__neutral(fG)&elem(fc,s__carrier(fG))).
+fof(leftinverse_eq_rightinverse10,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)&elem(fb,s__carrier(fG))).
+fof(leftinverse_eq_rightinverse11,axiom,elem(fa,s__carrier(fG))).
+fof(leftinverse_eq_rightinverse12,axiom,group(fG)).
\ No newline at end of file
-- 
cgit v1.2.3