%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP232-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.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 : 300s
% DateTime : Wed Apr 9 06:25:38 PM UTC 2025
% Result : Unsatisfiable 30.61s 19.90s
% Output : CNFRefutation 31.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 19
% Syntax : Number of formulae : 282 ( 226 unt; 0 typ; 0 def)
% Number of atoms : 389 ( 377 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 229 ( 122 ~; 107 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 122 ( 122 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X6,X3,X1,X2,X4] :
( ( inverse(sk_c8) != sk_c7 )
| ( multiply(X4,sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( multiply(X5,X6) != sk_c8 )
| ( inverse(X5) != X6 )
| ( multiply(X6,sk_c7) != sk_c8 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( multiply(sk_c8,X2) != sk_c7 )
| ( multiply(X3,sk_c8) != X2 )
| ( inverse(X3) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_36,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_111,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_115,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_111,c_4]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_8,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_98,plain,
inverse(sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_132549,plain,
! [X_482,Y_483,Z_484] : ( multiply(multiply(X_482,Y_483),Z_484) = multiply(X_482,multiply(Y_483,Z_484)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_132588,plain,
! [Z_484] : ( multiply(sk_c7,multiply(sk_c8,Z_484)) = multiply(identity,Z_484) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_132549]) ).
tff(c_132648,plain,
! [Z_487] : ( multiply(sk_c7,multiply(sk_c8,Z_487)) = Z_487 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_132588]) ).
tff(c_132672,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_132648]) ).
tff(c_68,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 )
| ( inverse(sk_c8) != sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_132623,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_98,c_68]) ).
tff(c_132749,plain,
! [X4_489] :
( ( inverse(X4_489) != sk_c8 )
| ( multiply(X4_489,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_132623]) ).
tff(c_132767,plain,
( ( inverse(identity) != sk_c8 )
| ( sk_c8 != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_132749]) ).
tff(c_132801,plain,
sk_c8 != sk_c7,
inference(splitLeft,[status(thm)],[c_132767]) ).
tff(c_160,plain,
! [X_14,Y_15,Z_16] : ( multiply(multiply(X_14,Y_15),Z_16) = multiply(X_14,multiply(Y_15,Z_16)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_193,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_160]) ).
tff(c_548,plain,
! [X_26,Z_27] : ( multiply(inverse(X_26),multiply(X_26,Z_27)) = Z_27 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_204,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_712,plain,
! [X_30,Z_31] : ( multiply(inverse(inverse(X_30)),Z_31) = multiply(X_30,Z_31) ),
inference(superposition,[status(thm),theory(equality)],[c_548,c_204]) ).
tff(c_757,plain,
! [X_30] : ( multiply(X_30,inverse(X_30)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_712]) ).
tff(c_578,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_548]) ).
tff(c_723,plain,
! [X_30] : ( multiply(X_30,identity) = X_30 ),
inference(superposition,[status(thm),theory(equality)],[c_712,c_578]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_139,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_184,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c1,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_160]) ).
tff(c_206,plain,
! [Z_17] : ( multiply(sk_c8,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_218,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_139,c_206]) ).
tff(c_187,plain,
! [Z_16] : ( multiply(sk_c7,multiply(sk_c8,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_160]) ).
tff(c_229,plain,
! [Z_18] : ( multiply(sk_c7,multiply(sk_c8,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_187]) ).
tff(c_241,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_218,c_229]) ).
tff(c_251,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_241]) ).
tff(c_339,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_251,c_98]) ).
tff(c_347,plain,
multiply(identity,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_339,c_4]) ).
tff(c_366,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_347,c_2]) ).
tff(c_247,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_229]) ).
tff(c_351,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_251,c_247]) ).
tff(c_354,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_351,c_111]) ).
tff(c_383,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_366,c_354]) ).
tff(c_436,plain,
! [X_21,Z_22] : ( multiply(inverse(X_21),multiply(X_21,Z_22)) = Z_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_470,plain,
! [X_23] : ( multiply(inverse(inverse(X_23)),identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_436]) ).
tff(c_476,plain,
! [X_23] : ( multiply(inverse(inverse(inverse(X_23))),X_23) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_470,c_204]) ).
tff(c_260,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_251,c_98]) ).
tff(c_268,plain,
multiply(identity,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_260,c_4]) ).
tff(c_287,plain,
sk_c8 = identity,
inference(superposition,[status(thm),theory(equality)],[c_268,c_2]) ).
tff(c_272,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_251,c_247]) ).
tff(c_275,plain,
inverse(identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_272,c_111]) ).
tff(c_304,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_287,c_275]) ).
tff(c_253,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_98,c_68]) ).
tff(c_254,plain,
! [X4_11] :
( ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_253]) ).
tff(c_316,plain,
! [X4_19] :
( ( inverse(X4_19) != identity )
| ( multiply(X4_19,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_287,c_251,c_287,c_254]) ).
tff(c_324,plain,
inverse(inverse(identity)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_316]) ).
tff(c_332,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_304,c_304,c_324]) ).
tff(c_333,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_253]) ).
tff(c_394,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),identity) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity )
| ( multiply(X1_9,identity) != identity )
| ( inverse(X1_9) != identity )
| ( inverse(X3_8) != identity )
| ( multiply(X3_8,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_366,c_2,c_366,c_251,c_366,c_366,c_366,c_251,c_366,c_366,c_251,c_333]) ).
tff(c_523,plain,
! [X3_25] :
( ( inverse(X3_25) != identity )
| ( multiply(X3_25,identity) != identity ) ),
inference(splitLeft,[status(thm)],[c_394]) ).
tff(c_527,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_476,c_523]) ).
tff(c_546,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_383,c_383,c_383,c_383,c_527]) ).
tff(c_547,plain,
! [X1_9,X5_6] :
( ( multiply(X1_9,identity) != identity )
| ( inverse(X1_9) != identity )
| ( multiply(inverse(X5_6),identity) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity ) ),
inference(splitRight,[status(thm)],[c_394]) ).
tff(c_132489,plain,
! [X1_9,X5_6] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( inverse(X5_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_757,c_723,c_723,c_547]) ).
tff(c_132490,plain,
! [X5_6] : ( inverse(X5_6) != identity ),
inference(splitLeft,[status(thm)],[c_132489]) ).
tff(c_132492,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_132490,c_383]) ).
tff(c_132494,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_132489]) ).
tff(c_132496,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_132494,c_383]) ).
tff(c_132498,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_22,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_132537,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_132498,c_22]) ).
tff(c_132497,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_132502,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_132497,c_4]) ).
tff(c_132669,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_132502,c_132648]) ).
tff(c_132730,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_132672,c_132669]) ).
tff(c_26,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_132511,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_132498,c_26]) ).
tff(c_132515,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_132511,c_4]) ).
tff(c_132666,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_132515,c_132648]) ).
tff(c_132720,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_132669,c_132666]) ).
tff(c_24,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_132532,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_132498,c_24]) ).
tff(c_132721,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_132720,c_132532]) ).
tff(c_132783,plain,
multiply(sk_c1,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_132730,c_132721]) ).
tff(c_132585,plain,
! [Z_484] : ( multiply(sk_c8,multiply(sk_c1,Z_484)) = multiply(identity,Z_484) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_132549]) ).
tff(c_132604,plain,
! [Z_484] : ( multiply(sk_c8,multiply(sk_c1,Z_484)) = Z_484 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_132585]) ).
tff(c_132791,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_132783,c_132604]) ).
tff(c_132799,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132537,c_132791]) ).
tff(c_132802,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_132801,c_132799]) ).
tff(c_132804,plain,
sk_c8 = sk_c7,
inference(splitRight,[status(thm)],[c_132767]) ).
tff(c_132818,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132804,c_98]) ).
tff(c_132834,plain,
multiply(sk_c7,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_132818,c_4]) ).
tff(c_132663,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_132537,c_132648]) ).
tff(c_132838,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_132834,c_132663]) ).
tff(c_132812,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132804,c_132537]) ).
tff(c_132853,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_132672,c_132838,c_132812]) ).
tff(c_132784,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_132783,c_132498]) ).
tff(c_132847,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_132838,c_132784]) ).
tff(c_132855,plain,
sk_c1 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_132853,c_132847]) ).
tff(c_132817,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_132804,c_102]) ).
tff(c_132865,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_132853,c_132853,c_132817]) ).
tff(c_20,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_132543,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_132498,c_20]) ).
tff(c_132740,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_132730,c_132543]) ).
tff(c_132806,plain,
multiply(sk_c1,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132804,c_132740]) ).
tff(c_132908,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_132865,c_132853,c_132853,c_132806]) ).
tff(c_132909,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_132855,c_132908]) ).
tff(c_132911,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_32,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_132939,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_132911,c_32]) ).
tff(c_132971,plain,
! [X_490,Y_491,Z_492] : ( multiply(multiply(X_490,Y_491),Z_492) = multiply(X_490,multiply(Y_491,Z_492)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_133001,plain,
! [Z_492] : ( multiply(sk_c7,multiply(sk_c8,Z_492)) = multiply(identity,Z_492) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_132971]) ).
tff(c_133237,plain,
! [Z_500] : ( multiply(sk_c7,multiply(sk_c8,Z_500)) = Z_500 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_133001]) ).
tff(c_133255,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_132939,c_133237]) ).
tff(c_28,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_132923,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_132911,c_28]) ).
tff(c_132927,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_132923,c_4]) ).
tff(c_133258,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_132927,c_133237]) ).
tff(c_132910,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_132915,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_132910,c_4]) ).
tff(c_133261,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_132915,c_133237]) ).
tff(c_133926,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_133258,c_133261]) ).
tff(c_34,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_132954,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_132911,c_34]) ).
tff(c_133935,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133926,c_132954]) ).
tff(c_132995,plain,
! [Z_492] : ( multiply(sk_c8,multiply(sk_c4,Z_492)) = multiply(identity,Z_492) ),
inference(superposition,[status(thm),theory(equality)],[c_132927,c_132971]) ).
tff(c_133015,plain,
! [Z_492] : ( multiply(sk_c8,multiply(sk_c4,Z_492)) = Z_492 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_132995]) ).
tff(c_133947,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_133935,c_133015]) ).
tff(c_133953,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132939,c_133947]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_132948,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_132911,c_30]) ).
tff(c_133214,plain,
! [Z_499] : ( multiply(sk_c8,multiply(sk_c4,Z_499)) = Z_499 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_132995]) ).
tff(c_133226,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_132948,c_133214]) ).
tff(c_134164,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_133953,c_133226]) ).
tff(c_134173,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133255,c_134164]) ).
tff(c_134169,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_132923]) ).
tff(c_134213,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_134173,c_134169]) ).
tff(c_134162,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_133935]) ).
tff(c_134221,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_134173,c_134162]) ).
tff(c_134178,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_134173,c_133953]) ).
tff(c_133958,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_133953,c_133226]) ).
tff(c_133967,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133255,c_133958]) ).
tff(c_133974,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133967,c_133967,c_133255]) ).
tff(c_133965,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_102]) ).
tff(c_134062,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133974,c_133967,c_133967,c_133965]) ).
tff(c_133956,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_133935]) ).
tff(c_134014,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133967,c_133956]) ).
tff(c_133963,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133953,c_132923]) ).
tff(c_134005,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133967,c_133963]) ).
tff(c_133972,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133967,c_133953]) ).
tff(c_133281,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_133258,c_133261]) ).
tff(c_133319,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133281,c_132954]) ).
tff(c_133342,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_133319,c_133015]) ).
tff(c_133348,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132939,c_133342]) ).
tff(c_133353,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133348,c_133348,c_133226]) ).
tff(c_133362,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133255,c_133353]) ).
tff(c_133360,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133348,c_102]) ).
tff(c_133427,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133362,c_133362,c_133360]) ).
tff(c_133358,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133348,c_132923]) ).
tff(c_133394,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133362,c_133358]) ).
tff(c_133355,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133348,c_132948]) ).
tff(c_133419,plain,
multiply(sk_c4,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133362,c_133362,c_133355]) ).
tff(c_133007,plain,
! [X_2,Z_492] : ( multiply(inverse(X_2),multiply(X_2,Z_492)) = multiply(identity,Z_492) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_132971]) ).
tff(c_133445,plain,
! [X_503,Z_504] : ( multiply(inverse(X_503),multiply(X_503,Z_504)) = Z_504 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_133007]) ).
tff(c_133469,plain,
multiply(inverse(sk_c4),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_133419,c_133445]) ).
tff(c_133502,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133427,c_133394,c_133469]) ).
tff(c_133367,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133362,c_133348]) ).
tff(c_133512,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133502,c_133367]) ).
tff(c_133361,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133348,c_98]) ).
tff(c_133402,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133362,c_133362,c_133361]) ).
tff(c_133510,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_133502,c_133502,c_133402]) ).
tff(c_133073,plain,
! [Z_496] : ( multiply(sk_c7,multiply(sk_c8,Z_496)) = Z_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_133001]) ).
tff(c_133094,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_132939,c_133073]) ).
tff(c_133097,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_132927,c_133073]) ).
tff(c_133100,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_132915,c_133073]) ).
tff(c_133119,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_133097,c_133100]) ).
tff(c_133120,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133119,c_132954]) ).
tff(c_133132,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_133120,c_133015]) ).
tff(c_133138,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_132939,c_133132]) ).
tff(c_133037,plain,
! [Z_494] : ( multiply(sk_c8,multiply(sk_c4,Z_494)) = Z_494 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_132995]) ).
tff(c_133049,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_132948,c_133037]) ).
tff(c_133171,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133138,c_133138,c_133049]) ).
tff(c_133180,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_133094,c_133171]) ).
tff(c_133022,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( multiply(X4_11,sk_c8) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_98,c_68]) ).
tff(c_133140,plain,
! [X4_497] :
( ( inverse(X4_497) != sk_c8 )
| ( multiply(X4_497,sk_c8) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_133022]) ).
tff(c_133143,plain,
( ( inverse(sk_c4) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_133120,c_133140]) ).
tff(c_133163,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_132923,c_133143]) ).
tff(c_133199,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_133180,c_133163]) ).
tff(c_133200,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_133022]) ).
tff(c_133265,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_133200]) ).
tff(c_133376,plain,
! [X3_502] :
( ( inverse(X3_502) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_502,sk_c8)) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_133362,c_133265]) ).
tff(c_133388,plain,
( ( inverse(identity) != sk_c8 )
| ( multiply(sk_c8,sk_c8) != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_133376]) ).
tff(c_133909,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_133512,c_2,c_133512,c_133502,c_133510,c_133512,c_133388]) ).
tff(c_133910,plain,
! [X1_9,X5_6] :
( ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_133200]) ).
tff(c_133955,plain,
! [X5_6] :
( ( multiply(inverse(X5_6),sk_c7) != sk_c8 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_133910]) ).
tff(c_134036,plain,
! [X5_513] :
( ( multiply(inverse(X5_513),sk_c6) != sk_c6 )
| ( multiply(X5_513,inverse(X5_513)) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_133972,c_133972,c_133967,c_133955]) ).
tff(c_134038,plain,
( ( multiply(sk_c6,sk_c6) != sk_c6 )
| ( multiply(sk_c4,inverse(sk_c4)) != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_134005,c_134036]) ).
tff(c_134047,plain,
multiply(sk_c6,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_134014,c_134005,c_134038]) ).
tff(c_134160,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134062,c_134047]) ).
tff(c_134161,plain,
! [X1_9] :
( ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_133910]) ).
tff(c_134230,plain,
! [X1_517] :
( ( multiply(X1_517,sk_c6) != sk_c6 )
| ( inverse(X1_517) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_134178,c_134178,c_134173,c_134161]) ).
tff(c_134233,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_134221,c_134230]) ).
tff(c_134249,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_134213,c_134233]) ).
tff(c_134251,plain,
inverse(sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_12,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_134303,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_134251,c_12]) ).
tff(c_14,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_134291,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_134251,c_14]) ).
tff(c_16,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_134264,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_134251,c_16]) ).
tff(c_134268,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_134264,c_4]) ).
tff(c_134324,plain,
! [X_518,Y_519,Z_520] : ( multiply(multiply(X_518,Y_519),Z_520) = multiply(X_518,multiply(Y_519,Z_520)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_134351,plain,
! [Z_520] : ( multiply(sk_c8,multiply(sk_c5,Z_520)) = multiply(identity,Z_520) ),
inference(superposition,[status(thm),theory(equality)],[c_134268,c_134324]) ).
tff(c_134374,plain,
! [Z_521] : ( multiply(sk_c8,multiply(sk_c5,Z_521)) = Z_521 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134351]) ).
tff(c_134386,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_134291,c_134374]) ).
tff(c_134390,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134303,c_134386]) ).
tff(c_134250,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_134401,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134390,c_134250]) ).
tff(c_10,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_134310,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_134251,c_10]) ).
tff(c_134392,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134390,c_134310]) ).
tff(c_134360,plain,
! [X_2,Z_520] : ( multiply(inverse(X_2),multiply(X_2,Z_520)) = multiply(identity,Z_520) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_134324]) ).
tff(c_134475,plain,
! [X_522,Z_523] : ( multiply(inverse(X_522),multiply(X_522,Z_523)) = Z_523 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134360]) ).
tff(c_134496,plain,
multiply(inverse(sk_c4),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_134392,c_134475]) ).
tff(c_134536,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134401,c_134496]) ).
tff(c_134372,plain,
! [X_2,Z_520] : ( multiply(inverse(X_2),multiply(X_2,Z_520)) = Z_520 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134360]) ).
tff(c_134548,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_134536,c_134372]) ).
tff(c_134554,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_134548]) ).
tff(c_134400,plain,
inverse(sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134390,c_134251]) ).
tff(c_134563,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_134554,c_134554,c_134400]) ).
tff(c_134278,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_134396,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134390,c_134278]) ).
tff(c_134424,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_134396,c_4]) ).
tff(c_134571,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134554,c_134424]) ).
tff(c_134561,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_134554,c_134396]) ).
tff(c_134600,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_134571,c_134561]) ).
tff(c_134601,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_134563,c_134600]) ).
tff(c_134603,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_134621,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_134603,c_32]) ).
tff(c_134602,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_134641,plain,
! [X_524,Y_525,Z_526] : ( multiply(multiply(X_524,Y_525),Z_526) = multiply(X_524,multiply(Y_525,Z_526)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_134665,plain,
! [Z_526] : ( multiply(sk_c8,multiply(sk_c5,Z_526)) = multiply(identity,Z_526) ),
inference(superposition,[status(thm),theory(equality)],[c_134268,c_134641]) ).
tff(c_134687,plain,
! [Z_527] : ( multiply(sk_c8,multiply(sk_c5,Z_527)) = Z_527 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134665]) ).
tff(c_134699,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_134602,c_134687]) ).
tff(c_134703,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134621,c_134699]) ).
tff(c_134612,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_134251,c_10]) ).
tff(c_134706,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134703,c_134612]) ).
tff(c_134255,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_134250,c_4]) ).
tff(c_134668,plain,
! [Z_526] : ( multiply(sk_c8,multiply(sk_c4,Z_526)) = multiply(identity,Z_526) ),
inference(superposition,[status(thm),theory(equality)],[c_134255,c_134641]) ).
tff(c_134683,plain,
! [Z_526] : ( multiply(sk_c8,multiply(sk_c4,Z_526)) = Z_526 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134668]) ).
tff(c_134773,plain,
! [Z_528] : ( multiply(sk_c7,multiply(sk_c4,Z_528)) = Z_528 ),
inference(demodulation,[status(thm),theory(equality)],[c_134703,c_134683]) ).
tff(c_134785,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_134706,c_134773]) ).
tff(c_134674,plain,
! [X_2,Z_526] : ( multiply(inverse(X_2),multiply(X_2,Z_526)) = multiply(identity,Z_526) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_134641]) ).
tff(c_134685,plain,
! [X_2,Z_526] : ( multiply(inverse(X_2),multiply(X_2,Z_526)) = Z_526 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_134674]) ).
tff(c_134860,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_134785,c_134685]) ).
tff(c_134866,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_134860]) ).
tff(c_134712,plain,
inverse(sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134703,c_134251]) ).
tff(c_134875,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_134866,c_134866,c_134712]) ).
tff(c_134713,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_134703,c_134250]) ).
tff(c_134874,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_134866,c_134713]) ).
tff(c_134939,plain,
multiply(identity,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_134874,c_4]) ).
tff(c_134967,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_134939,c_134685]) ).
tff(c_134979,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_134967]) ).
tff(c_134983,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_134979,c_134874]) ).
tff(c_134986,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_134875,c_134983]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP232-1 : TPTP v9.0.0. Released v2.5.0.
% 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.35 % Computer : n026.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Mon Apr 7 21:38:08 EDT 2025
% 0.12/0.35 % CPUTime :
% 30.61/19.90 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.03/19.94
% 31.03/19.94 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------