Improve formatting

source/casestudies/2023-cade/Category Theory/result_overview.txt

@@ -5,7 +5,10 @@ Total:
 translated DHOL: 3/6 lemmas proved by some prover, 20 successful proofs found in total
 native HOL:	     5/6 lemmas proved by some prover, 25 successful proofs found in total
 
-Lemma 1:
+======
+= transitiveIsomorphic (lemma 1) =
+======
+
 translated DHOL - 13/18 HOL ATP prover succeed:
 % RESULT: SOT_BWCW6Y - agsyHOL---1.0 says Theorem - CPU = 0.00 WC = 0.05 
 % RESULT: SOT_BWCW6Y - cocATP---0.2.0 says Theorem - CPU = 0.00 WC = 1.24 
@@ -46,7 +49,10 @@ native HOL - 9/18 HOL ATP prover succeed:
 % RESULT: SOT_6WGjU7 - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.09 
 % RESULT: SOT_6WGjU7 - Zipperpin---2.1 says Theorem - CPU = 0.00 WC = 0.87 
 
-Lemma 2:
+======
+= uniquenessProd (lemma 2) =
+======
+
 translated DHOL - 0/18 HOL ATP prover succeed:
 % RESULT: SOT_aCz4z4 - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_aCz4z4 - cocATP---0.2.0 says Timeout - CPU = 62.50 WC = 62.66 
@@ -87,7 +93,11 @@ native HOL - 0/18 HOL ATP prover succeed:
 % RESULT: SOT_ooO59W - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.11 
 % RESULT: SOT_ooO59W - Zipperpin---2.1 says Timeout - CPU = 317.69 WC = 9.81 
 
-Lemma 3
+
+======
+= symmetricIsProd (lemma 3) =
+======
+
 translated DHOL - 5/18 HOL ATP prover succeed:
 % RESULT: SOT_nppqvU - agsyHOL---1.0 says Theorem - CPU = 0.00 WC = 0.12 
 % RESULT: SOT_nppqvU - cocATP---0.2.0 says Timeout - CPU = 62.63 WC = 62.72 
@@ -128,7 +138,11 @@ native HOL: - 4/18 HOL ATP prover succeed:
 % RESULT: SOT_0ceY90 - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.07 
 % RESULT: SOT_0ceY90 - Zipperpin---2.1 says Theorem - CPU = 0.00 WC = 1.27 
 
-Lemma 4
+
+======
+= isProdUnique (lemma 4) =
+======
+
 translated DHOL - 0/18 HOL ATP prover succeed:
 % RESULT: SOT_Rgt07Q - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_Rgt07Q - cocATP---0.2.0 says Timeout - CPU = 62.85 WC = 65.24 
@@ -169,7 +183,11 @@ native HOL - 5/18 HOL ATP prover succeed:
 % RESULT: SOT_sFKE0q - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.09 
 % RESULT: SOT_sFKE0q - Zipperpin---2.1 says Theorem - CPU = 0.00 WC = 3.61 
 
-Lemma 5:
+
+======
+= symmetricProd (lemma 5) =
+======
+
 translated DHOL - 2/18 HOL ATP prover succeed:
 % RESULT: SOT_SKb2Cd - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_SKb2Cd - cocATP---0.2.0 says Timeout - CPU = 63.56 WC = 63.81 
@@ -210,7 +228,11 @@ native HOL - 3/18 HOL ATP prover succeed:
 % RESULT: SOT_wUWHCv - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.08 
 % RESULT: SOT_wUWHCv - Zipperpin---2.1 says Theorem - CPU = 0.00 WC = 1.18 
 
-Lemma 6:
+
+======
+= assocProd (lemma 6) =
+======
+
 translated DHOL - 0/18 HOL ATP prover succeed:
 % RESULT: SOT_u5UrA4 - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_u5UrA4 - cocATP---0.2.0 says Timeout - CPU = 61.92 WC = 62.04 

source/casestudies/2023-cade/FunctionsOnSets/test-results-function-composition-lemmas.txt

 Results from proving the translations of the 6 lemmas by different HOL provers via https://www.tptp.org/cgi-bin/SystemOnTPTP 
 5/6 lemmas are proved by some prover.
 
-Lemma 1:
+======
+= concatAssocAppl (lemma 1) =
+======
+
 % RESULT: SOT_DLMVIz - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_DLMVIz - cvc5---1.0 says Theorem - CPU = 0.00 WC = 0.14 
 % RESULT: SOT_DLMVIz - cvc5-SAT---1.0 says Timeout - CPU = 61.04 WC = 61.43 
@@ -20,7 +23,10 @@ Lemma 1:
 % RESULT: SOT_DLMVIz - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.06 
 % RESULT: SOT_DLMVIz - Zipperpin---2.1 says Theorem - CPU = 0.42 WC = 1.02 
 
-Lemma 2:
+======
+= concatAssoc (lemma 2) =
+======
+
 % RESULT: SOT_6ft6o7 - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_6ft6o7 - cvc5---1.0 says Timeout - CPU = 60.53 WC = 61.35 
 % RESULT: SOT_6ft6o7 - cvc5-SAT---1.0 says Timeout - CPU = 60.48 WC = 61.12 
@@ -39,7 +45,10 @@ Lemma 2:
 % RESULT: SOT_6ft6o7 - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.04 
 % RESULT: SOT_6ft6o7 - Zipperpin---2.1 says Timeout - CPU = 101.38 WC = 4.07 
 
-Lemma 3:
+======
+= left_right_inverses (lemma 3) =
+======
+
 % RESULT: SOT_QstGO0 - agsyHOL---1.0 says Theorem - CPU = 12.78 WC = 13.50 
 % RESULT: SOT_QstGO0 - cvc5---1.0 says Theorem - CPU = 0.00 WC = 0.30 
 % RESULT: SOT_QstGO0 - cvc5-SAT---1.0 says Timeout - CPU = 60.40 WC = 63.01 
@@ -57,7 +66,10 @@ Lemma 3:
 % RESULT: SOT_QstGO0 - Vampire---4.7 says Theorem - CPU = 0.00 WC = 0.15 
 % RESULT: SOT_QstGO0 - Zipperpin---2.1 says Timeout - CPU = 105.98 WC = 4.28 
 
-Lemma 4:
+======
+= left_inverse_injective (lemma 4) =
+======
+
 % RESULT: SOT_PsPB7S - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_PsPB7S - cvc5---1.0 says Timeout - CPU = 60.09 WC = 61.04 
 % RESULT: SOT_PsPB7S - cvc5-SAT---1.0 says Timeout - CPU = 60.17 WC = 60.97 
@@ -76,7 +88,10 @@ Lemma 4:
 % RESULT: SOT_PsPB7S - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.05 
 % RESULT: SOT_PsPB7S - Zipperpin---2.1 says Timeout - CPU = 90.61 WC = 3.93 
 
-Lemma 5:
+======
+= right_inverse_surjective (lemma 5) =
+======
+
 % RESULT: SOT_yfFfqb - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.00 
 % RESULT: SOT_yfFfqb - cvc5---1.0 says Timeout - CPU = 60.53 WC = 62.28 
 % RESULT: SOT_yfFfqb - cvc5-SAT---1.0 says Timeout - CPU = 62.63 WC = 64.43 
@@ -95,7 +110,10 @@ Lemma 5:
 % RESULT: SOT_yfFfqb - Vampire-FMO---4.7 says Unknown - CPU = 0.00 WC = 0.06 
 % RESULT: SOT_yfFfqb - Zipperpin---2.1 says Theorem - CPU = 0.40 WC = 1.41 
 
-Lemma 6:
+======
+= inverses_bijective (lemma 6) =
+======
+
 % RESULT: SOT_ALsefO - agsyHOL---1.0 says Timeout - CPU = 60 WC = 60.02 
 % RESULT: SOT_ALsefO - cvc5---1.0 says Theorem - CPU = 1.03 WC = 1.63 
 % RESULT: SOT_ALsefO - cvc5-SAT---1.0 says Timeout - CPU = 60.69 WC = 61.27