%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP345-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/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:26:00 PM UTC 2025
% Result : Unsatisfiable 10.38s 3.51s
% Output : CNFRefutation 11.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 30
% Syntax : Number of formulae : 501 ( 416 unt; 0 typ; 0 def)
% Number of atoms : 679 ( 657 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 375 ( 197 ~; 178 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 2 avg)
% Maximal term depth : 4 ( 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 : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 222 ( 222 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > 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(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_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
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_146,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( inverse(sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X3) != sk_c7 )
| ( multiply(X3,sk_c6) != sk_c7 )
| ( inverse(X4) != sk_c6 )
| ( multiply(X4,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X1,sk_c7) != sk_c6 )
| ( inverse(X1) != sk_c7 )
| ( inverse(sk_c6) != sk_c5 )
| ( multiply(X2,sk_c6) != sk_c5 )
| ( inverse(X2) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_7445,plain,
! [X_158,Y_159,Z_160] : ( multiply(multiply(X_158,Y_159),Z_160) = multiply(X_158,multiply(Y_159,Z_160)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_7481,plain,
! [X_2,Z_160] : ( multiply(inverse(X_2),multiply(X_2,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_7445]) ).
tff(c_7493,plain,
! [X_2,Z_160] : ( multiply(inverse(X_2),multiply(X_2,Z_160)) = Z_160 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7481]) ).
tff(c_8676,plain,
! [X_187,Z_188] : ( multiply(inverse(X_187),multiply(X_187,Z_188)) = Z_188 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7481]) ).
tff(c_8811,plain,
! [X_190,Z_191] : ( multiply(inverse(inverse(X_190)),Z_191) = multiply(X_190,Z_191) ),
inference(superposition,[status(thm),theory(equality)],[c_7493,c_8676]) ).
tff(c_8706,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8676]) ).
tff(c_8818,plain,
! [X_190] : ( multiply(X_190,identity) = X_190 ),
inference(superposition,[status(thm),theory(equality)],[c_8811,c_8706]) ).
tff(c_62,plain,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_3766,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_89,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_3828,plain,
! [X_84,Y_85,Z_86] : ( multiply(multiply(X_84,Y_85),Z_86) = multiply(X_84,multiply(Y_85,Z_86)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_3870,plain,
! [Z_86] : ( multiply(sk_c6,multiply(sk_c2,Z_86)) = multiply(identity,Z_86) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_3828]) ).
tff(c_3901,plain,
! [Z_88] : ( multiply(sk_c6,multiply(sk_c2,Z_88)) = Z_88 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3870]) ).
tff(c_3913,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_3766,c_3901]) ).
tff(c_66,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_2966,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_3023,plain,
! [X_67,Y_68,Z_69] : ( multiply(multiply(X_67,Y_68),Z_69) = multiply(X_67,multiply(Y_68,Z_69)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_3065,plain,
! [Z_69] : ( multiply(sk_c6,multiply(sk_c2,Z_69)) = multiply(identity,Z_69) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_3023]) ).
tff(c_3106,plain,
! [Z_71] : ( multiply(sk_c6,multiply(sk_c2,Z_71)) = Z_71 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3065]) ).
tff(c_3118,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2966,c_3106]) ).
tff(c_149,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_179,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_149]) ).
tff(c_237,plain,
! [X_17,Z_18] : ( multiply(inverse(X_17),multiply(X_17,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_189,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_1736,plain,
! [X_41,Z_42] : ( multiply(inverse(inverse(X_41)),Z_42) = multiply(X_41,Z_42) ),
inference(superposition,[status(thm),theory(equality)],[c_237,c_189]) ).
tff(c_291,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_237]) ).
tff(c_1743,plain,
! [X_41] : ( multiply(X_41,identity) = X_41 ),
inference(superposition,[status(thm),theory(equality)],[c_1736,c_291]) ).
tff(c_1324,plain,
! [X_31,Z_32] : ( multiply(inverse(inverse(X_31)),Z_32) = multiply(X_31,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_237,c_189]) ).
tff(c_1331,plain,
! [X_31] : ( multiply(X_31,identity) = X_31 ),
inference(superposition,[status(thm),theory(equality)],[c_1324,c_291]) ).
tff(c_126,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_176,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_149]) ).
tff(c_214,plain,
! [Z_16] : ( multiply(sk_c6,multiply(sk_c2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_176]) ).
tff(c_226,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_126,c_214]) ).
tff(c_255,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_226,c_237]) ).
tff(c_14,plain,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_119,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_273,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_119,c_237]) ).
tff(c_672,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_255,c_273]) ).
tff(c_397,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_255,c_273]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_113,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_24,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_98,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_173,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_149]) ).
tff(c_191,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_203,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_113,c_191]) ).
tff(c_410,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_397,c_397,c_203]) ).
tff(c_416,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_226,c_410]) ).
tff(c_444,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_416,c_416,c_255]) ).
tff(c_451,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_444]) ).
tff(c_461,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_451,c_416]) ).
tff(c_68,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_303,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_119,c_68]) ).
tff(c_304,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitLeft,[status(thm)],[c_303]) ).
tff(c_409,plain,
multiply(sk_c6,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_397,c_304]) ).
tff(c_556,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_461,c_2,c_461,c_451,c_409]) ).
tff(c_558,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_303]) ).
tff(c_562,plain,
multiply(inverse(sk_c6),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_558,c_189]) ).
tff(c_683,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_672,c_562]) ).
tff(c_692,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_683]) ).
tff(c_686,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_672,c_672,c_203]) ).
tff(c_693,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_226,c_686]) ).
tff(c_708,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_692,c_693]) ).
tff(c_285,plain,
multiply(inverse(sk_c6),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_237]) ).
tff(c_710,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_708,c_285]) ).
tff(c_714,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_710]) ).
tff(c_713,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_708,c_85]) ).
tff(c_768,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_714,c_713]) ).
tff(c_557,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(sk_c6) != sk_c5 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_303]) ).
tff(c_616,plain,
inverse(sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_557]) ).
tff(c_700,plain,
inverse(sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_692,c_616]) ).
tff(c_788,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_768,c_708,c_700]) ).
tff(c_790,plain,
inverse(sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_557]) ).
tff(c_1066,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_790,c_562]) ).
tff(c_1070,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_1066,c_189]) ).
tff(c_1076,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1070]) ).
tff(c_1201,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_1076,c_1076,c_203]) ).
tff(c_1209,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1201]) ).
tff(c_294,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_237]) ).
tff(c_1225,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1209,c_85]) ).
tff(c_1253,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_1225,c_291]) ).
tff(c_1262,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_294,c_1253]) ).
tff(c_791,plain,
multiply(sk_c5,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_790,c_285]) ).
tff(c_1197,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_1076,c_1066]) ).
tff(c_1207,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_791,c_1197]) ).
tff(c_1265,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1262,c_1207]) ).
tff(c_1083,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_1076,c_1076,c_203]) ).
tff(c_1091,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1083]) ).
tff(c_1107,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1091,c_85]) ).
tff(c_1135,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_1107,c_291]) ).
tff(c_1144,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_294,c_1135]) ).
tff(c_1079,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_1076,c_1066]) ).
tff(c_1089,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_791,c_1079]) ).
tff(c_1098,plain,
inverse(sk_c6) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_1089,c_790]) ).
tff(c_1156,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1144,c_1091,c_1098]) ).
tff(c_1147,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1144,c_1089]) ).
tff(c_885,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_790,c_562]) ).
tff(c_889,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_885,c_189]) ).
tff(c_895,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_889]) ).
tff(c_901,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_895,c_895,c_203]) ).
tff(c_909,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_901]) ).
tff(c_897,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_895,c_885]) ).
tff(c_907,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_791,c_897]) ).
tff(c_917,plain,
inverse(sk_c6) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_907,c_790]) ).
tff(c_956,plain,
inverse(identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_909,c_917]) ).
tff(c_279,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_102,c_237]) ).
tff(c_899,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_895,c_279]) ).
tff(c_908,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_294,c_899]) ).
tff(c_906,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_895,c_98]) ).
tff(c_983,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_956,c_908,c_906]) ).
tff(c_947,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_909,c_85]) ).
tff(c_996,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_983,c_947]) ).
tff(c_789,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_557]) ).
tff(c_802,plain,
! [X3_6] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_789]) ).
tff(c_926,plain,
! [X3_27] :
( ( multiply(X3_27,sk_c6) != identity )
| ( inverse(X3_27) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_895,c_895,c_802]) ).
tff(c_943,plain,
inverse(inverse(sk_c6)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_926]) ).
tff(c_1020,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_996,c_996,c_909,c_943]) ).
tff(c_1021,plain,
! [X4_7,X1_8,X2_9] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_789]) ).
tff(c_1078,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_1021]) ).
tff(c_1176,plain,
! [X2_29] :
( ( inverse(X2_29) != identity )
| ( multiply(X2_29,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1147,c_1091,c_1091,c_1078]) ).
tff(c_1187,plain,
inverse(inverse(identity)) != identity,
inference(superposition,[status(thm),theory(equality)],[c_4,c_1176]) ).
tff(c_1195,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1156,c_1156,c_1187]) ).
tff(c_1196,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_1021]) ).
tff(c_1293,plain,
! [X1_8,X4_7] :
( ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != identity )
| ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1209,c_1265,c_1209,c_1209,c_1076,c_1076,c_1196]) ).
tff(c_1294,plain,
! [X4_7] :
( ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity ) ),
inference(splitLeft,[status(thm)],[c_1293]) ).
tff(c_1706,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_1331,c_1294]) ).
tff(c_1216,plain,
inverse(sk_c6) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_1207,c_790]) ).
tff(c_1274,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1262,c_1209,c_1216]) ).
tff(c_1708,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1706,c_1274]) ).
tff(c_1709,plain,
! [X1_8] :
( ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != identity ) ),
inference(splitRight,[status(thm)],[c_1293]) ).
tff(c_2122,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_1743,c_1709]) ).
tff(c_2124,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2122,c_1274]) ).
tff(c_2125,plain,
inverse(sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_2130,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2125,c_4]) ).
tff(c_2190,plain,
! [X_51,Y_52,Z_53] : ( multiply(multiply(X_51,Y_52),Z_53) = multiply(X_51,multiply(Y_52,Z_53)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_2220,plain,
! [Z_53] : ( multiply(sk_c5,multiply(sk_c6,Z_53)) = multiply(identity,Z_53) ),
inference(superposition,[status(thm),theory(equality)],[c_2130,c_2190]) ).
tff(c_2379,plain,
! [Z_59] : ( multiply(sk_c5,multiply(sk_c6,Z_59)) = Z_59 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2220]) ).
tff(c_2403,plain,
multiply(sk_c5,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_2379]) ).
tff(c_2126,plain,
multiply(sk_c2,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_2134,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2126,c_66]) ).
tff(c_2138,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2134,c_4]) ).
tff(c_2397,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_2138,c_2379]) ).
tff(c_2471,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2403,c_2397]) ).
tff(c_64,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_2175,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2126,c_64]) ).
tff(c_2472,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2471,c_2175]) ).
tff(c_2232,plain,
! [Z_53] : ( multiply(sk_c6,multiply(sk_c2,Z_53)) = multiply(identity,Z_53) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_2190]) ).
tff(c_2247,plain,
! [Z_53] : ( multiply(sk_c6,multiply(sk_c2,Z_53)) = Z_53 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2232]) ).
tff(c_2484,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_2472,c_2247]) ).
tff(c_56,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_2169,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_2126,c_56]) ).
tff(c_2678,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2484,c_2169]) ).
tff(c_2394,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2169,c_2379]) ).
tff(c_2697,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2678,c_2394]) ).
tff(c_2707,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2130,c_2697]) ).
tff(c_2400,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_119,c_2379]) ).
tff(c_2695,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2678,c_2400]) ).
tff(c_2844,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2707,c_2,c_2707,c_2695]) ).
tff(c_2714,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_2707,c_2403]) ).
tff(c_2720,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2714]) ).
tff(c_2718,plain,
multiply(sk_c2,identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_2707,c_2126]) ).
tff(c_2950,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2844,c_2,c_2720,c_2718]) ).
tff(c_2951,plain,
inverse(sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_2956,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2951,c_4]) ).
tff(c_3056,plain,
! [Z_69] : ( multiply(sk_c5,multiply(sk_c6,Z_69)) = multiply(identity,Z_69) ),
inference(superposition,[status(thm),theory(equality)],[c_2956,c_3023]) ).
tff(c_3129,plain,
! [Z_72] : ( multiply(sk_c5,multiply(sk_c6,Z_72)) = Z_72 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3056]) ).
tff(c_3153,plain,
multiply(sk_c5,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_3129]) ).
tff(c_2952,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_2989,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2952,c_18]) ).
tff(c_2993,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2989,c_4]) ).
tff(c_3150,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_2993,c_3129]) ).
tff(c_3174,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_3153,c_3150]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_3017,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2952,c_16]) ).
tff(c_3214,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_3174,c_3017]) ).
tff(c_3080,plain,
! [Z_69] : ( multiply(sk_c6,multiply(sk_c2,Z_69)) = Z_69 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3065]) ).
tff(c_3226,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3214,c_3080]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_3012,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_2952,c_8]) ).
tff(c_3233,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3226,c_3012]) ).
tff(c_3256,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_3233,c_2952]) ).
tff(c_3264,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3118,c_3256]) ).
tff(c_3266,plain,
multiply(sk_c2,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_3301,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_3266,c_56]) ).
tff(c_3325,plain,
! [X_74,Y_75,Z_76] : ( multiply(multiply(X_74,Y_75),Z_76) = multiply(X_74,multiply(Y_75,Z_76)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_3355,plain,
! [Z_76] : ( multiply(sk_c5,multiply(sk_c6,Z_76)) = multiply(identity,Z_76) ),
inference(superposition,[status(thm),theory(equality)],[c_2956,c_3325]) ).
tff(c_3420,plain,
! [Z_79] : ( multiply(sk_c5,multiply(sk_c6,Z_79)) = Z_79 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3355]) ).
tff(c_3435,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_3301,c_3420]) ).
tff(c_3367,plain,
! [X_2,Z_76] : ( multiply(inverse(X_2),multiply(X_2,Z_76)) = multiply(identity,Z_76) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_3325]) ).
tff(c_3469,plain,
! [X_80,Z_81] : ( multiply(inverse(X_80),multiply(X_80,Z_81)) = Z_81 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3367]) ).
tff(c_3490,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_3435,c_3469]) ).
tff(c_3557,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_3490]) ).
tff(c_3265,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_3307,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_3266,c_64]) ).
tff(c_3511,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3307,c_3469]) ).
tff(c_3560,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3301,c_3265,c_3511]) ).
tff(c_3653,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_3557,c_3560]) ).
tff(c_3568,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_3560,c_3435]) ).
tff(c_3579,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2956,c_3568]) ).
tff(c_3575,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_3560,c_2952]) ).
tff(c_3749,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3653,c_2,c_3653,c_3579,c_3575]) ).
tff(c_3751,plain,
multiply(sk_c1,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_40,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_3809,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_3751,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_3781,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_3751,c_42]) ).
tff(c_3785,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_3781,c_4]) ).
tff(c_3855,plain,
! [Z_86] : ( multiply(sk_c6,multiply(sk_c4,Z_86)) = multiply(identity,Z_86) ),
inference(superposition,[status(thm),theory(equality)],[c_3785,c_3828]) ).
tff(c_4037,plain,
! [Z_91] : ( multiply(sk_c6,multiply(sk_c4,Z_91)) = Z_91 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3855]) ).
tff(c_4049,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3809,c_4037]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_3817,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_3751,c_32]) ).
tff(c_4053,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4049,c_3817]) ).
tff(c_34,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_3823,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_3751,c_34]) ).
tff(c_4149,plain,
multiply(sk_c3,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4053,c_3823]) ).
tff(c_3750,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_3755,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_3750,c_4]) ).
tff(c_3864,plain,
! [Z_86] : ( multiply(sk_c7,multiply(sk_c3,Z_86)) = multiply(identity,Z_86) ),
inference(superposition,[status(thm),theory(equality)],[c_3755,c_3828]) ).
tff(c_3883,plain,
! [Z_86] : ( multiply(sk_c7,multiply(sk_c3,Z_86)) = Z_86 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3864]) ).
tff(c_4203,plain,
! [Z_93] : ( multiply(sk_c6,multiply(sk_c3,Z_93)) = Z_93 ),
inference(demodulation,[status(thm),theory(equality)],[c_4053,c_3883]) ).
tff(c_4215,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4149,c_4203]) ).
tff(c_4219,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_3913,c_4215]) ).
tff(c_4230,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4219,c_4219,c_3913]) ).
tff(c_3873,plain,
! [X_2,Z_86] : ( multiply(inverse(X_2),multiply(X_2,Z_86)) = multiply(identity,Z_86) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_3828]) ).
tff(c_3886,plain,
! [X_2,Z_86] : ( multiply(inverse(X_2),multiply(X_2,Z_86)) = Z_86 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3873]) ).
tff(c_4355,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4230,c_3886]) ).
tff(c_4364,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4355]) ).
tff(c_4154,plain,
multiply(sk_c6,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4053,c_102]) ).
tff(c_4223,plain,
multiply(sk_c5,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4219,c_4154]) ).
tff(c_4472,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4364,c_4223]) ).
tff(c_4152,plain,
multiply(sk_c1,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4053,c_3751]) ).
tff(c_4221,plain,
multiply(sk_c1,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4219,c_4219,c_4152]) ).
tff(c_4470,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_4364,c_4364,c_4221]) ).
tff(c_4473,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_4472,c_4470]) ).
tff(c_4477,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4473]) ).
tff(c_4478,plain,
inverse(sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_4483,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4478,c_4]) ).
tff(c_5275,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_3751,c_40]) ).
tff(c_4479,plain,
multiply(sk_c2,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_4525,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_4479,c_64]) ).
tff(c_4501,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4479,c_66]) ).
tff(c_4505,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4501,c_4]) ).
tff(c_4543,plain,
! [X_98,Y_99,Z_100] : ( multiply(multiply(X_98,Y_99),Z_100) = multiply(X_98,multiply(Y_99,Z_100)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4567,plain,
! [Z_100] : ( multiply(sk_c6,multiply(sk_c4,Z_100)) = multiply(identity,Z_100) ),
inference(superposition,[status(thm),theory(equality)],[c_4505,c_4543]) ).
tff(c_4815,plain,
! [Z_107] : ( multiply(sk_c6,multiply(sk_c4,Z_107)) = Z_107 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4567]) ).
tff(c_4827,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4525,c_4815]) ).
tff(c_4520,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_3751,c_32]) ).
tff(c_4831,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4827,c_4520]) ).
tff(c_4492,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_4936,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4831,c_4492]) ).
tff(c_58,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_4536,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4479,c_58]) ).
tff(c_4576,plain,
! [Z_100] : ( multiply(sk_c7,multiply(sk_c3,Z_100)) = multiply(identity,Z_100) ),
inference(superposition,[status(thm),theory(equality)],[c_3755,c_4543]) ).
tff(c_4626,plain,
! [Z_103] : ( multiply(sk_c7,multiply(sk_c3,Z_103)) = Z_103 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4576]) ).
tff(c_4638,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_4536,c_4626]) ).
tff(c_4932,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4831,c_4831,c_4638]) ).
tff(c_4993,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4936,c_4932]) ).
tff(c_5009,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4993,c_4993,c_4827]) ).
tff(c_4585,plain,
! [X_2,Z_100] : ( multiply(inverse(X_2),multiply(X_2,Z_100)) = multiply(identity,Z_100) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4543]) ).
tff(c_4598,plain,
! [X_2,Z_100] : ( multiply(inverse(X_2),multiply(X_2,Z_100)) = Z_100 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4585]) ).
tff(c_5123,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5009,c_4598]) ).
tff(c_5129,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5123]) ).
tff(c_4941,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4831,c_98]) ).
tff(c_5006,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4993,c_4941]) ).
tff(c_5048,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5006,c_4]) ).
tff(c_5149,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5129,c_5048]) ).
tff(c_4938,plain,
multiply(sk_c1,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4831,c_3751]) ).
tff(c_5003,plain,
multiply(sk_c1,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4993,c_4993,c_4938]) ).
tff(c_5238,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5149,c_5129,c_5129,c_5003]) ).
tff(c_5239,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_5244,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5239,c_4]) ).
tff(c_5293,plain,
! [X_111,Y_112,Z_113] : ( multiply(multiply(X_111,Y_112),Z_113) = multiply(X_111,multiply(Y_112,Z_113)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_5317,plain,
! [Z_113] : ( multiply(sk_c6,multiply(sk_c4,Z_113)) = multiply(identity,Z_113) ),
inference(superposition,[status(thm),theory(equality)],[c_5244,c_5293]) ).
tff(c_5375,plain,
! [Z_116] : ( multiply(sk_c6,multiply(sk_c4,Z_116)) = Z_116 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5317]) ).
tff(c_5387,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5275,c_5375]) ).
tff(c_5332,plain,
! [X_2,Z_113] : ( multiply(inverse(X_2),multiply(X_2,Z_113)) = multiply(identity,Z_113) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_5293]) ).
tff(c_5418,plain,
! [X_117,Z_118] : ( multiply(inverse(X_117),multiply(X_117,Z_118)) = Z_118 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5332]) ).
tff(c_5439,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5387,c_5418]) ).
tff(c_5479,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4483,c_4478,c_5439]) ).
tff(c_5491,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5479,c_4478]) ).
tff(c_5240,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_5266,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_5240,c_8]) ).
tff(c_5391,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5387,c_5266]) ).
tff(c_5406,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5391,c_98]) ).
tff(c_5502,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5406,c_4]) ).
tff(c_5345,plain,
! [X_2,Z_113] : ( multiply(inverse(X_2),multiply(X_2,Z_113)) = Z_113 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5332]) ).
tff(c_5519,plain,
multiply(inverse(sk_c6),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_5502,c_5345]) ).
tff(c_5525,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5491,c_5519]) ).
tff(c_5403,plain,
multiply(sk_c1,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5391,c_3751]) ).
tff(c_5595,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5525,c_5403]) ).
tff(c_5597,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_26,plain,
( ( inverse(sk_c6) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_5621,plain,
inverse(sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_5597,c_26]) ).
tff(c_5625,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5621,c_4]) ).
tff(c_5670,plain,
! [X_120,Y_121,Z_122] : ( multiply(multiply(X_120,Y_121),Z_122) = multiply(X_120,multiply(Y_121,Z_122)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_5694,plain,
! [Z_122] : ( multiply(sk_c5,multiply(sk_c6,Z_122)) = multiply(identity,Z_122) ),
inference(superposition,[status(thm),theory(equality)],[c_5625,c_5670]) ).
tff(c_5720,plain,
! [Z_123] : ( multiply(sk_c5,multiply(sk_c6,Z_123)) = Z_123 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5694]) ).
tff(c_5738,plain,
multiply(sk_c5,identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_5720]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_5605,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_5597,c_30]) ).
tff(c_5609,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5605,c_4]) ).
tff(c_5735,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_5609,c_5720]) ).
tff(c_5757,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_5738,c_5735]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_5648,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_5597,c_28]) ).
tff(c_5766,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5757,c_5648]) ).
tff(c_5703,plain,
! [Z_122] : ( multiply(sk_c6,multiply(sk_c2,Z_122)) = multiply(identity,Z_122) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_5670]) ).
tff(c_6276,plain,
! [Z_134] : ( multiply(sk_c6,multiply(sk_c2,Z_134)) = Z_134 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5703]) ).
tff(c_6291,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5766,c_6276]) ).
tff(c_20,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_5656,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_5597,c_20]) ).
tff(c_6295,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6291,c_5656]) ).
tff(c_5732,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5656,c_5720]) ).
tff(c_6408,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_5732]) ).
tff(c_6413,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5625,c_6408]) ).
tff(c_5828,plain,
! [Z_126] : ( multiply(sk_c6,multiply(sk_c2,Z_126)) = Z_126 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5703]) ).
tff(c_5849,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5766,c_5828]) ).
tff(c_5853,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5849,c_5656]) ).
tff(c_5872,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5853,c_5732]) ).
tff(c_5877,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5625,c_5872]) ).
tff(c_5885,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_5877,c_5738]) ).
tff(c_5890,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5885]) ).
tff(c_5935,plain,
multiply(sk_c6,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5890,c_89]) ).
tff(c_5882,plain,
multiply(sk_c6,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_5877,c_5849]) ).
tff(c_6028,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5935,c_5882]) ).
tff(c_5776,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5656,c_5621,c_68]) ).
tff(c_5777,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_5776]) ).
tff(c_5871,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5853,c_5777]) ).
tff(c_6073,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6028,c_2,c_6028,c_5877,c_5871]) ).
tff(c_6075,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_5776]) ).
tff(c_6407,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_6075]) ).
tff(c_6988,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6413,c_6407]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_5640,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_5597,c_22]) ).
tff(c_5596,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_5601,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5596,c_4]) ).
tff(c_5700,plain,
! [Z_122] : ( multiply(sk_c7,multiply(sk_c3,Z_122)) = multiply(identity,Z_122) ),
inference(superposition,[status(thm),theory(equality)],[c_5601,c_5670]) ).
tff(c_6253,plain,
! [Z_133] : ( multiply(sk_c7,multiply(sk_c3,Z_133)) = Z_133 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5700]) ).
tff(c_6265,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5640,c_6253]) ).
tff(c_6404,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_6295,c_6265]) ).
tff(c_6989,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6988,c_6404]) ).
tff(c_5706,plain,
! [X_2,Z_122] : ( multiply(inverse(X_2),multiply(X_2,Z_122)) = multiply(identity,Z_122) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_5670]) ).
tff(c_6937,plain,
! [X_148,Z_149] : ( multiply(inverse(X_148),multiply(X_148,Z_149)) = Z_149 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5706]) ).
tff(c_5718,plain,
! [X_2,Z_122] : ( multiply(inverse(X_2),multiply(X_2,Z_122)) = Z_122 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5706]) ).
tff(c_7095,plain,
! [X_151,Z_152] : ( multiply(inverse(inverse(X_151)),Z_152) = multiply(X_151,Z_152) ),
inference(superposition,[status(thm),theory(equality)],[c_6937,c_5718]) ).
tff(c_6976,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_6937]) ).
tff(c_7102,plain,
! [X_151] : ( multiply(X_151,identity) = X_151 ),
inference(superposition,[status(thm),theory(equality)],[c_7095,c_6976]) ).
tff(c_6554,plain,
! [X_138,Z_139] : ( multiply(inverse(X_138),multiply(X_138,Z_139)) = Z_139 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5706]) ).
tff(c_6643,plain,
! [X_141,Z_142] : ( multiply(inverse(inverse(X_141)),Z_142) = multiply(X_141,Z_142) ),
inference(superposition,[status(thm),theory(equality)],[c_5718,c_6554]) ).
tff(c_6581,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_6554]) ).
tff(c_6650,plain,
! [X_141] : ( multiply(X_141,identity) = X_141 ),
inference(superposition,[status(thm),theory(equality)],[c_6643,c_6581]) ).
tff(c_6423,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6413,c_5621]) ).
tff(c_6467,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6423,c_4]) ).
tff(c_6509,plain,
sk_c6 = identity,
inference(superposition,[status(thm),theory(equality)],[c_6467,c_2]) ).
tff(c_6312,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_5732]) ).
tff(c_6317,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5625,c_6312]) ).
tff(c_6324,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_6317,c_5738]) ).
tff(c_6328,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6324]) ).
tff(c_6336,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6328,c_85]) ).
tff(c_6101,plain,
! [Z_130] : ( multiply(sk_c7,multiply(sk_c3,Z_130)) = Z_130 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5700]) ).
tff(c_6113,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5640,c_6101]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_6124,plain,
! [Z_131] : ( multiply(sk_c6,multiply(sk_c7,Z_131)) = multiply(sk_c5,Z_131) ),
inference(superposition,[status(thm),theory(equality)],[c_6075,c_6]) ).
tff(c_6139,plain,
multiply(sk_c6,sk_c7) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_6113,c_6124]) ).
tff(c_6149,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6075,c_5625,c_6139]) ).
tff(c_6154,plain,
multiply(identity,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_6149,c_5738]) ).
tff(c_6162,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6154]) ).
tff(c_6179,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6162,c_85]) ).
tff(c_6159,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6149,c_5621]) ).
tff(c_6215,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6159,c_4]) ).
tff(c_6074,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_5776]) ).
tff(c_6093,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_6074]) ).
tff(c_6195,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6149,c_6093]) ).
tff(c_6229,plain,
inverse(identity) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_6215,c_6195]) ).
tff(c_6244,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6179,c_6229]) ).
tff(c_6245,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_6074]) ).
tff(c_6307,plain,
! [X3_6] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_6245]) ).
tff(c_6384,plain,
! [X3_136] :
( ( multiply(X3_136,sk_c6) != sk_c6 )
| ( inverse(X3_136) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_6295,c_6307]) ).
tff(c_6396,plain,
inverse(identity) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_2,c_6384]) ).
tff(c_6402,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6336,c_6396]) ).
tff(c_6403,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_6245]) ).
tff(c_6471,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,identity) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_6295,c_6413,c_6403]) ).
tff(c_6472,plain,
! [X1_8] :
( ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_6471]) ).
tff(c_6903,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_6650,c_6509,c_6509,c_6509,c_6472]) ).
tff(c_6522,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6509,c_6423]) ).
tff(c_6905,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6903,c_6522]) ).
tff(c_6906,plain,
! [X4_7] :
( ( multiply(X4_7,identity) != sk_c6 )
| ( inverse(X4_7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_6471]) ).
tff(c_7355,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_6989,c_7102,c_6989,c_6906]) ).
tff(c_6412,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_6295,c_5596]) ).
tff(c_6910,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_6412,c_4]) ).
tff(c_7025,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_6989,c_6910]) ).
tff(c_7008,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_6989,c_6412]) ).
tff(c_7031,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7025,c_7008]) ).
tff(c_7357,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7355,c_7031]) ).
tff(c_7359,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_50,plain,
( ( inverse(sk_c6) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_7371,plain,
inverse(sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_7359,c_50]) ).
tff(c_7375,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_7371,c_4]) ).
tff(c_46,plain,
( ( multiply(sk_c3,sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_7407,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_7359,c_46]) ).
tff(c_48,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_7383,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_7359,c_48]) ).
tff(c_7387,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_7383,c_4]) ).
tff(c_7472,plain,
! [Z_160] : ( multiply(sk_c7,multiply(sk_c3,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_7387,c_7445]) ).
tff(c_7498,plain,
! [Z_161] : ( multiply(sk_c7,multiply(sk_c3,Z_161)) = Z_161 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7472]) ).
tff(c_7510,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_7407,c_7498]) ).
tff(c_7545,plain,
! [X_163,Z_164] : ( multiply(inverse(X_163),multiply(X_163,Z_164)) = Z_164 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7481]) ).
tff(c_7569,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_7510,c_7545]) ).
tff(c_7617,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_7569]) ).
tff(c_52,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_7417,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_7359,c_52]) ).
tff(c_7358,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_7363,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_7358,c_4]) ).
tff(c_7478,plain,
! [Z_160] : ( multiply(sk_c6,multiply(sk_c4,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_7363,c_7445]) ).
tff(c_7521,plain,
! [Z_162] : ( multiply(sk_c6,multiply(sk_c4,Z_162)) = Z_162 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7478]) ).
tff(c_7533,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_7417,c_7521]) ).
tff(c_7563,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_7533,c_7545]) ).
tff(c_7615,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_7563]) ).
tff(c_44,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_7422,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_7359,c_44]) ).
tff(c_7537,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_7533,c_7422]) ).
tff(c_7496,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7422,c_7371,c_68]) ).
tff(c_7497,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_7496]) ).
tff(c_7625,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_7537,c_7497]) ).
tff(c_7777,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7617,c_2,c_7617,c_7615,c_7625]) ).
tff(c_7779,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_7496]) ).
tff(c_7787,plain,
! [Z_167] : ( multiply(sk_c7,multiply(sk_c3,Z_167)) = Z_167 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7472]) ).
tff(c_7799,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_7407,c_7787]) ).
tff(c_7991,plain,
! [Z_173] : ( multiply(sk_c6,multiply(sk_c7,Z_173)) = multiply(sk_c5,Z_173) ),
inference(superposition,[status(thm),theory(equality)],[c_7779,c_6]) ).
tff(c_8006,plain,
multiply(sk_c6,sk_c7) = multiply(sk_c5,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_7799,c_7991]) ).
tff(c_8019,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_7375,c_7779,c_8006]) ).
tff(c_8027,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8019,c_7371]) ).
tff(c_8048,plain,
multiply(identity,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_8027,c_4]) ).
tff(c_8649,plain,
sk_c6 = identity,
inference(superposition,[status(thm),theory(equality)],[c_8048,c_2]) ).
tff(c_8116,plain,
! [X_174,Z_175] : ( multiply(inverse(X_174),multiply(X_174,Z_175)) = Z_175 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7481]) ).
tff(c_8251,plain,
! [X_177,Z_178] : ( multiply(inverse(inverse(X_177)),Z_178) = multiply(X_177,Z_178) ),
inference(superposition,[status(thm),theory(equality)],[c_7493,c_8116]) ).
tff(c_8146,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_8116]) ).
tff(c_8258,plain,
! [X_177] : ( multiply(X_177,identity) = X_177 ),
inference(superposition,[status(thm),theory(equality)],[c_8251,c_8146]) ).
tff(c_8089,plain,
sk_c6 = identity,
inference(superposition,[status(thm),theory(equality)],[c_8048,c_2]) ).
tff(c_7475,plain,
! [Z_160] : ( multiply(sk_c5,multiply(sk_c6,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_7375,c_7445]) ).
tff(c_7962,plain,
! [Z_172] : ( multiply(sk_c5,multiply(sk_c6,Z_172)) = Z_172 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_7475]) ).
tff(c_7974,plain,
multiply(sk_c5,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_7779,c_7962]) ).
tff(c_8021,plain,
multiply(identity,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_8019,c_8019,c_7974]) ).
tff(c_8029,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8021]) ).
tff(c_7778,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_7496]) ).
tff(c_7931,plain,
! [X2_171] :
( ( inverse(X2_171) != sk_c6 )
| ( multiply(X2_171,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_7778]) ).
tff(c_7938,plain,
inverse(sk_c4) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_7417,c_7931]) ).
tff(c_7953,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7358,c_7938]) ).
tff(c_7954,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_7778]) ).
tff(c_8066,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != sk_c6 )
| ( multiply(X4_7,identity) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != identity )
| ( inverse(X3_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8029,c_8029,c_8019,c_8029,c_8029,c_7954]) ).
tff(c_8067,plain,
! [X3_6] :
( ( multiply(X3_6,sk_c6) != identity )
| ( inverse(X3_6) != identity ) ),
inference(splitLeft,[status(thm)],[c_8066]) ).
tff(c_8632,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_8258,c_8089,c_8067]) ).
tff(c_8099,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8089,c_8027]) ).
tff(c_8634,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8632,c_8099]) ).
tff(c_8635,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,identity) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_8066]) ).
tff(c_17613,plain,
! [X4_7,X1_8] :
( ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8818,c_8649,c_8649,c_8818,c_8649,c_8635]) ).
tff(c_17615,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_17613]) ).
tff(c_7980,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_7363,c_7962]) ).
tff(c_8636,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_8019,c_7980]) ).
tff(c_8638,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_8636,c_7358]) ).
tff(c_8666,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8649,c_8638]) ).
tff(c_17617,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17615,c_8666]) ).
tff(c_17619,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_17613]) ).
tff(c_17621,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17619,c_8666]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP345-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 21:43:23 EDT 2025
% 0.14/0.34 % CPUTime :
% 10.38/3.51 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.59/3.60
% 10.59/3.60 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------