%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP489-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sat Jul 16 10:30:30 EDT 2022
% Result : Unsatisfiable 1.30s 0.68s
% Output : CNFRefutation 1.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP489-1 : TPTP v8.1.0. Released v2.6.0.
% 0.06/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jun 14 10:33:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 1916: Facts:
% 0.12/0.34 1916: Id : 2, {_}:
% 0.12/0.34 double_divide ?2
% 0.12/0.34 (double_divide
% 0.12/0.34 (double_divide
% 0.12/0.34 (double_divide identity
% 0.12/0.34 (double_divide (double_divide ?2 identity)
% 0.12/0.34 (double_divide ?3 ?4))) ?3) identity)
% 0.12/0.34 =>=
% 0.12/0.34 ?4
% 0.12/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.34 1916: Id : 3, {_}:
% 0.12/0.34 multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity
% 0.12/0.34 [7, 6] by multiply ?6 ?7
% 0.12/0.34 1916: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.34 1916: Id : 5, {_}:
% 0.12/0.34 identity =<= double_divide ?11 (inverse ?11)
% 0.12/0.34 [11] by identity ?11
% 0.12/0.34 1916: Goal:
% 0.12/0.34 1916: Id : 1, {_}:
% 0.12/0.34 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.12/0.34 [] by prove_these_axioms_3
% 1.30/0.68 Statistics :
% 1.30/0.68 Max weight : 34
% 1.30/0.68 Found proof, 0.343920s
% 1.30/0.68 % SZS status Unsatisfiable for theBenchmark.p
% 1.30/0.68 % SZS output start CNFRefutation for theBenchmark.p
% 1.30/0.68 Id : 6, {_}: double_divide ?13 (double_divide (double_divide (double_divide identity (double_divide (double_divide ?13 identity) (double_divide ?14 ?15))) ?14) identity) =>= ?15 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 1.30/0.68 Id : 13, {_}: multiply ?37 ?38 =<= double_divide (double_divide ?38 ?37) identity [38, 37] by multiply ?37 ?38
% 1.30/0.68 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 1.30/0.68 Id : 2, {_}: double_divide ?2 (double_divide (double_divide (double_divide identity (double_divide (double_divide ?2 identity) (double_divide ?3 ?4))) ?3) identity) =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 1.30/0.68 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 1.30/0.68 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 1.30/0.68 Id : 17, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 1.30/0.68 Id : 10, {_}: double_divide ?2 (multiply ?3 (double_divide identity (double_divide (double_divide ?2 identity) (double_divide ?3 ?4)))) =>= ?4 [4, 3, 2] by Demod 2 with 3 at 2,2
% 1.30/0.68 Id : 18, {_}: double_divide ?2 (multiply ?3 (double_divide identity (double_divide (inverse ?2) (double_divide ?3 ?4)))) =>= ?4 [4, 3, 2] by Demod 10 with 4 at 1,2,2,2,2
% 1.30/0.68 Id : 23, {_}: double_divide ?59 (multiply ?60 (double_divide identity (double_divide (inverse ?59) identity))) =>= inverse ?60 [60, 59] by Super 18 with 5 at 2,2,2,2,2
% 1.30/0.68 Id : 28, {_}: double_divide ?59 (multiply ?60 (double_divide identity (inverse (inverse ?59)))) =>= inverse ?60 [60, 59] by Demod 23 with 4 at 2,2,2,2
% 1.30/0.68 Id : 14, {_}: multiply (multiply ?40 (double_divide identity (double_divide (double_divide ?41 identity) (double_divide ?40 ?42)))) ?41 =>= double_divide ?42 identity [42, 41, 40] by Super 13 with 10 at 1,3
% 1.30/0.68 Id : 841, {_}: multiply (multiply ?40 (double_divide identity (double_divide (inverse ?41) (double_divide ?40 ?42)))) ?41 =>= double_divide ?42 identity [42, 41, 40] by Demod 14 with 4 at 1,2,2,1,2
% 1.30/0.68 Id : 842, {_}: multiply (multiply ?40 (double_divide identity (double_divide (inverse ?41) (double_divide ?40 ?42)))) ?41 =>= inverse ?42 [42, 41, 40] by Demod 841 with 4 at 3
% 1.30/0.68 Id : 296, {_}: double_divide ?621 (multiply ?622 (double_divide identity (inverse (inverse ?621)))) =>= inverse ?622 [622, 621] by Demod 23 with 4 at 2,2,2,2
% 1.30/0.68 Id : 19, {_}: multiply identity ?50 =>= inverse (inverse ?50) [50] by Super 17 with 4 at 1,3
% 1.30/0.68 Id : 302, {_}: double_divide ?638 (inverse (inverse (double_divide identity (inverse (inverse ?638))))) =>= inverse identity [638] by Super 296 with 19 at 2,2
% 1.30/0.68 Id : 312, {_}: double_divide ?638 (inverse (multiply (inverse (inverse ?638)) identity)) =>= inverse identity [638] by Demod 302 with 17 at 1,2,2
% 1.30/0.68 Id : 83, {_}: multiply (inverse ?210) ?210 =>= inverse identity [210] by Super 17 with 5 at 1,3
% 1.30/0.68 Id : 84, {_}: multiply (multiply ?212 ?213) (double_divide ?213 ?212) =>= inverse identity [213, 212] by Super 83 with 17 at 1,2
% 1.30/0.68 Id : 304, {_}: double_divide ?642 (inverse identity) =<= inverse (multiply (inverse (inverse ?642)) identity) [642] by Super 296 with 84 at 2,2
% 1.30/0.68 Id : 975, {_}: double_divide ?638 (double_divide ?638 (inverse identity)) =>= inverse identity [638] by Demod 312 with 304 at 2,2
% 1.30/0.68 Id : 993, {_}: multiply (multiply (inverse ?1621) (double_divide identity (inverse identity))) ?1621 =>= inverse (inverse identity) [1621] by Super 842 with 975 at 2,2,1,2
% 1.30/0.68 Id : 1063, {_}: multiply (multiply (inverse ?1693) identity) ?1693 =>= inverse (inverse identity) [1693] by Demod 993 with 5 at 2,1,2
% 1.30/0.68 Id : 24, {_}: multiply (inverse ?62) ?62 =>= inverse identity [62] by Super 17 with 5 at 1,3
% 1.30/0.68 Id : 1075, {_}: multiply (inverse identity) identity =>= inverse (inverse identity) [] by Super 1063 with 24 at 1,2
% 1.30/0.68 Id : 1087, {_}: inverse identity =<= inverse (inverse identity) [] by Demod 1075 with 24 at 2
% 1.30/0.68 Id : 1105, {_}: double_divide identity (multiply ?1727 (double_divide identity (inverse identity))) =>= inverse ?1727 [1727] by Super 28 with 1087 at 2,2,2,2
% 1.30/0.68 Id : 1141, {_}: double_divide identity (multiply ?1727 identity) =>= inverse ?1727 [1727] by Demod 1105 with 5 at 2,2,2
% 1.30/0.68 Id : 1355, {_}: multiply (multiply ?1901 identity) identity =>= inverse (inverse ?1901) [1901] by Super 17 with 1141 at 1,3
% 1.30/0.68 Id : 1472, {_}: double_divide identity (inverse (inverse ?2014)) =>= inverse (multiply ?2014 identity) [2014] by Super 1141 with 1355 at 2,2
% 1.30/0.68 Id : 1115, {_}: double_divide identity (inverse identity) =<= inverse (multiply (inverse identity) identity) [] by Super 304 with 1087 at 1,1,3
% 1.30/0.68 Id : 1135, {_}: identity =<= inverse (multiply (inverse identity) identity) [] by Demod 1115 with 5 at 2
% 1.30/0.68 Id : 1136, {_}: identity =<= inverse (inverse identity) [] by Demod 1135 with 24 at 1,3
% 1.30/0.68 Id : 1137, {_}: identity =<= inverse identity [] by Demod 1136 with 1087 at 3
% 1.30/0.68 Id : 1183, {_}: double_divide ?642 identity =<= inverse (multiply (inverse (inverse ?642)) identity) [642] by Demod 304 with 1137 at 2,2
% 1.30/0.68 Id : 1200, {_}: inverse ?642 =<= inverse (multiply (inverse (inverse ?642)) identity) [642] by Demod 1183 with 4 at 2
% 1.30/0.68 Id : 323, {_}: double_divide ?678 (inverse identity) =<= inverse (multiply (inverse (inverse ?678)) identity) [678] by Super 296 with 84 at 2,2
% 1.30/0.68 Id : 409, {_}: double_divide (double_divide ?821 ?822) (inverse identity) =<= inverse (multiply (inverse (multiply ?822 ?821)) identity) [822, 821] by Super 323 with 17 at 1,1,1,3
% 1.30/0.68 Id : 416, {_}: double_divide (double_divide identity (inverse (inverse ?842))) (inverse identity) =>= inverse (multiply (double_divide ?842 (inverse identity)) identity) [842] by Super 409 with 304 at 1,1,3
% 1.30/0.68 Id : 628, {_}: multiply (inverse identity) (double_divide identity (inverse (inverse ?1205))) =>= inverse (inverse (multiply (double_divide ?1205 (inverse identity)) identity)) [1205] by Super 17 with 416 at 1,3
% 1.30/0.68 Id : 1186, {_}: multiply identity (double_divide identity (inverse (inverse ?1205))) =<= inverse (inverse (multiply (double_divide ?1205 (inverse identity)) identity)) [1205] by Demod 628 with 1137 at 1,2
% 1.30/0.68 Id : 1187, {_}: multiply identity (double_divide identity (inverse (inverse ?1205))) =>= inverse (inverse (multiply (double_divide ?1205 identity) identity)) [1205] by Demod 1186 with 1137 at 2,1,1,1,3
% 1.30/0.68 Id : 1195, {_}: inverse (inverse (double_divide identity (inverse (inverse ?1205)))) =>= inverse (inverse (multiply (double_divide ?1205 identity) identity)) [1205] by Demod 1187 with 19 at 2
% 1.30/0.68 Id : 1196, {_}: inverse (inverse (double_divide identity (inverse (inverse ?1205)))) =>= inverse (inverse (multiply (inverse ?1205) identity)) [1205] by Demod 1195 with 4 at 1,1,1,3
% 1.30/0.68 Id : 1197, {_}: inverse (multiply (inverse (inverse ?1205)) identity) =>= inverse (inverse (multiply (inverse ?1205) identity)) [1205] by Demod 1196 with 17 at 1,2
% 1.30/0.68 Id : 1201, {_}: inverse ?642 =<= inverse (inverse (multiply (inverse ?642) identity)) [642] by Demod 1200 with 1197 at 3
% 1.30/0.68 Id : 1477, {_}: double_divide identity (inverse ?2025) =<= inverse (multiply (multiply (inverse ?2025) identity) identity) [2025] by Super 1472 with 1201 at 2,2
% 1.30/0.68 Id : 1609, {_}: double_divide identity (inverse ?2132) =<= inverse (inverse (inverse (inverse ?2132))) [2132] by Demod 1477 with 1355 at 1,3
% 1.30/0.68 Id : 1475, {_}: double_divide identity (inverse (inverse ?2020)) =<= inverse (multiply (inverse (multiply (inverse ?2020) identity)) identity) [2020] by Super 1472 with 1201 at 1,2,2
% 1.30/0.68 Id : 1407, {_}: double_divide identity (inverse (inverse ?1955)) =>= inverse (multiply ?1955 identity) [1955] by Super 1141 with 1355 at 2,2
% 1.30/0.68 Id : 1502, {_}: inverse (multiply ?2020 identity) =<= inverse (multiply (inverse (multiply (inverse ?2020) identity)) identity) [2020] by Demod 1475 with 1407 at 2
% 1.30/0.68 Id : 327, {_}: double_divide (double_divide ?685 ?686) (inverse identity) =<= inverse (multiply (inverse (multiply ?686 ?685)) identity) [686, 685] by Super 323 with 17 at 1,1,1,3
% 1.30/0.68 Id : 1178, {_}: double_divide (double_divide ?685 ?686) identity =<= inverse (multiply (inverse (multiply ?686 ?685)) identity) [686, 685] by Demod 327 with 1137 at 2,2
% 1.30/0.68 Id : 1204, {_}: inverse (double_divide ?685 ?686) =<= inverse (multiply (inverse (multiply ?686 ?685)) identity) [686, 685] by Demod 1178 with 4 at 2
% 1.30/0.68 Id : 1205, {_}: multiply ?686 ?685 =<= inverse (multiply (inverse (multiply ?686 ?685)) identity) [685, 686] by Demod 1204 with 17 at 2
% 1.30/0.68 Id : 1503, {_}: inverse (multiply ?2020 identity) =<= multiply (inverse ?2020) identity [2020] by Demod 1502 with 1205 at 3
% 1.30/0.68 Id : 1511, {_}: inverse ?642 =<= inverse (inverse (inverse (multiply ?642 identity))) [642] by Demod 1201 with 1503 at 1,1,3
% 1.30/0.68 Id : 1615, {_}: double_divide identity (inverse (inverse (inverse (multiply ?2144 identity)))) =>= inverse (inverse (inverse (inverse ?2144))) [2144] by Super 1609 with 1511 at 1,1,1,3
% 1.30/0.68 Id : 1660, {_}: inverse (multiply (inverse (multiply ?2144 identity)) identity) =>= inverse (inverse (inverse (inverse ?2144))) [2144] by Demod 1615 with 1407 at 2
% 1.30/0.68 Id : 1505, {_}: double_divide identity (inverse ?2025) =<= inverse (inverse (inverse (inverse ?2025))) [2025] by Demod 1477 with 1355 at 1,3
% 1.30/0.68 Id : 1661, {_}: inverse (multiply (inverse (multiply ?2144 identity)) identity) =>= double_divide identity (inverse ?2144) [2144] by Demod 1660 with 1505 at 3
% 1.30/0.68 Id : 1662, {_}: inverse (inverse (multiply (multiply ?2144 identity) identity)) =>= double_divide identity (inverse ?2144) [2144] by Demod 1661 with 1503 at 1,2
% 1.30/0.68 Id : 1512, {_}: multiply ?686 ?685 =<= inverse (inverse (multiply (multiply ?686 ?685) identity)) [685, 686] by Demod 1205 with 1503 at 1,3
% 1.30/0.68 Id : 1663, {_}: multiply ?2144 identity =<= double_divide identity (inverse ?2144) [2144] by Demod 1662 with 1512 at 2
% 1.30/0.68 Id : 1473, {_}: double_divide identity (inverse (multiply ?2016 ?2017)) =>= inverse (multiply (double_divide ?2017 ?2016) identity) [2017, 2016] by Super 1472 with 17 at 1,2,2
% 1.30/0.68 Id : 2359, {_}: multiply (multiply ?2016 ?2017) identity =<= inverse (multiply (double_divide ?2017 ?2016) identity) [2017, 2016] by Demod 1473 with 1663 at 2
% 1.30/0.68 Id : 1460, {_}: double_divide ?59 (multiply ?60 (inverse (multiply ?59 identity))) =>= inverse ?60 [60, 59] by Demod 28 with 1407 at 2,2,2
% 1.30/0.68 Id : 1611, {_}: double_divide identity (inverse (double_divide ?2136 ?2137)) =>= inverse (inverse (inverse (multiply ?2137 ?2136))) [2137, 2136] by Super 1609 with 17 at 1,1,1,3
% 1.30/0.68 Id : 1643, {_}: double_divide identity (multiply ?2137 ?2136) =<= inverse (inverse (inverse (multiply ?2137 ?2136))) [2136, 2137] by Demod 1611 with 17 at 2,2
% 1.30/0.68 Id : 1692, {_}: multiply ?2201 identity =<= double_divide identity (inverse ?2201) [2201] by Demod 1662 with 1512 at 2
% 1.30/0.68 Id : 1695, {_}: multiply (double_divide ?2207 ?2208) identity =<= double_divide identity (multiply ?2208 ?2207) [2208, 2207] by Super 1692 with 17 at 2,3
% 1.30/0.68 Id : 2477, {_}: multiply (double_divide ?2136 ?2137) identity =<= inverse (inverse (inverse (multiply ?2137 ?2136))) [2137, 2136] by Demod 1643 with 1695 at 2
% 1.30/0.68 Id : 20, {_}: double_divide ?52 (multiply ?53 (double_divide identity (double_divide (inverse ?52) (inverse ?53)))) =>= identity [53, 52] by Super 18 with 4 at 2,2,2,2,2
% 1.30/0.68 Id : 1792, {_}: multiply (double_divide (double_divide identity (double_divide (inverse identity) (inverse ?2286))) ?2286) identity =>= identity [2286] by Super 20 with 1695 at 2
% 1.30/0.68 Id : 1818, {_}: multiply (double_divide (double_divide identity (double_divide identity (inverse ?2286))) ?2286) identity =>= identity [2286] by Demod 1792 with 1137 at 1,2,1,1,2
% 1.30/0.68 Id : 1819, {_}: multiply (double_divide (double_divide identity (multiply ?2286 identity)) ?2286) identity =>= identity [2286] by Demod 1818 with 1663 at 2,1,1,2
% 1.30/0.68 Id : 1820, {_}: multiply (double_divide (multiply (double_divide identity ?2286) identity) ?2286) identity =>= identity [2286] by Demod 1819 with 1695 at 1,1,2
% 1.30/0.68 Id : 1776, {_}: multiply (double_divide identity ?1727) identity =>= inverse ?1727 [1727] by Demod 1141 with 1695 at 2
% 1.30/0.68 Id : 1821, {_}: multiply (double_divide (inverse ?2286) ?2286) identity =>= identity [2286] by Demod 1820 with 1776 at 1,1,2
% 1.30/0.68 Id : 2621, {_}: multiply (double_divide identity (double_divide (inverse ?3351) ?3351)) identity =>= inverse (inverse (inverse identity)) [3351] by Super 2477 with 1821 at 1,1,1,3
% 1.30/0.68 Id : 2640, {_}: inverse (double_divide (inverse ?3351) ?3351) =>= inverse (inverse (inverse identity)) [3351] by Demod 2621 with 1776 at 2
% 1.30/0.68 Id : 2641, {_}: inverse (double_divide (inverse ?3351) ?3351) =>= inverse (inverse identity) [3351] by Demod 2640 with 1137 at 1,1,3
% 1.30/0.68 Id : 2642, {_}: multiply ?3351 (inverse ?3351) =>= inverse (inverse identity) [3351] by Demod 2641 with 17 at 2
% 1.30/0.68 Id : 2643, {_}: multiply ?3351 (inverse ?3351) =>= inverse identity [3351] by Demod 2642 with 1137 at 1,3
% 1.30/0.68 Id : 2644, {_}: multiply ?3351 (inverse ?3351) =>= identity [3351] by Demod 2643 with 1137 at 3
% 1.30/0.68 Id : 2709, {_}: double_divide ?3395 identity =<= inverse (multiply ?3395 identity) [3395] by Super 1460 with 2644 at 2,2
% 1.30/0.68 Id : 2756, {_}: inverse ?3395 =<= inverse (multiply ?3395 identity) [3395] by Demod 2709 with 4 at 2
% 1.30/0.68 Id : 2772, {_}: multiply (multiply ?2016 ?2017) identity =>= inverse (double_divide ?2017 ?2016) [2017, 2016] by Demod 2359 with 2756 at 3
% 1.30/0.68 Id : 2791, {_}: multiply (multiply ?2016 ?2017) identity =>= multiply ?2016 ?2017 [2017, 2016] by Demod 2772 with 17 at 3
% 1.30/0.68 Id : 2792, {_}: multiply ?1901 identity =>= inverse (inverse ?1901) [1901] by Demod 1355 with 2791 at 2
% 1.30/0.68 Id : 2794, {_}: inverse (inverse ?2144) =<= double_divide identity (inverse ?2144) [2144] by Demod 1663 with 2792 at 2
% 1.30/0.68 Id : 2777, {_}: double_divide ?59 (multiply ?60 (inverse ?59)) =>= inverse ?60 [60, 59] by Demod 1460 with 2756 at 2,2,2
% 1.30/0.68 Id : 982, {_}: double_divide ?1590 (multiply (inverse ?1590) (double_divide identity (inverse identity))) =>= inverse identity [1590] by Super 18 with 975 at 2,2,2,2
% 1.30/0.68 Id : 1013, {_}: double_divide ?1590 (multiply (inverse ?1590) identity) =>= inverse identity [1590] by Demod 982 with 5 at 2,2,2
% 1.30/0.68 Id : 2046, {_}: double_divide ?1590 (inverse (multiply ?1590 identity)) =>= inverse identity [1590] by Demod 1013 with 1503 at 2,2
% 1.30/0.68 Id : 2047, {_}: double_divide ?1590 (inverse (multiply ?1590 identity)) =>= identity [1590] by Demod 2046 with 1137 at 3
% 1.30/0.68 Id : 2052, {_}: multiply (multiply ?2804 (double_divide identity (double_divide (inverse ?2805) identity))) ?2805 =>= inverse (inverse (multiply ?2804 identity)) [2805, 2804] by Super 842 with 2047 at 2,2,2,1,2
% 1.30/0.68 Id : 2131, {_}: multiply (multiply ?2804 (double_divide identity (inverse (inverse ?2805)))) ?2805 =>= inverse (inverse (multiply ?2804 identity)) [2805, 2804] by Demod 2052 with 4 at 2,2,1,2
% 1.30/0.68 Id : 2132, {_}: multiply (multiply ?2804 (multiply (inverse ?2805) identity)) ?2805 =>= inverse (inverse (multiply ?2804 identity)) [2805, 2804] by Demod 2131 with 1663 at 2,1,2
% 1.30/0.68 Id : 2133, {_}: multiply (multiply ?2804 (inverse (multiply ?2805 identity))) ?2805 =>= inverse (inverse (multiply ?2804 identity)) [2805, 2804] by Demod 2132 with 1503 at 2,1,2
% 1.30/0.68 Id : 3591, {_}: multiply (multiply ?2804 (inverse (inverse (inverse ?2805)))) ?2805 =>= inverse (inverse (multiply ?2804 identity)) [2805, 2804] by Demod 2133 with 2792 at 1,2,1,2
% 1.30/0.68 Id : 2778, {_}: multiply ?686 ?685 =<= inverse (inverse (multiply ?686 ?685)) [685, 686] by Demod 1512 with 2756 at 1,3
% 1.30/0.68 Id : 3592, {_}: multiply (multiply ?2804 (inverse (inverse (inverse ?2805)))) ?2805 =>= multiply ?2804 identity [2805, 2804] by Demod 3591 with 2778 at 3
% 1.30/0.68 Id : 2800, {_}: inverse ?3395 =<= inverse (inverse (inverse ?3395)) [3395] by Demod 2756 with 2792 at 1,3
% 1.30/0.68 Id : 3593, {_}: multiply (multiply ?2804 (inverse ?2805)) ?2805 =>= multiply ?2804 identity [2805, 2804] by Demod 3592 with 2800 at 2,1,2
% 1.30/0.68 Id : 3594, {_}: multiply (multiply ?2804 (inverse ?2805)) ?2805 =>= inverse (inverse ?2804) [2805, 2804] by Demod 3593 with 2792 at 3
% 1.30/0.68 Id : 3799, {_}: double_divide ?4473 (inverse (inverse ?4474)) =<= inverse (multiply ?4474 (inverse (inverse ?4473))) [4474, 4473] by Super 2777 with 3594 at 2,2
% 1.30/0.68 Id : 3810, {_}: double_divide ?4513 (inverse (inverse (multiply ?4514 (double_divide identity (double_divide (inverse (inverse (inverse ?4513))) (double_divide ?4514 ?4515)))))) =>= inverse (inverse ?4515) [4515, 4514, 4513] by Super 3799 with 842 at 1,3
% 1.30/0.68 Id : 3851, {_}: double_divide ?4513 (multiply ?4514 (double_divide identity (double_divide (inverse (inverse (inverse ?4513))) (double_divide ?4514 ?4515)))) =>= inverse (inverse ?4515) [4515, 4514, 4513] by Demod 3810 with 2778 at 2,2
% 1.30/0.68 Id : 3852, {_}: double_divide ?4513 (multiply ?4514 (double_divide identity (double_divide (inverse ?4513) (double_divide ?4514 ?4515)))) =>= inverse (inverse ?4515) [4515, 4514, 4513] by Demod 3851 with 2800 at 1,2,2,2,2
% 1.30/0.68 Id : 3853, {_}: ?4515 =<= inverse (inverse ?4515) [4515] by Demod 3852 with 18 at 2
% 1.30/0.68 Id : 3872, {_}: ?2144 =<= double_divide identity (inverse ?2144) [2144] by Demod 2794 with 3853 at 2
% 1.30/0.68 Id : 3896, {_}: inverse ?4579 =<= double_divide identity ?4579 [4579] by Super 3872 with 3853 at 2,3
% 1.30/0.68 Id : 3917, {_}: double_divide ?2 (multiply ?3 (inverse (double_divide (inverse ?2) (double_divide ?3 ?4)))) =>= ?4 [4, 3, 2] by Demod 18 with 3896 at 2,2,2
% 1.30/0.68 Id : 3937, {_}: double_divide ?2 (multiply ?3 (multiply (double_divide ?3 ?4) (inverse ?2))) =>= ?4 [4, 3, 2] by Demod 3917 with 17 at 2,2,2
% 1.30/0.68 Id : 3945, {_}: inverse (multiply ?4613 (multiply (double_divide ?4613 ?4614) (inverse identity))) =>= ?4614 [4614, 4613] by Super 3937 with 3896 at 2
% 1.30/0.68 Id : 3596, {_}: double_divide ?4170 (inverse (inverse ?4171)) =<= inverse (multiply ?4171 (inverse (inverse ?4170))) [4171, 4170] by Super 2777 with 3594 at 2,2
% 1.30/0.68 Id : 3867, {_}: double_divide ?4170 ?4171 =<= inverse (multiply ?4171 (inverse (inverse ?4170))) [4171, 4170] by Demod 3596 with 3853 at 2,2
% 1.30/0.68 Id : 3868, {_}: double_divide ?4170 ?4171 =<= inverse (multiply ?4171 ?4170) [4171, 4170] by Demod 3867 with 3853 at 2,1,3
% 1.30/0.68 Id : 4015, {_}: double_divide (multiply (double_divide ?4613 ?4614) (inverse identity)) ?4613 =>= ?4614 [4614, 4613] by Demod 3945 with 3868 at 2
% 1.30/0.68 Id : 4016, {_}: double_divide (multiply (double_divide ?4613 ?4614) identity) ?4613 =>= ?4614 [4614, 4613] by Demod 4015 with 1137 at 2,1,2
% 1.30/0.68 Id : 3873, {_}: multiply ?1901 identity =>= ?1901 [1901] by Demod 2792 with 3853 at 3
% 1.30/0.68 Id : 4017, {_}: double_divide (double_divide ?4613 ?4614) ?4613 =>= ?4614 [4614, 4613] by Demod 4016 with 3873 at 1,2
% 1.30/0.68 Id : 4056, {_}: multiply ?4740 (double_divide ?4740 ?4741) =>= inverse ?4741 [4741, 4740] by Super 17 with 4017 at 1,3
% 1.30/0.68 Id : 7, {_}: double_divide ?17 (double_divide (double_divide (double_divide identity (double_divide (double_divide ?17 identity) ?18)) ?19) identity) =?= double_divide (double_divide (double_divide identity (double_divide (double_divide ?19 identity) (double_divide ?20 ?18))) ?20) identity [20, 19, 18, 17] by Super 6 with 2 at 2,2,1,1,2,2
% 1.30/0.68 Id : 42, {_}: double_divide ?17 (inverse (double_divide (double_divide identity (double_divide (double_divide ?17 identity) ?18)) ?19)) =?= double_divide (double_divide (double_divide identity (double_divide (double_divide ?19 identity) (double_divide ?20 ?18))) ?20) identity [20, 19, 18, 17] by Demod 7 with 4 at 2,2
% 1.30/0.68 Id : 43, {_}: double_divide ?17 (inverse (double_divide (double_divide identity (double_divide (double_divide ?17 identity) ?18)) ?19)) =?= inverse (double_divide (double_divide identity (double_divide (double_divide ?19 identity) (double_divide ?20 ?18))) ?20) [20, 19, 18, 17] by Demod 42 with 4 at 3
% 1.30/0.68 Id : 44, {_}: double_divide ?17 (multiply ?19 (double_divide identity (double_divide (double_divide ?17 identity) ?18))) =?= inverse (double_divide (double_divide identity (double_divide (double_divide ?19 identity) (double_divide ?20 ?18))) ?20) [20, 18, 19, 17] by Demod 43 with 17 at 2,2
% 1.30/0.68 Id : 45, {_}: double_divide ?17 (multiply ?19 (double_divide identity (double_divide (double_divide ?17 identity) ?18))) =?= multiply ?20 (double_divide identity (double_divide (double_divide ?19 identity) (double_divide ?20 ?18))) [20, 18, 19, 17] by Demod 44 with 17 at 3
% 1.30/0.68 Id : 46, {_}: double_divide ?17 (multiply ?19 (double_divide identity (double_divide (inverse ?17) ?18))) =?= multiply ?20 (double_divide identity (double_divide (double_divide ?19 identity) (double_divide ?20 ?18))) [20, 18, 19, 17] by Demod 45 with 4 at 1,2,2,2,2
% 1.30/0.68 Id : 47, {_}: double_divide ?17 (multiply ?19 (double_divide identity (double_divide (inverse ?17) ?18))) =?= multiply ?20 (double_divide identity (double_divide (inverse ?19) (double_divide ?20 ?18))) [20, 18, 19, 17] by Demod 46 with 4 at 1,2,2,3
% 1.30/0.68 Id : 50, {_}: double_divide ?98 (double_divide ?99 (multiply ?98 (double_divide identity (double_divide (inverse ?99) ?100)))) =>= ?100 [100, 99, 98] by Super 18 with 47 at 2,2
% 1.30/0.68 Id : 4359, {_}: double_divide ?98 (double_divide ?99 (multiply ?98 (inverse (double_divide (inverse ?99) ?100)))) =>= ?100 [100, 99, 98] by Demod 50 with 3896 at 2,2,2,2
% 1.30/0.68 Id : 4379, {_}: double_divide ?5327 (double_divide ?5328 (multiply ?5327 (multiply ?5329 (inverse ?5328)))) =>= ?5329 [5329, 5328, 5327] by Demod 4359 with 17 at 2,2,2,2
% 1.30/0.68 Id : 3869, {_}: multiply (multiply ?2804 (inverse ?2805)) ?2805 =>= ?2804 [2805, 2804] by Demod 3594 with 3853 at 3
% 1.30/0.68 Id : 4386, {_}: double_divide ?5354 (double_divide ?5355 (multiply ?5354 ?5356)) =>= multiply ?5356 (inverse (inverse ?5355)) [5356, 5355, 5354] by Super 4379 with 3869 at 2,2,2,2
% 1.30/0.68 Id : 4421, {_}: double_divide ?5354 (double_divide ?5355 (multiply ?5354 ?5356)) =>= multiply ?5356 ?5355 [5356, 5355, 5354] by Demod 4386 with 3853 at 2,3
% 1.30/0.68 Id : 5772, {_}: multiply ?7258 (multiply ?7259 ?7260) =<= inverse (double_divide ?7260 (multiply ?7258 ?7259)) [7260, 7259, 7258] by Super 4056 with 4421 at 2,2
% 1.30/0.68 Id : 5820, {_}: multiply ?7258 (multiply ?7259 ?7260) =<= multiply (multiply ?7258 ?7259) ?7260 [7260, 7259, 7258] by Demod 5772 with 17 at 3
% 1.30/0.68 Id : 6318, {_}: multiply a3 (multiply b3 c3) =?= multiply a3 (multiply b3 c3) [] by Demod 1 with 5820 at 2
% 1.30/0.68 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 1.30/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.68 1917: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.338345 using kbo
%------------------------------------------------------------------------------