%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP572-1 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n032.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:50 EDT 2022
% Result : Unsatisfiable 0.11s 0.39s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : GRP572-1 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.07/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.11/0.32 % Computer : n032.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Mon Jun 13 09:50:26 EDT 2022
% 0.11/0.32 % CPUTime :
% 0.11/0.32 24695: Facts:
% 0.11/0.32 24695: Id : 2, {_}:
% 0.11/0.32 double_divide
% 0.11/0.32 (double_divide ?2
% 0.11/0.32 (double_divide (double_divide ?3 (double_divide ?2 ?4))
% 0.11/0.32 (double_divide ?4 identity))) (double_divide identity identity)
% 0.11/0.32 =>=
% 0.11/0.32 ?3
% 0.11/0.32 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.11/0.32 24695: Id : 3, {_}:
% 0.11/0.32 multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity
% 0.11/0.32 [7, 6] by multiply ?6 ?7
% 0.11/0.32 24695: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.11/0.32 24695: Id : 5, {_}:
% 0.11/0.32 identity =<= double_divide ?11 (inverse ?11)
% 0.11/0.32 [11] by identity ?11
% 0.11/0.32 24695: Goal:
% 0.11/0.32 24695: Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.11/0.39 Statistics :
% 0.11/0.39 Max weight : 20
% 0.11/0.39 Found proof, 0.073939s
% 0.11/0.39 % SZS status Unsatisfiable for theBenchmark.p
% 0.11/0.39 % SZS output start CNFRefutation for theBenchmark.p
% 0.11/0.39 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 0.11/0.39 Id : 2, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (double_divide ?4 identity))) (double_divide identity identity) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.11/0.39 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.11/0.39 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 0.11/0.39 Id : 16, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 0.11/0.39 Id : 17, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) (double_divide identity identity) =>= ?3 [4, 3, 2] by Demod 2 with 4 at 2,2,1,2
% 0.11/0.39 Id : 18, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) (inverse identity) =>= ?3 [4, 3, 2] by Demod 17 with 4 at 2,2
% 0.11/0.39 Id : 23, {_}: double_divide (double_divide ?59 (double_divide (double_divide ?60 identity) (inverse (inverse ?59)))) (inverse identity) =>= ?60 [60, 59] by Super 18 with 5 at 2,1,2,1,2
% 0.11/0.39 Id : 28, {_}: double_divide (double_divide ?59 (double_divide (inverse ?60) (inverse (inverse ?59)))) (inverse identity) =>= ?60 [60, 59] by Demod 23 with 4 at 1,2,1,2
% 0.11/0.39 Id : 84, {_}: multiply (inverse identity) (double_divide ?134 (double_divide (inverse ?135) (inverse (inverse ?134)))) =>= inverse ?135 [135, 134] by Super 16 with 28 at 1,3
% 0.11/0.39 Id : 180, {_}: double_divide (double_divide ?281 (double_divide (double_divide ?282 (inverse ?281)) (inverse identity))) (inverse identity) =>= ?282 [282, 281] by Super 18 with 4 at 2,1,2,1,2
% 0.11/0.39 Id : 87, {_}: double_divide (double_divide ?144 (double_divide (inverse ?145) (inverse (inverse ?144)))) (inverse identity) =>= ?145 [145, 144] by Demod 23 with 4 at 1,2,1,2
% 0.11/0.39 Id : 90, {_}: double_divide (double_divide ?155 identity) (inverse identity) =>= ?155 [155] by Super 87 with 5 at 2,1,2
% 0.11/0.39 Id : 92, {_}: double_divide (inverse ?155) (inverse identity) =>= ?155 [155] by Demod 90 with 4 at 1,2
% 0.11/0.39 Id : 199, {_}: double_divide (double_divide identity (double_divide ?322 (inverse identity))) (inverse identity) =>= inverse ?322 [322] by Super 180 with 92 at 1,2,1,2
% 0.11/0.39 Id : 206, {_}: double_divide (double_divide identity identity) (inverse identity) =>= inverse identity [] by Super 199 with 5 at 2,1,2
% 0.11/0.40 Id : 218, {_}: double_divide (inverse identity) (inverse identity) =>= inverse identity [] by Demod 206 with 4 at 1,2
% 0.11/0.40 Id : 219, {_}: identity =<= inverse identity [] by Demod 218 with 92 at 2
% 0.11/0.40 Id : 225, {_}: multiply identity (double_divide ?134 (double_divide (inverse ?135) (inverse (inverse ?134)))) =>= inverse ?135 [135, 134] by Demod 84 with 219 at 1,2
% 0.11/0.40 Id : 19, {_}: multiply identity ?50 =>= inverse (inverse ?50) [50] by Super 16 with 4 at 1,3
% 0.11/0.40 Id : 227, {_}: double_divide (inverse ?155) identity =>= ?155 [155] by Demod 92 with 219 at 2,2
% 0.11/0.40 Id : 246, {_}: inverse (inverse ?155) =>= ?155 [155] by Demod 227 with 4 at 2
% 0.11/0.40 Id : 248, {_}: multiply identity ?50 =>= ?50 [50] by Demod 19 with 246 at 3
% 0.11/0.40 Id : 252, {_}: double_divide ?134 (double_divide (inverse ?135) (inverse (inverse ?134))) =>= inverse ?135 [135, 134] by Demod 225 with 248 at 2
% 0.11/0.40 Id : 253, {_}: double_divide ?134 (double_divide (inverse ?135) ?134) =>= inverse ?135 [135, 134] by Demod 252 with 246 at 2,2,2
% 0.11/0.40 Id : 20, {_}: double_divide (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) (inverse identity))) (inverse identity) =>= ?53 [53, 52] by Super 18 with 4 at 2,1,2,1,2
% 0.11/0.40 Id : 234, {_}: double_divide (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) identity)) (inverse identity) =>= ?53 [53, 52] by Demod 20 with 219 at 2,2,1,2
% 0.11/0.40 Id : 235, {_}: double_divide (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) identity)) identity =>= ?53 [53, 52] by Demod 234 with 219 at 2,2
% 0.11/0.40 Id : 236, {_}: inverse (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) identity)) =>= ?53 [53, 52] by Demod 235 with 4 at 2
% 0.11/0.40 Id : 237, {_}: multiply (double_divide (double_divide ?53 (inverse ?52)) identity) ?52 =>= ?53 [52, 53] by Demod 236 with 16 at 2
% 0.11/0.40 Id : 238, {_}: multiply (inverse (double_divide ?53 (inverse ?52))) ?52 =>= ?53 [52, 53] by Demod 237 with 4 at 1,2
% 0.11/0.40 Id : 239, {_}: multiply (multiply (inverse ?52) ?53) ?52 =>= ?53 [53, 52] by Demod 238 with 16 at 1,2
% 0.11/0.40 Id : 230, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) identity =>= ?3 [4, 3, 2] by Demod 18 with 219 at 2,2
% 0.11/0.40 Id : 244, {_}: inverse (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) =>= ?3 [4, 3, 2] by Demod 230 with 4 at 2
% 0.11/0.40 Id : 245, {_}: multiply (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4)) ?2 =>= ?3 [4, 2, 3] by Demod 244 with 16 at 2
% 0.11/0.40 Id : 97, {_}: double_divide (inverse ?168) (inverse identity) =>= ?168 [168] by Demod 90 with 4 at 1,2
% 0.11/0.40 Id : 98, {_}: double_divide (multiply ?170 ?171) (inverse identity) =>= double_divide ?171 ?170 [171, 170] by Super 97 with 16 at 1,2
% 0.11/0.40 Id : 226, {_}: double_divide (multiply ?170 ?171) identity =>= double_divide ?171 ?170 [171, 170] by Demod 98 with 219 at 2,2
% 0.11/0.40 Id : 251, {_}: inverse (multiply ?170 ?171) =>= double_divide ?171 ?170 [171, 170] by Demod 226 with 4 at 2
% 0.11/0.40 Id : 260, {_}: multiply (multiply identity ?354) identity =>= ?354 [354] by Super 239 with 219 at 1,1,2
% 0.11/0.40 Id : 272, {_}: multiply ?354 identity =>= ?354 [354] by Demod 260 with 248 at 1,2
% 0.11/0.40 Id : 288, {_}: inverse ?378 =<= double_divide identity ?378 [378] by Super 251 with 272 at 1,2
% 0.11/0.40 Id : 308, {_}: multiply (double_divide (double_divide ?395 (inverse ?396)) (inverse ?396)) identity =>= ?395 [396, 395] by Super 245 with 288 at 2,1,1,2
% 0.11/0.40 Id : 442, {_}: double_divide (double_divide ?482 (inverse ?483)) (inverse ?483) =>= ?482 [483, 482] by Demod 308 with 272 at 2
% 0.11/0.40 Id : 443, {_}: double_divide (double_divide ?485 (inverse (inverse ?486))) ?486 =>= ?485 [486, 485] by Super 442 with 246 at 2,2
% 0.11/0.40 Id : 457, {_}: double_divide (double_divide ?485 ?486) ?486 =>= ?485 [486, 485] by Demod 443 with 246 at 2,1,2
% 0.11/0.40 Id : 481, {_}: multiply ?533 (double_divide ?534 ?533) =>= inverse ?534 [534, 533] by Super 16 with 457 at 1,3
% 0.11/0.40 Id : 554, {_}: multiply (inverse ?635) ?636 =<= double_divide ?635 (inverse ?636) [636, 635] by Super 239 with 481 at 1,2
% 0.11/0.40 Id : 593, {_}: multiply (inverse ?677) (inverse ?678) =>= double_divide ?677 ?678 [678, 677] by Super 554 with 246 at 2,3
% 0.11/0.40 Id : 598, {_}: multiply ?693 (inverse ?694) =<= double_divide (inverse ?693) ?694 [694, 693] by Super 593 with 246 at 1,2
% 0.11/0.40 Id : 624, {_}: double_divide ?134 (multiply ?135 (inverse ?134)) =>= inverse ?135 [135, 134] by Demod 253 with 598 at 2,2
% 0.11/0.40 Id : 635, {_}: multiply ?737 (inverse (multiply ?738 (inverse (inverse ?737)))) =>= inverse ?738 [738, 737] by Super 624 with 598 at 2
% 0.11/0.40 Id : 645, {_}: multiply ?737 (double_divide (inverse (inverse ?737)) ?738) =>= inverse ?738 [738, 737] by Demod 635 with 251 at 2,2
% 0.11/0.40 Id : 646, {_}: multiply ?737 (multiply (inverse ?737) (inverse ?738)) =>= inverse ?738 [738, 737] by Demod 645 with 598 at 2,2
% 0.11/0.40 Id : 555, {_}: multiply (inverse ?638) (inverse ?639) =>= double_divide ?638 ?639 [639, 638] by Super 554 with 246 at 2,3
% 0.11/0.40 Id : 647, {_}: multiply ?737 (double_divide ?737 ?738) =>= inverse ?738 [738, 737] by Demod 646 with 555 at 2,2
% 0.11/0.40 Id : 590, {_}: multiply (double_divide ?669 ?670) ?669 =>= inverse ?670 [670, 669] by Super 239 with 555 at 1,2
% 0.11/0.40 Id : 668, {_}: inverse (inverse ?770) =<= double_divide ?771 (double_divide ?771 ?770) [771, 770] by Super 251 with 590 at 1,2
% 0.11/0.40 Id : 692, {_}: ?770 =<= double_divide ?771 (double_divide ?771 ?770) [771, 770] by Demod 668 with 246 at 2
% 0.11/0.40 Id : 751, {_}: multiply ?888 ?889 =<= inverse (double_divide ?888 ?889) [889, 888] by Super 647 with 692 at 2,2
% 0.11/0.40 Id : 764, {_}: multiply ?888 ?889 =?= multiply ?889 ?888 [889, 888] by Demod 751 with 16 at 3
% 0.11/0.40 Id : 2454, {_}: multiply a b === multiply a b [] by Demod 1 with 764 at 3
% 0.11/0.40 Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.11/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.40 24698: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.07611 using nrkbo
%------------------------------------------------------------------------------