%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP062-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:30:28 PM UTC 2026
% Result : Unsatisfiable 55.47s 8.86s
% Output : CNFRefutation 55.47s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(reorient_equations,[],[f2]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
( ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 ) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(X4,inverse(X4)),X2)))) = X3,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,multiply(X3,X5)))),
inference(superposition,[status(thm)],[c_102,c_102]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))) = iPr_def_10(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_130]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,iPr_def_10(X0,X1,X2)))),multiply(multiply(X5,inverse(X5)),X4)))) = multiply(X6,inverse(X6)),
inference(superposition,[status(thm)],[c_131,c_102]) ).
tcf(c_156,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = iPr_def_11,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_149]) ).
tcf(c_2782,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1))))))) = X2,
inference(demodulation,[status(thm)],[c_51,c_156]) ).
tcf(c_2784,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))))) = X1,
inference(superposition,[status(thm)],[c_156,c_2782]) ).
tcf(c_2786,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,multiply(X2,X0)))),multiply(iPr_def_11,X1)))) = X2,
inference(superposition,[status(thm)],[c_2782,c_2782]) ).
tcf(c_2790,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))),X1) = iPr_def_11,
inference(superposition,[status(thm)],[c_2784,c_156]) ).
tcf(c_2792,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1)))))),multiply(X2,multiply(iPr_def_11,inverse(multiply(X3,iPr_def_11))))),X3) = iPr_def_11,
inference(superposition,[status(thm)],[c_2782,c_2790]) ).
tcf(c_2798,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(iPr_def_11,iPr_def_11))))) = inverse(multiply(X1,multiply(inverse(X1),multiply(iPr_def_11,inverse(iPr_def_11))))),
inference(superposition,[status(thm)],[c_2790,c_2784]) ).
tcf(c_2799,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(iPr_def_11,iPr_def_11))))) = inverse(multiply(X1,multiply(inverse(X1),iPr_def_11))),
inference(demodulation,[status(thm)],[c_2798,c_156]) ).
tcf(c_2800,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),iPr_def_11))) = iPr_def_15,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_2799]) ).
tcf(c_2804,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1)))))),multiply(X2,iPr_def_11))) = iPr_def_15,
inference(superposition,[status(thm)],[c_2782,c_2800]) ).
tcf(c_2806,plain,
! [X0: $i] : inverse(multiply(multiply(X0,multiply(inverse(X0),iPr_def_11)),multiply(iPr_def_15,iPr_def_11))) = iPr_def_15,
inference(superposition,[status(thm)],[c_2800,c_2800]) ).
tcf(c_2808,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,multiply(inverse(X0),iPr_def_11)),multiply(iPr_def_15,multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))),X1) = iPr_def_11,
inference(superposition,[status(thm)],[c_2800,c_2790]) ).
tcf(c_2810,plain,
! [X0: $i] : multiply(multiply(X0,multiply(inverse(X0),iPr_def_11)),iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_2800,c_156]) ).
tcf(c_2811,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = X0,
inference(superposition,[status(thm)],[c_2800,c_2782]) ).
tcf(c_2814,plain,
! [X0: $i] : multiply(multiply(multiply(X0,multiply(inverse(X0),iPr_def_11)),multiply(iPr_def_15,iPr_def_11)),iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_2800,c_2810]) ).
tcf(c_2816,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1)))))) = inverse(multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2782,c_2811]) ).
tcf(c_2817,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))) = inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2784,c_2811]) ).
tcf(c_2819,plain,
! [X0: $i] : inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(inverse(X0),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),
inference(superposition,[status(thm)],[c_2811,c_2811]) ).
tcf(c_2825,plain,
! [X0: $i] : multiply(multiply(inverse(X0),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),X0) = iPr_def_11,
inference(superposition,[status(thm)],[c_2811,c_156]) ).
tcf(c_2826,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_15),multiply(iPr_def_11,X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_2811,c_2782]) ).
tcf(c_2827,plain,
! [X0: $i] : multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),X0) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2825,c_2819]) ).
tcf(c_2832,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(X0,X1),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = inverse(multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(iPr_def_11))))),
inference(superposition,[status(thm)],[c_2827,c_2782]) ).
tcf(c_2834,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(iPr_def_11))))) = inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2827,c_2784]) ).
tcf(c_2841,plain,
inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2834,c_156,c_2800]) ).
tcf(c_2843,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(X0,X1),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = inverse(multiply(X0,multiply(X1,iPr_def_11))),
inference(demodulation,[status(thm)],[c_2832,c_156]) ).
tcf(c_2851,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(iPr_def_11)),multiply(iPr_def_11,inverse(multiply(multiply(X1,X0),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))))))) = X1,
inference(superposition,[status(thm)],[c_2827,c_2786]) ).
tcf(c_2854,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_15,multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),multiply(iPr_def_11,X0)))) = multiply(X1,multiply(inverse(X1),iPr_def_11)),
inference(superposition,[status(thm)],[c_2810,c_2786]) ).
tcf(c_2855,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))),multiply(iPr_def_11,X1)))) = inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2827,c_2786]) ).
tcf(c_2857,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,multiply(X2,X0)))),multiply(iPr_def_11,X1))) = inverse(multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2786,c_2811]) ).
tcf(c_2858,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,multiply(X2,X0)))),multiply(iPr_def_11,X1))),multiply(X2,iPr_def_11)),iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_2786,c_2810]) ).
tcf(c_2864,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(iPr_def_11,X0),multiply(multiply(iPr_def_11,X1),multiply(iPr_def_11,X2)))) = multiply(iPr_def_11,inverse(multiply(X0,multiply(X1,X2)))),
inference(superposition,[status(thm)],[c_2786,c_2786]) ).
tcf(c_2865,plain,
! [X0: $i] : multiply(X0,multiply(inverse(X0),iPr_def_11)) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_2854]) ).
tcf(c_2866,plain,
! [X0: $i] : inverse(multiply(iPr_def_15,multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),multiply(iPr_def_11,X0)))) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2854]) ).
tcf(c_2867,plain,
! [X0: $i] : inverse(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))))) = X0,
inference(demodulation,[status(thm)],[c_2851,c_156,c_2816,c_2843]) ).
tcf(c_2870,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X0,multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))),X1) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2792,c_2816]) ).
tcf(c_2881,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X0,multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))),multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,iPr_def_11)))))) = X2,
inference(superposition,[status(thm)],[c_2870,c_2782]) ).
tcf(c_2886,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X0,multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))) = inverse(multiply(X1,multiply(multiply(iPr_def_11,inverse(multiply(X2,iPr_def_11))),multiply(iPr_def_11,X2)))),
inference(superposition,[status(thm)],[c_2870,c_2786]) ).
tcf(c_2887,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(iPr_def_11)),multiply(iPr_def_11,multiply(inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X1,multiply(iPr_def_11,inverse(multiply(multiply(X2,X0),iPr_def_11))))))))) = X2,
inference(superposition,[status(thm)],[c_2870,c_2786]) ).
tcf(c_2899,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,multiply(inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X1,multiply(iPr_def_11,inverse(multiply(multiply(X2,X0),iPr_def_11))))))))) = X2,
inference(demodulation,[status(thm)],[c_2887,c_156]) ).
tcf(c_2900,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X0,multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))))) = inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(demodulation,[status(thm)],[c_2886,c_2855]) ).
tcf(c_2906,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X0,iPr_def_11))) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2804,c_2816]) ).
tcf(c_2911,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(iPr_def_11,iPr_def_11))))),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),iPr_def_11)) = iPr_def_15,
inference(superposition,[status(thm)],[c_2790,c_2906]) ).
tcf(c_2922,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(X0,multiply(multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(iPr_def_11,iPr_def_11)))),iPr_def_11))),iPr_def_11)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2911,c_2843]) ).
tcf(c_2926,plain,
inverse(multiply(iPr_def_16,multiply(iPr_def_15,iPr_def_11))) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2806,c_2865]) ).
tcf(c_2927,plain,
inverse(multiply(iPr_def_15,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(iPr_def_16,multiply(iPr_def_15,iPr_def_11)),
inference(superposition,[status(thm)],[c_2926,c_2811]) ).
tcf(c_2934,plain,
inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_15),multiply(iPr_def_11,iPr_def_16)))) = iPr_def_15,
inference(superposition,[status(thm)],[c_2926,c_2786]) ).
tcf(c_2935,plain,
inverse(iPr_def_16) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2934,c_2826]) ).
tcf(c_2936,plain,
! [X0: $i] : multiply(multiply(iPr_def_16,multiply(iPr_def_15,multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))))),X0) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2808,c_2865]) ).
tcf(c_2975,plain,
multiply(iPr_def_16,multiply(iPr_def_15,iPr_def_11)) = iPr_def_16,
inference(superposition,[status(thm)],[c_2935,c_2865]) ).
tcf(c_2980,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(inverse(X0),iPr_def_11),multiply(multiply(iPr_def_11,inverse(multiply(X1,iPr_def_16))),multiply(iPr_def_11,X1)))) = X0,
inference(superposition,[status(thm)],[c_2865,c_2786]) ).
tcf(c_2982,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(inverse(iPr_def_11),iPr_def_11),multiply(X1,X0)))),iPr_def_16))) = X1,
inference(superposition,[status(thm)],[c_2865,c_2786]) ).
tcf(c_2997,plain,
inverse(multiply(iPr_def_15,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),
inference(superposition,[status(thm)],[c_2841,c_2811]) ).
tcf(c_3000,plain,
! [X0: $i] : multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),multiply(iPr_def_15,multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))))),X0) = iPr_def_11,
inference(superposition,[status(thm)],[c_2841,c_2790]) ).
tcf(c_3003,plain,
inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_15),multiply(iPr_def_11,iPr_def_15)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_2841,c_2782]) ).
tcf(c_3007,plain,
multiply(iPr_def_15,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_2841,c_2827]) ).
tcf(c_3008,plain,
inverse(iPr_def_15) = iPr_def_11,
inference(demodulation,[status(thm)],[c_3003,c_2826]) ).
tcf(c_3010,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_2997,c_2927,c_2975]) ).
tcf(c_3018,plain,
multiply(multiply(iPr_def_16,iPr_def_11),iPr_def_15) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2814,c_2865,c_3007]) ).
tcf(c_3020,plain,
! [X0: $i] : inverse(multiply(iPr_def_15,multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),multiply(iPr_def_11,X0)))) = multiply(iPr_def_16,iPr_def_11),
inference(superposition,[status(thm)],[c_3018,c_2786]) ).
tcf(c_3021,plain,
multiply(iPr_def_16,iPr_def_11) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3020,c_2866]) ).
tcf(c_3026,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_15),multiply(iPr_def_11,X0))) = X0,
inference(superposition,[status(thm)],[c_2811,c_2816]) ).
tcf(c_3033,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(multiply(X0,X1),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(iPr_def_11)))),
inference(superposition,[status(thm)],[c_2827,c_2816]) ).
tcf(c_3034,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(X0,multiply(iPr_def_11,inverse(multiply(multiply(X1,X2),iPr_def_11))))),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(X1,multiply(X2,multiply(iPr_def_11,inverse(iPr_def_11)))),
inference(superposition,[status(thm)],[c_2870,c_2816]) ).
tcf(c_3036,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(iPr_def_16,multiply(iPr_def_15,multiply(iPr_def_11,inverse(multiply(multiply(X0,X1),iPr_def_11))))),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(iPr_def_11)))),
inference(superposition,[status(thm)],[c_2936,c_2816]) ).
tcf(c_3048,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1))))),multiply(iPr_def_11,inverse(multiply(X3,inverse(multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))))))))) = inverse(multiply(X3,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2816,c_2816]) ).
tcf(c_3049,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1))))),multiply(iPr_def_11,inverse(multiply(X3,inverse(multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))))))))) = X3,
inference(superposition,[status(thm)],[c_2816,c_2782]) ).
tcf(c_3054,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(iPr_def_11,inverse(multiply(X0,multiply(X1,X2)))),multiply(multiply(iPr_def_11,inverse(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))))),multiply(iPr_def_11,X1)))) = X2,
inference(superposition,[status(thm)],[c_2816,c_2786]) ).
tcf(c_3058,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))) = multiply(X0,multiply(X1,iPr_def_11)),
inference(demodulation,[status(thm)],[c_3033,c_156,c_2811]) ).
tcf(c_3059,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11,inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X1)))) = X2,
inference(demodulation,[status(thm)],[c_3054,c_2864,c_2867]) ).
tcf(c_3060,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_16,multiply(multiply(iPr_def_15,multiply(iPr_def_11,inverse(multiply(multiply(X0,X1),iPr_def_11)))),iPr_def_11))) = multiply(X0,multiply(X1,iPr_def_11)),
inference(demodulation,[status(thm)],[c_3036,c_156,c_2843]) ).
tcf(c_3062,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),multiply(multiply(X0,multiply(iPr_def_11,inverse(multiply(multiply(X1,X2),iPr_def_11)))),iPr_def_11))) = multiply(X1,multiply(X2,iPr_def_11)),
inference(demodulation,[status(thm)],[c_3034,c_156,c_2843]) ).
tcf(c_3063,plain,
! [X0: $i] : multiply(multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),iPr_def_11) = inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2827,c_2817]) ).
tcf(c_3073,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_11,multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))))) = inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_3008,c_2817]) ).
tcf(c_3078,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))),multiply(iPr_def_11,inverse(multiply(X2,inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))))))))) = inverse(multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2817,c_2816]) ).
tcf(c_3079,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))),multiply(iPr_def_11,inverse(multiply(X2,inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))))))))) = X2,
inference(superposition,[status(thm)],[c_2817,c_2782]) ).
tcf(c_3082,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))),multiply(multiply(iPr_def_11,inverse(multiply(X2,inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))))))),multiply(iPr_def_11,X2)))) = X0,
inference(superposition,[status(thm)],[c_2817,c_2786]) ).
tcf(c_3083,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),multiply(multiply(iPr_def_11,inverse(inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))))),multiply(iPr_def_11,X1)))) = inverse(X1),
inference(superposition,[status(thm)],[c_2817,c_2786]) ).
tcf(c_3086,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(inverse(iPr_def_11),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))),multiply(X2,X0)))),inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))))))) = X2,
inference(superposition,[status(thm)],[c_2817,c_2786]) ).
tcf(c_3087,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(multiply(X0,iPr_def_11)),iPr_def_11)),iPr_def_11) = inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(demodulation,[status(thm)],[c_3063,c_3058]) ).
tcf(c_3088,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11,inverse(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,X1)))) = inverse(X1),
inference(demodulation,[status(thm)],[c_3083,c_2864,c_2867]) ).
tcf(c_3093,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(X0,multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1)))))),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),
inference(superposition,[status(thm)],[c_2782,c_2819]) ).
tcf(c_3103,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)),multiply(iPr_def_11,inverse(multiply(X1,inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))))))))) = inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_2819,c_2816]) ).
tcf(c_3122,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(multiply(X1,multiply(iPr_def_11,inverse(multiply(X2,multiply(X0,X1))))),iPr_def_11))) = multiply(X2,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),
inference(demodulation,[status(thm)],[c_3093,c_2843]) ).
tcf(c_3152,plain,
inverse(multiply(inverse(multiply(iPr_def_16,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),iPr_def_16)) = iPr_def_15,
inference(superposition,[status(thm)],[c_3021,c_2906]) ).
tcf(c_3156,plain,
inverse(iPr_def_11) = iPr_def_15,
inference(demodulation,[status(thm)],[c_3152,c_2827]) ).
tcf(c_3168,plain,
multiply(iPr_def_11,iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_3156,c_156]) ).
tcf(c_3176,plain,
! [X0: $i] : inverse(multiply(iPr_def_15,multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),multiply(iPr_def_11,X0)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_3168,c_2786]) ).
tcf(c_3191,plain,
iPr_def_11 = iPr_def_16,
inference(demodulation,[status(thm)],[c_3176,c_2855,c_2927,c_2975]) ).
tcf(c_3194,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_3191,c_3021]) ).
tcf(c_3201,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))),multiply(iPr_def_11,X1)))) = inverse(multiply(X0,iPr_def_11)),
inference(demodulation,[status(thm)],[c_2855,c_3168,c_3194]) ).
tcf(c_3221,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))),multiply(iPr_def_11,X1))) = inverse(multiply(inverse(multiply(X0,iPr_def_11)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_3201,c_2811]) ).
tcf(c_3234,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))),multiply(iPr_def_11,X1))) = multiply(X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_3221,c_2811]) ).
tcf(c_3243,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(X1,multiply(X2,X0)))),multiply(iPr_def_11,X1))) = inverse(multiply(X2,iPr_def_11)),
inference(demodulation,[status(thm)],[c_2857,c_3168,c_3194]) ).
tcf(c_3248,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_15),multiply(iPr_def_11,X0))) = inverse(multiply(inverse(X0),iPr_def_11)),
inference(superposition,[status(thm)],[c_2800,c_3243]) ).
tcf(c_3252,plain,
multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_15),multiply(iPr_def_11,iPr_def_16))) = inverse(multiply(iPr_def_15,iPr_def_11)),
inference(superposition,[status(thm)],[c_2926,c_3243]) ).
tcf(c_3264,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11))),multiply(iPr_def_11,X1))) = inverse(multiply(X0,iPr_def_11)),
inference(superposition,[status(thm)],[c_156,c_3243]) ).
tcf(c_3293,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(iPr_def_11,inverse(multiply(X0,multiply(X1,X2)))),multiply(iPr_def_11,X0)),multiply(multiply(iPr_def_11,inverse(multiply(X3,inverse(multiply(X1,iPr_def_11))))),multiply(iPr_def_11,X3))) = inverse(multiply(X2,iPr_def_11)),
inference(superposition,[status(thm)],[c_3243,c_3243]) ).
tcf(c_3301,plain,
iPr_def_11 = iPr_def_15,
inference(demodulation,[status(thm)],[c_3252,c_3007,c_3026,c_3156,c_3191]) ).
tcf(c_3305,plain,
! [X0: $i] : inverse(multiply(inverse(X0),iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_3248,c_3026]) ).
tcf(c_3312,plain,
! [X0: $i] : inverse(multiply(X0,iPr_def_11)) = multiply(inverse(X0),iPr_def_11),
inference(demodulation,[status(thm)],[c_3264,c_3234]) ).
tcf(c_3335,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_11)),iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2858,c_3243,c_3301]) ).
tcf(c_3353,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_11)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(X1,multiply(inverse(X1),multiply(iPr_def_11,inverse(iPr_def_11)))),
inference(superposition,[status(thm)],[c_3335,c_2817]) ).
tcf(c_3370,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,iPr_def_11)),multiply(multiply(X0,iPr_def_11),iPr_def_11))) = multiply(X1,inverse(multiply(X1,iPr_def_11))),
inference(demodulation,[status(thm)],[c_3353,c_156,c_3058,c_3312]) ).
tcf(c_3371,plain,
! [X0: $i] : multiply(X0,inverse(multiply(X0,iPr_def_11))) = iPr_def_18,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_3370]) ).
tcf(c_3473,plain,
inverse(iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_3301,c_3008]) ).
tcf(c_3500,plain,
! [X0: $i] : multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(iPr_def_11)))) = inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_3194,c_2817]) ).
tcf(c_3515,plain,
iPr_def_11 = iPr_def_18,
inference(demodulation,[status(thm)],[c_3500,c_156,c_2841,c_3301,c_3312,c_3371]) ).
tcf(c_3517,plain,
inverse(iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_3515,c_3473]) ).
tcf(c_3525,plain,
multiply(iPr_def_15,iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_3515,c_3007]) ).
tcf(c_3529,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(iPr_def_18,inverse(multiply(X2,multiply(X0,X1)))))) = inverse(multiply(X2,multiply(iPr_def_18,multiply(iPr_def_18,iPr_def_15)))),
inference(superposition,[status(thm)],[c_3515,c_2816]) ).
tcf(c_3532,plain,
multiply(iPr_def_16,multiply(iPr_def_15,iPr_def_18)) = iPr_def_16,
inference(superposition,[status(thm)],[c_3515,c_2975]) ).
tcf(c_3546,plain,
multiply(iPr_def_18,iPr_def_18) = iPr_def_18,
inference(demodulation,[status(thm)],[c_3525,c_3301,c_3515]) ).
tcf(c_3549,plain,
multiply(iPr_def_18,multiply(iPr_def_18,iPr_def_18)) = iPr_def_18,
inference(demodulation,[status(thm)],[c_3532,c_3191,c_3301,c_3515]) ).
tcf(c_3564,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(iPr_def_18,inverse(multiply(X2,multiply(X0,X1)))))) = inverse(multiply(X2,multiply(iPr_def_18,multiply(iPr_def_18,iPr_def_18)))),
inference(demodulation,[status(thm)],[c_3529,c_3301,c_3515]) ).
tcf(c_3565,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,iPr_def_18)),multiply(X0,multiply(iPr_def_18,inverse(multiply(X1,iPr_def_18)))))) = X1,
inference(demodulation,[status(thm)],[c_2881,c_2900,c_3168,c_3515,c_3546]) ).
tcf(c_3590,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_18,inverse(multiply(X1,iPr_def_18))),multiply(iPr_def_11,X1))) = inverse(multiply(inverse(multiply(X0,iPr_def_18)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))),
inference(superposition,[status(thm)],[c_3565,c_2816]) ).
tcf(c_3606,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_18,inverse(multiply(X1,iPr_def_18))),multiply(iPr_def_18,X1))) = multiply(X0,iPr_def_18),
inference(demodulation,[status(thm)],[c_3590,c_2811,c_3515]) ).
tcf(c_3736,plain,
! [X0: $i] : inverse(inverse(multiply(X0,iPr_def_18))) = X0,
inference(demodulation,[status(thm)],[c_2899,c_2900,c_3058,c_3515,c_3549,c_3564]) ).
tcf(c_3775,plain,
! [X0: $i] : multiply(X0,multiply(multiply(inverse(X0),iPr_def_18),iPr_def_18)) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2922,c_3301,c_3305,c_3371,c_3515]) ).
tcf(c_3802,plain,
! [X0: $i] : inverse(multiply(iPr_def_18,multiply(multiply(iPr_def_11,inverse(iPr_def_18)),multiply(iPr_def_11,X0)))) = multiply(inverse(X0),iPr_def_18),
inference(superposition,[status(thm)],[c_3775,c_2786]) ).
tcf(c_3808,plain,
! [X0: $i] : inverse(multiply(iPr_def_18,multiply(iPr_def_18,multiply(iPr_def_18,X0)))) = multiply(inverse(X0),iPr_def_18),
inference(demodulation,[status(thm)],[c_3802,c_3515,c_3546,c_3517]) ).
tcf(c_3823,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(X0,iPr_def_18)),iPr_def_18)) = X0,
inference(demodulation,[status(thm)],[c_2980,c_3191,c_3312,c_3515,c_3606]) ).
tcf(c_3834,plain,
! [X0: $i] : inverse(multiply(multiply(inverse(multiply(X0,iPr_def_18)),iPr_def_18),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15))),
inference(superposition,[status(thm)],[c_3823,c_2819]) ).
tcf(c_3843,plain,
! [X0: $i] : inverse(multiply(X0,iPr_def_18)) = inverse(X0),
inference(superposition,[status(thm)],[c_3823,c_3736]) ).
tcf(c_3854,plain,
! [X0: $i] : multiply(X0,iPr_def_18) = X0,
inference(demodulation,[status(thm)],[c_3834,c_3058,c_3168,c_3515,c_3546,c_3823]) ).
tcf(c_3856,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(iPr_def_18,inverse(multiply(iPr_def_18,multiply(X1,X0)))))) = X1,
inference(demodulation,[status(thm)],[c_2982,c_3191,c_3194,c_3312,c_3515,c_3517,c_3854]) ).
tcf(c_3860,plain,
! [X0: $i] : inverse(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_18,inverse(multiply(iPr_def_18,iPr_def_11))))) = multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),
inference(superposition,[status(thm)],[c_3201,c_3856]) ).
tcf(c_3868,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(iPr_def_18,inverse(multiply(iPr_def_18,iPr_def_11))))) = X0,
inference(superposition,[status(thm)],[c_156,c_3856]) ).
tcf(c_3908,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_3868,c_3371,c_3854]) ).
tcf(c_3922,plain,
! [X0: $i] : inverse(multiply(iPr_def_18,X0)) = multiply(iPr_def_18,inverse(X0)),
inference(demodulation,[status(thm)],[c_3860,c_3371,c_3515,c_3854]) ).
tcf(c_3987,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_18,
inference(demodulation,[status(thm)],[c_3000,c_3010,c_3191,c_3301,c_3515,c_3808,c_3854,c_3922]) ).
tcf(c_4027,plain,
! [X0: $i] : inverse(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))) = multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),iPr_def_18),
inference(superposition,[status(thm)],[c_3987,c_2817]) ).
tcf(c_4029,plain,
! [X0: $i] : inverse(multiply(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),iPr_def_18)) = X0,
inference(superposition,[status(thm)],[c_3987,c_2784]) ).
tcf(c_4050,plain,
! [X0: $i] : multiply(iPr_def_18,X0) = X0,
inference(demodulation,[status(thm)],[c_4029,c_3515,c_3843,c_3854,c_3908,c_3922]) ).
tcf(c_4056,plain,
! [X0: $i] : inverse(multiply(iPr_def_18,X0)) = inverse(X0),
inference(demodulation,[status(thm)],[c_4027,c_3168,c_3515,c_3546,c_3854,c_3922]) ).
tcf(c_4070,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_18,multiply(multiply(iPr_def_11,inverse(multiply(X0,X1))),multiply(iPr_def_11,X0))) = inverse(multiply(X1,iPr_def_11)),
inference(superposition,[status(thm)],[c_3854,c_3243]) ).
tcf(c_4072,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(iPr_def_18,multiply(X1,X0)))),iPr_def_11)) = inverse(multiply(X1,iPr_def_11)),
inference(superposition,[status(thm)],[c_3854,c_3243]) ).
tcf(c_4098,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(demodulation,[status(thm)],[c_4072,c_3515,c_3854,c_3922,c_4056]) ).
tcf(c_4099,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(demodulation,[status(thm)],[c_4070,c_3515,c_3854,c_3922,c_4050,c_4056]) ).
tcf(c_4118,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,iPr_def_18)),multiply(X0,multiply(iPr_def_18,inverse(multiply(X1,iPr_def_18))))) = inverse(X1),
inference(superposition,[status(thm)],[c_3565,c_3908]) ).
tcf(c_4140,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,inverse(X1))) = inverse(X1),
inference(demodulation,[status(thm)],[c_4118,c_3843,c_3922,c_4056]) ).
tcf(c_4237,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(X1,inverse(multiply(X2,multiply(X0,X1)))),inverse(multiply(X3,inverse(X2))))) = inverse(X3),
inference(demodulation,[status(thm)],[c_3048,c_3168,c_3515,c_3546,c_3854,c_3922,c_4056]) ).
tcf(c_4337,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(multiply(iPr_def_11,inverse(inverse(X0))),multiply(iPr_def_11,X2))) = inverse(multiply(multiply(X3,inverse(multiply(X1,multiply(X2,X3)))),iPr_def_11)),
inference(superposition,[status(thm)],[c_4237,c_3243]) ).
tcf(c_4338,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(multiply(iPr_def_11,inverse(inverse(X0))),multiply(iPr_def_11,X2)))) = multiply(X3,inverse(multiply(X1,multiply(X2,X3)))),
inference(superposition,[status(thm)],[c_4237,c_2786]) ).
tcf(c_4363,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2))) = multiply(X3,inverse(multiply(X1,multiply(X2,X3)))),
inference(demodulation,[status(thm)],[c_4338,c_3515,c_3908,c_4050]) ).
tcf(c_4364,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(multiply(X1,multiply(X2,X0)))) = iPr_def_19(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_4363]) ).
tcf(c_4365,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2))) = iPr_def_19(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_4363]) ).
tcf(c_4368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,inverse(multiply(X1,multiply(X2,X0))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,X2)),
inference(demodulation,[status(thm)],[c_4337,c_3515,c_3854,c_3908,c_4050]) ).
tcf(c_4370,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)) = iPr_def_20(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_4368]) ).
tcf(c_4394,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(iPr_def_19(X1,X0),inverse(multiply(X2,inverse(X1)))))) = X2,
inference(demodulation,[status(thm)],[c_3049,c_3168,c_3515,c_3546,c_3854,c_3922,c_4056,c_4364]) ).
tcf(c_4447,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X2))) = inverse(multiply(iPr_def_19(X1,X2),iPr_def_11)),
inference(superposition,[status(thm)],[c_4394,c_3243]) ).
tcf(c_4448,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X2)))) = iPr_def_19(X1,X2),
inference(superposition,[status(thm)],[c_4394,c_2786]) ).
tcf(c_4449,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(iPr_def_18,X0))) = iPr_def_19(X1,iPr_def_18),
inference(superposition,[status(thm)],[c_4394,c_3856]) ).
tcf(c_4461,plain,
! [X0: $i] : iPr_def_19(X0,iPr_def_18) = inverse(X0),
inference(demodulation,[status(thm)],[c_4449,c_3908,c_4050,c_4099]) ).
tcf(c_4468,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_20(X0,X1)) = iPr_def_19(X0,X1),
inference(demodulation,[status(thm)],[c_4448,c_3515,c_4050,c_4370]) ).
tcf(c_4476,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_19(X0,X1)) = iPr_def_20(X0,X1),
inference(demodulation,[status(thm)],[c_4447,c_3515,c_3854,c_4050,c_4370]) ).
tcf(c_4501,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X1))) = X2,
inference(demodulation,[status(thm)],[c_3059,c_3515,c_3922,c_4050]) ).
tcf(c_4540,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_15)))))),multiply(X0,X2))) = multiply(inverse(X2),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))),
inference(superposition,[status(thm)],[c_2817,c_4501]) ).
tcf(c_4541,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,iPr_def_11)))),multiply(X0,X2))) = multiply(multiply(iPr_def_11,inverse(multiply(X3,multiply(X1,X2)))),multiply(iPr_def_11,X3)),
inference(superposition,[status(thm)],[c_3243,c_4501]) ).
tcf(c_4652,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,X1)) = iPr_def_19(X0,X1),
inference(demodulation,[status(thm)],[c_4541,c_3515,c_3854,c_3922,c_4050,c_4099,c_4365]) ).
tcf(c_4654,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(X1)) = iPr_def_19(X1,X0),
inference(demodulation,[status(thm)],[c_4540,c_3168,c_3515,c_3546,c_3854,c_4098,c_4365]) ).
tcf(c_4661,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_18,iPr_def_19(X0,X1)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_3060,c_3191,c_3301,c_3515,c_3854,c_4050,c_4098,c_4652]) ).
tcf(c_4662,plain,
! [X0: $i] : iPr_def_19(iPr_def_18,inverse(X0)) = multiply(X0,iPr_def_18),
inference(superposition,[status(thm)],[c_4461,c_4661]) ).
tcf(c_4665,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_18,iPr_def_19(X0,X1)) = iPr_def_19(iPr_def_18,multiply(X0,X1)),
inference(superposition,[status(thm)],[c_4661,c_4661]) ).
tcf(c_4666,plain,
! [X0: $i] : iPr_def_19(iPr_def_18,inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_4662,c_3854]) ).
tcf(c_4667,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_18,multiply(X0,X1)) = iPr_def_19(X0,X1),
inference(demodulation,[status(thm)],[c_4665,c_4050]) ).
tcf(c_4669,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_19(inverse(X0),multiply(X0,iPr_def_19(X1,X2))) = multiply(X1,X2),
inference(demodulation,[status(thm)],[c_3062,c_3168,c_3515,c_3546,c_3854,c_4098,c_4461,c_4652]) ).
tcf(c_4696,plain,
! [X0: $i,X1: $i] : iPr_def_19(inverse(multiply(iPr_def_16,multiply(iPr_def_15,multiply(iPr_def_11,inverse(multiply(iPr_def_19(X0,X1),iPr_def_11)))))),iPr_def_11) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_2936,c_4669]) ).
tcf(c_4700,plain,
! [X0: $i,X1: $i] : iPr_def_19(inverse(inverse(iPr_def_19(X0,X1))),iPr_def_18) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3987,c_4669]) ).
tcf(c_4708,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = iPr_def_20(X0,X1),
inference(demodulation,[status(thm)],[c_4700,c_3908,c_4461,c_4476]) ).
tcf(c_4716,plain,
! [X0: $i,X1: $i] : iPr_def_20(iPr_def_18,iPr_def_20(X0,X1)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_4696,c_3191,c_3301,c_3515,c_4050,c_4098,c_4461,c_4476,c_4652]) ).
tcf(c_4728,plain,
! [X0: $i] : iPr_def_19(X0,iPr_def_20(iPr_def_18,iPr_def_18)) = iPr_def_19(iPr_def_18,X0),
inference(demodulation,[status(thm)],[c_3073,c_3168,c_3301,c_3515,c_3922,c_4098,c_4652,c_4708,c_4716]) ).
tcf(c_4735,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_20(X0,iPr_def_20(iPr_def_20(inverse(X0),inverse(X1)),iPr_def_20(iPr_def_18,iPr_def_19(X2,iPr_def_19(iPr_def_18,X1))))) = iPr_def_19(iPr_def_18,X2),
inference(demodulation,[status(thm)],[c_3078,c_3168,c_3515,c_4098,c_4652,c_4708,c_4728]) ).
tcf(c_4835,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_19(X0,iPr_def_20(iPr_def_20(inverse(X0),inverse(X1)),iPr_def_20(iPr_def_18,iPr_def_19(X2,iPr_def_19(iPr_def_18,X1))))) = X2,
inference(demodulation,[status(thm)],[c_3079,c_3168,c_3515,c_4098,c_4652,c_4708,c_4728]) ).
tcf(c_4887,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,iPr_def_20(iPr_def_20(inverse(X0),inverse(X1)),iPr_def_20(iPr_def_18,iPr_def_19(X2,iPr_def_19(iPr_def_18,X1))))) = iPr_def_19(inverse(X3),multiply(X3,X2)),
inference(superposition,[status(thm)],[c_4835,c_4669]) ).
tcf(c_4909,plain,
! [X0: $i,X1: $i] : iPr_def_19(inverse(X0),iPr_def_20(X0,X1)) = iPr_def_19(iPr_def_18,X1),
inference(demodulation,[status(thm)],[c_4887,c_4708,c_4735]) ).
tcf(c_4934,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_19(iPr_def_20(inverse(X0),inverse(X1)),iPr_def_20(iPr_def_20(iPr_def_18,iPr_def_19(X2,iPr_def_19(iPr_def_18,X1))),iPr_def_20(iPr_def_18,X2))) = X0,
inference(demodulation,[status(thm)],[c_3082,c_3168,c_3515,c_4098,c_4652,c_4708,c_4728]) ).
tcf(c_5042,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_19(X0,iPr_def_20(iPr_def_20(iPr_def_18,iPr_def_19(inverse(X1),iPr_def_20(X2,X0))),iPr_def_19(iPr_def_18,X1))) = X2,
inference(demodulation,[status(thm)],[c_3086,c_3168,c_3515,c_4140,c_4461,c_4652,c_4708,c_4728]) ).
tcf(c_5119,plain,
! [X0: $i] : iPr_def_20(iPr_def_20(iPr_def_18,inverse(X0)),iPr_def_18) = iPr_def_19(iPr_def_18,X0),
inference(demodulation,[status(thm)],[c_3087,c_3168,c_3312,c_3515,c_4461,c_4468,c_4652,c_4708,c_4728]) ).
tcf(c_5121,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_18,multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))))) = iPr_def_20(iPr_def_20(iPr_def_18,X1),iPr_def_18),
inference(superposition,[status(thm)],[c_2784,c_5119]) ).
tcf(c_5125,plain,
! [X0: $i] : iPr_def_20(iPr_def_20(iPr_def_18,X0),iPr_def_18) = iPr_def_19(iPr_def_18,inverse(X0)),
inference(superposition,[status(thm)],[c_3908,c_5119]) ).
tcf(c_5140,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_18,multiply(X0,multiply(iPr_def_18,inverse(multiply(iPr_def_18,multiply(X1,X0)))))) = iPr_def_20(iPr_def_20(iPr_def_18,X1),iPr_def_18),
inference(superposition,[status(thm)],[c_3856,c_5119]) ).
tcf(c_5150,plain,
! [X0: $i] : iPr_def_20(iPr_def_20(iPr_def_18,X0),iPr_def_18) = X0,
inference(demodulation,[status(thm)],[c_5125,c_4666]) ).
tcf(c_5158,plain,
! [X0: $i,X1: $i] : iPr_def_19(X0,iPr_def_19(X1,X0)) = iPr_def_20(iPr_def_20(iPr_def_18,X1),iPr_def_18),
inference(demodulation,[status(thm)],[c_5140,c_3922,c_4652,c_4667]) ).
tcf(c_5161,plain,
! [X0: $i,X1: $i] : iPr_def_19(X0,iPr_def_20(inverse(X0),inverse(X1))) = iPr_def_20(iPr_def_20(iPr_def_18,X1),iPr_def_18),
inference(demodulation,[status(thm)],[c_5121,c_4098,c_4667,c_4708]) ).
tcf(c_5167,plain,
! [X0: $i] : iPr_def_20(iPr_def_18,iPr_def_19(iPr_def_18,X0)) = inverse(X0),
inference(demodulation,[status(thm)],[c_3088,c_3515,c_4461,c_4652,c_4708,c_4909]) ).
tcf(c_5168,plain,
iPr_def_20(iPr_def_18,inverse(iPr_def_18)) = inverse(iPr_def_18),
inference(superposition,[status(thm)],[c_4461,c_5167]) ).
tcf(c_5172,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_20(iPr_def_20(iPr_def_18,iPr_def_19(inverse(X0),iPr_def_20(X1,iPr_def_18))),iPr_def_19(iPr_def_18,X0))) = iPr_def_20(iPr_def_18,X1),
inference(superposition,[status(thm)],[c_5042,c_5167]) ).
tcf(c_5178,plain,
iPr_def_20(iPr_def_18,iPr_def_18) = iPr_def_18,
inference(demodulation,[status(thm)],[c_5168,c_3517]) ).
tcf(c_5180,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_20(iPr_def_18,iPr_def_19(inverse(X0),iPr_def_20(X1,iPr_def_18))),iPr_def_19(iPr_def_18,X0)) = iPr_def_20(iPr_def_18,X1),
inference(demodulation,[status(thm)],[c_5172,c_4468]) ).
tcf(c_5182,plain,
! [X0: $i] : iPr_def_19(X0,iPr_def_18) = iPr_def_19(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_5178,c_4728]) ).
tcf(c_5185,plain,
! [X0: $i] : iPr_def_19(iPr_def_18,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_5182,c_4461]) ).
tcf(c_5236,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),inverse(multiply(X1,inverse(iPr_def_18)))))) = X1,
inference(superposition,[status(thm)],[c_5185,c_4394]) ).
tcf(c_5250,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_20(iPr_def_20(iPr_def_18,iPr_def_19(inverse(X0),iPr_def_20(X1,iPr_def_18))),iPr_def_19(iPr_def_18,X0))) = X1,
inference(superposition,[status(thm)],[c_5185,c_5042]) ).
tcf(c_5251,plain,
! [X0: $i] : iPr_def_20(X0,iPr_def_18) = X0,
inference(demodulation,[status(thm)],[c_5236,c_3517,c_4652,c_4654,c_4708,c_5150,c_5158]) ).
tcf(c_5252,plain,
! [X0: $i] : iPr_def_20(iPr_def_18,X0) = X0,
inference(demodulation,[status(thm)],[c_5250,c_4468,c_5180]) ).
tcf(c_5256,plain,
! [X0: $i,X1: $i] : iPr_def_20(inverse(X0),iPr_def_19(X1,inverse(X0))) = inverse(X1),
inference(demodulation,[status(thm)],[c_3103,c_3168,c_3515,c_4461,c_4652,c_4708,c_5178,c_5252]) ).
tcf(c_5280,plain,
! [X0: $i] : iPr_def_20(inverse(X0),inverse(inverse(X0))) = inverse(iPr_def_18),
inference(superposition,[status(thm)],[c_5185,c_5256]) ).
tcf(c_5306,plain,
! [X0: $i] : iPr_def_20(inverse(X0),X0) = iPr_def_18,
inference(demodulation,[status(thm)],[c_5280,c_3517,c_3908]) ).
tcf(c_5308,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_19(X0,iPr_def_20(X1,iPr_def_19(X2,iPr_def_20(X0,X1)))) = X2,
inference(demodulation,[status(thm)],[c_3122,c_3168,c_3515,c_4652,c_4708,c_5178,c_5251,c_5252]) ).
tcf(c_5408,plain,
! [X0: $i] : iPr_def_20(X0,inverse(X0)) = iPr_def_18,
inference(superposition,[status(thm)],[c_3908,c_5306]) ).
tcf(c_5470,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_18,iPr_def_20(iPr_def_20(iPr_def_18,iPr_def_19(X0,iPr_def_19(iPr_def_18,inverse(X1)))),iPr_def_20(iPr_def_18,X0))) = X1,
inference(superposition,[status(thm)],[c_5408,c_4934]) ).
tcf(c_5476,plain,
! [X0: $i,X1: $i] : iPr_def_19(iPr_def_19(X0,X1),X0) = X1,
inference(demodulation,[status(thm)],[c_5470,c_3908,c_4468,c_5185,c_5252]) ).
tcf(c_5696,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_20(iPr_def_20(iPr_def_18,iPr_def_19(X0,iPr_def_19(iPr_def_18,X1))),iPr_def_20(iPr_def_18,X0)) = iPr_def_19(X2,iPr_def_20(inverse(X2),inverse(X1))),
inference(superposition,[status(thm)],[c_4934,c_5476]) ).
tcf(c_5717,plain,
! [X0: $i,X1: $i] : iPr_def_20(iPr_def_19(X0,inverse(X1)),X0) = X1,
inference(demodulation,[status(thm)],[c_5696,c_5161,c_5185,c_5251,c_5252]) ).
tcf(c_5844,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_20(iPr_def_20(iPr_def_19(X0,iPr_def_20(X1,X2)),X0),X1) = inverse(X2),
inference(demodulation,[status(thm)],[c_3293,c_3515,c_4461,c_4652,c_4708,c_5252,c_5717]) ).
tcf(c_5853,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_19(X0,iPr_def_20(X1,X2))) = iPr_def_20(iPr_def_20(X0,X1),X2),
inference(superposition,[status(thm)],[c_5308,c_5844]) ).
tcf(c_5878,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_20(iPr_def_20(X0,X1),X2) = iPr_def_20(X0,iPr_def_20(X1,X2)),
inference(demodulation,[status(thm)],[c_5853,c_4476]) ).
tcf(c_17238,plain,
( ( iPr_def_18 != iPr_def_18 )
| ( a2 != a2 )
| ( iPr_def_20(a3,iPr_def_20(b3,c3)) != iPr_def_20(a3,iPr_def_20(b3,c3)) ) ),
inference(demodulation,[status(thm)],[c_52,c_3987,c_4708,c_5252,c_5878]) ).
tcf(c_17239,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_17238]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP062-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.38 % Computer : n001.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Wed Sep 23 13:31:51 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.43 % Detected problem language: tptp
% 0.09/0.44 % Proving...
% 55.47/8.86 % SZS status Started for theBenchmark.p
% 55.47/8.86 % SZS status Unsatisfiable for theBenchmark.p
% 55.47/8.86
% 55.47/8.86 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 55.47/8.86
% 55.47/8.86 % ------ iProver source info
% 55.47/8.86
% 55.47/8.86 % git: date: 2026-07-19 20:42:38 +0200
% 55.47/8.86 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 55.47/8.86 % git: non_committed_changes: false
% 55.47/8.86
% 55.47/8.86 % ------ Parsing...% successful
% 55.47/8.86
% 55.47/8.86
% 55.47/8.86 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 55.47/8.86
% 55.47/8.86 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 55.47/8.86
% 55.47/8.86 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 55.47/8.86
% 55.47/8.86 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 55.47/8.86 % ------ Proving...
% 55.47/8.86 % ------ Problem Properties
% 55.47/8.86
% 55.47/8.86 %
% 55.47/8.86 % clauses 2
% 55.47/8.86 % conjectures 1
% 55.47/8.86 % EPR 0
% 55.47/8.86 % Horn 2
% 55.47/8.86 % unary 1
% 55.47/8.86 % binary 0
% 55.47/8.86 % lits 4
% 55.47/8.86 % lits eq 4
% 55.47/8.86 % fd_pure 0
% 55.47/8.86 % fd_pseudo 0
% 55.47/8.86 % fd_cond 0
% 55.47/8.86 % fd_pseudo_cond 0
% 55.47/8.86 % AC symbols 0
% 55.47/8.86
% 55.47/8.86 % ------ Input Options Time Limit: Unbounded
% 55.47/8.86
% 55.47/8.86
% 55.47/8.86 % ------
% 55.47/8.86 % Current options:
% 55.47/8.86 % ------
% 55.47/8.86
% 55.47/8.86
% 55.47/8.86 %
% 55.47/8.86
% 55.47/8.86 % ------ Proving...
% 55.47/8.86 %
% 55.47/8.86
% 55.47/8.86 % SZS status Unsatisfiable for theBenchmark.p
% 55.47/8.86
% 55.47/8.86 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 55.47/8.86
% 55.47/8.86
%------------------------------------------------------------------------------