%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP574-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n016.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.18s 0.35s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP574-1 : TPTP v8.1.0. Released v2.6.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n016.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 05:35:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 31238: Facts:
% 0.12/0.34 31238: Id : 2, {_}:
% 0.12/0.34 double_divide
% 0.12/0.34 (double_divide ?2
% 0.12/0.34 (double_divide (double_divide ?3 (double_divide ?4 ?2))
% 0.12/0.34 (double_divide ?4 identity))) (double_divide identity identity)
% 0.12/0.34 =>=
% 0.12/0.34 ?3
% 0.12/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.34 31238: 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 31238: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.34 31238: Id : 5, {_}:
% 0.12/0.34 identity =<= double_divide ?11 (inverse ?11)
% 0.12/0.34 [11] by identity ?11
% 0.12/0.34 31238: Goal:
% 0.12/0.34 31238: Id : 1, {_}: multiply identity a2 =>= a2 [] by prove_these_axioms_2
% 0.18/0.35 Statistics :
% 0.18/0.35 Max weight : 20
% 0.18/0.35 Found proof, 0.018143s
% 0.18/0.35 % SZS status Unsatisfiable for theBenchmark.p
% 0.18/0.35 % SZS output start CNFRefutation for theBenchmark.p
% 0.18/0.35 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 0.18/0.35 Id : 2, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?4 ?2)) (double_divide ?4 identity))) (double_divide identity identity) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.18/0.35 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.18/0.35 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 0.18/0.35 Id : 17, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 0.18/0.35 Id : 20, {_}: multiply identity ?50 =>= inverse (inverse ?50) [50] by Super 17 with 4 at 1,3
% 0.18/0.36 Id : 18, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?4 ?2)) (inverse ?4))) (double_divide identity identity) =>= ?3 [4, 3, 2] by Demod 2 with 4 at 2,2,1,2
% 0.18/0.36 Id : 19, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?4 ?2)) (inverse ?4))) (inverse identity) =>= ?3 [4, 3, 2] by Demod 18 with 4 at 2,2
% 0.18/0.36 Id : 24, {_}: double_divide (double_divide (inverse ?59) (double_divide (double_divide ?60 identity) (inverse ?59))) (inverse identity) =>= ?60 [60, 59] by Super 19 with 5 at 2,1,2,1,2
% 0.18/0.36 Id : 93, {_}: double_divide (double_divide (inverse ?144) (double_divide (inverse ?145) (inverse ?144))) (inverse identity) =>= ?145 [145, 144] by Demod 24 with 4 at 1,2,1,2
% 0.18/0.36 Id : 96, {_}: double_divide (double_divide (inverse (inverse ?155)) identity) (inverse identity) =>= ?155 [155] by Super 93 with 5 at 2,1,2
% 0.18/0.36 Id : 101, {_}: double_divide (inverse (inverse (inverse ?155))) (inverse identity) =>= ?155 [155] by Demod 96 with 4 at 1,2
% 0.18/0.36 Id : 29, {_}: double_divide (double_divide (inverse ?59) (double_divide (inverse ?60) (inverse ?59))) (inverse identity) =>= ?60 [60, 59] by Demod 24 with 4 at 1,2,1,2
% 0.18/0.36 Id : 131, {_}: double_divide (double_divide (inverse identity) ?208) (inverse identity) =>= inverse (inverse ?208) [208] by Super 29 with 101 at 2,1,2
% 0.18/0.36 Id : 133, {_}: double_divide identity (inverse identity) =<= inverse (inverse (inverse (inverse identity))) [] by Super 131 with 5 at 1,2
% 0.18/0.36 Id : 143, {_}: identity =<= inverse (inverse (inverse (inverse identity))) [] by Demod 133 with 5 at 2
% 0.18/0.36 Id : 158, {_}: double_divide identity (inverse identity) =>= inverse identity [] by Super 101 with 143 at 1,2
% 0.18/0.36 Id : 161, {_}: identity =<= inverse identity [] by Demod 158 with 5 at 2
% 0.18/0.36 Id : 181, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?4 ?2)) (inverse ?4))) identity =>= ?3 [4, 3, 2] by Demod 19 with 161 at 2,2
% 0.18/0.36 Id : 190, {_}: inverse (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?4 ?2)) (inverse ?4))) =>= ?3 [4, 3, 2] by Demod 181 with 4 at 2
% 0.18/0.36 Id : 191, {_}: multiply (double_divide (double_divide ?3 (double_divide ?4 ?2)) (inverse ?4)) ?2 =>= ?3 [2, 4, 3] by Demod 190 with 17 at 2
% 0.18/0.36 Id : 109, {_}: double_divide (inverse (inverse (inverse ?174))) (inverse identity) =>= ?174 [174] by Demod 96 with 4 at 1,2
% 0.18/0.36 Id : 110, {_}: double_divide (inverse (inverse (multiply ?176 ?177))) (inverse identity) =>= double_divide ?177 ?176 [177, 176] by Super 109 with 17 at 1,1,1,2
% 0.18/0.36 Id : 310, {_}: double_divide (inverse (inverse (multiply ?176 ?177))) identity =>= double_divide ?177 ?176 [177, 176] by Demod 110 with 161 at 2,2
% 0.18/0.36 Id : 321, {_}: inverse (inverse (inverse (multiply ?315 ?316))) =>= double_divide ?316 ?315 [316, 315] by Demod 310 with 4 at 2
% 0.18/0.36 Id : 108, {_}: double_divide (double_divide (inverse identity) ?172) (inverse identity) =>= inverse (inverse ?172) [172] by Super 29 with 101 at 2,1,2
% 0.18/0.36 Id : 185, {_}: double_divide (double_divide identity ?172) (inverse identity) =>= inverse (inverse ?172) [172] by Demod 108 with 161 at 1,1,2
% 0.18/0.36 Id : 186, {_}: double_divide (double_divide identity ?172) identity =>= inverse (inverse ?172) [172] by Demod 185 with 161 at 2,2
% 0.18/0.36 Id : 187, {_}: inverse (double_divide identity ?172) =>= inverse (inverse ?172) [172] by Demod 186 with 4 at 2
% 0.18/0.36 Id : 188, {_}: multiply ?172 identity =>= inverse (inverse ?172) [172] by Demod 187 with 17 at 2
% 0.18/0.36 Id : 325, {_}: inverse (inverse (inverse (inverse (inverse ?325)))) =>= double_divide identity ?325 [325] by Super 321 with 188 at 1,1,1,2
% 0.18/0.36 Id : 184, {_}: double_divide (inverse (inverse (inverse ?155))) identity =>= ?155 [155] by Demod 101 with 161 at 2,2
% 0.18/0.36 Id : 189, {_}: inverse (inverse (inverse (inverse ?155))) =>= ?155 [155] by Demod 184 with 4 at 2
% 0.18/0.36 Id : 345, {_}: inverse ?325 =<= double_divide identity ?325 [325] by Demod 325 with 189 at 2
% 0.18/0.36 Id : 352, {_}: multiply (double_divide (double_divide ?339 (inverse ?340)) (inverse identity)) ?340 =>= ?339 [340, 339] by Super 191 with 345 at 2,1,1,2
% 0.18/0.36 Id : 370, {_}: multiply (double_divide (double_divide ?339 (inverse ?340)) identity) ?340 =>= ?339 [340, 339] by Demod 352 with 161 at 2,1,2
% 0.18/0.36 Id : 371, {_}: multiply (inverse (double_divide ?339 (inverse ?340))) ?340 =>= ?339 [340, 339] by Demod 370 with 4 at 1,2
% 0.18/0.36 Id : 383, {_}: multiply (multiply (inverse ?370) ?371) ?370 =>= ?371 [371, 370] by Demod 371 with 17 at 1,2
% 0.18/0.36 Id : 25, {_}: multiply (inverse ?62) ?62 =>= inverse identity [62] by Super 17 with 5 at 1,3
% 0.18/0.36 Id : 182, {_}: multiply (inverse ?62) ?62 =>= identity [62] by Demod 25 with 161 at 3
% 0.18/0.36 Id : 388, {_}: multiply identity ?386 =>= ?386 [386] by Super 383 with 182 at 1,2
% 0.18/0.36 Id : 398, {_}: inverse (inverse ?386) =>= ?386 [386] by Demod 388 with 20 at 2
% 0.18/0.36 Id : 406, {_}: multiply identity ?50 =>= ?50 [50] by Demod 20 with 398 at 3
% 0.18/0.36 Id : 426, {_}: a2 === a2 [] by Demod 1 with 406 at 2
% 0.18/0.36 Id : 1, {_}: multiply identity a2 =>= a2 [] by prove_these_axioms_2
% 0.18/0.36 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.36 31241: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.020787 using nrkbo
%------------------------------------------------------------------------------