%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP296-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 : n021.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:50 PM UTC 2025
% Result : Unsatisfiable 14.78s 5.09s
% Output : CNFRefutation 15.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 37
% Syntax : Number of formulae : 485 ( 400 unt; 0 typ; 0 def)
% Number of atoms : 689 ( 661 equ)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 410 ( 206 ~; 204 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 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 : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 231 ( 231 !; 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_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_152,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_206,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( multiply(X3,sk_c8) != sk_c7 )
| ( inverse(X3) != sk_c8 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( multiply(X4,sk_c8) != sk_c6 )
| ( inverse(X4) != sk_c8 )
| ( multiply(sk_c6,sk_c8) != sk_c7 )
| ( multiply(sk_c8,X1) != sk_c7 )
| ( multiply(X2,sk_c8) != X1 )
| ( inverse(X2) != sk_c8 )
| ( multiply(X5,sk_c6) != sk_c8 )
| ( inverse(X5) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c8,sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c5,sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c2,sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c8,sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c5,sk_c6) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( inverse(sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_155,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c6,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( inverse(sk_c2) = sk_c8 )
| ( multiply(sk_c8,sk_c4) = 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_30879,plain,
! [X_382,Y_383,Z_384] : ( multiply(multiply(X_382,Y_383),Z_384) = multiply(X_382,multiply(Y_383,Z_384)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_30915,plain,
! [X_2,Z_384] : ( multiply(inverse(X_2),multiply(X_2,Z_384)) = multiply(identity,Z_384) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_30879]) ).
tff(c_31203,plain,
! [X_390,Z_391] : ( multiply(inverse(X_390),multiply(X_390,Z_391)) = Z_391 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30915]) ).
tff(c_30926,plain,
! [X_2,Z_384] : ( multiply(inverse(X_2),multiply(X_2,Z_384)) = Z_384 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30915]) ).
tff(c_31490,plain,
! [X_394,Z_395] : ( multiply(inverse(inverse(X_394)),Z_395) = multiply(X_394,Z_395) ),
inference(superposition,[status(thm),theory(equality)],[c_31203,c_30926]) ).
tff(c_31257,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_31203]) ).
tff(c_31497,plain,
! [X_394] : ( multiply(X_394,identity) = X_394 ),
inference(superposition,[status(thm),theory(equality)],[c_31490,c_31257]) ).
tff(c_17632,plain,
! [X_248,Y_249,Z_250] : ( multiply(multiply(X_248,Y_249),Z_250) = multiply(X_248,multiply(Y_249,Z_250)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_17668,plain,
! [X_2,Z_250] : ( multiply(inverse(X_2),multiply(X_2,Z_250)) = multiply(identity,Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17632]) ).
tff(c_17679,plain,
! [X_2,Z_250] : ( multiply(inverse(X_2),multiply(X_2,Z_250)) = Z_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17668]) ).
tff(c_18041,plain,
! [X_259,Z_260] : ( multiply(inverse(X_259),multiply(X_259,Z_260)) = Z_260 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17668]) ).
tff(c_18334,plain,
! [X_264,Z_265] : ( multiply(inverse(inverse(X_264)),Z_265) = multiply(X_264,Z_265) ),
inference(superposition,[status(thm),theory(equality)],[c_17679,c_18041]) ).
tff(c_18101,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18041]) ).
tff(c_18341,plain,
! [X_264] : ( multiply(X_264,identity) = X_264 ),
inference(superposition,[status(thm),theory(equality)],[c_18334,c_18101]) ).
tff(c_66,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_123,plain,
multiply(sk_c2,sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_74,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_97,plain,
inverse(sk_c2) = sk_c8,
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_101,plain,
multiply(sk_c8,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_97,c_4]) ).
tff(c_14118,plain,
! [X_172,Y_173,Z_174] : ( multiply(multiply(X_172,Y_173),Z_174) = multiply(X_172,multiply(Y_173,Z_174)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14160,plain,
! [Z_174] : ( multiply(sk_c8,multiply(sk_c2,Z_174)) = multiply(identity,Z_174) ),
inference(superposition,[status(thm),theory(equality)],[c_101,c_14118]) ).
tff(c_14179,plain,
! [Z_175] : ( multiply(sk_c8,multiply(sk_c2,Z_175)) = Z_175 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14160]) ).
tff(c_14191,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_123,c_14179]) ).
tff(c_54,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_13412,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_13786,plain,
! [X_165,Y_166,Z_167] : ( multiply(multiply(X_165,Y_166),Z_167) = multiply(X_165,multiply(Y_166,Z_167)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13828,plain,
! [Z_167] : ( multiply(sk_c8,multiply(sk_c2,Z_167)) = multiply(identity,Z_167) ),
inference(superposition,[status(thm),theory(equality)],[c_101,c_13786]) ).
tff(c_13858,plain,
! [Z_169] : ( multiply(sk_c8,multiply(sk_c2,Z_169)) = Z_169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13828]) ).
tff(c_13870,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_123,c_13858]) ).
tff(c_13874,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13412,c_13870]) ).
tff(c_13882,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13874,c_13412]) ).
tff(c_13831,plain,
! [X_2,Z_167] : ( multiply(inverse(X_2),multiply(X_2,Z_167)) = multiply(identity,Z_167) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13786]) ).
tff(c_13843,plain,
! [X_2,Z_167] : ( multiply(inverse(X_2),multiply(X_2,Z_167)) = Z_167 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13831]) ).
tff(c_13986,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_13882,c_13843]) ).
tff(c_13992,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13986]) ).
tff(c_13284,plain,
! [X_151,Y_152,Z_153] : ( multiply(multiply(X_151,Y_152),Z_153) = multiply(X_151,multiply(Y_152,Z_153)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13326,plain,
! [Z_153] : ( multiply(sk_c8,multiply(sk_c2,Z_153)) = multiply(identity,Z_153) ),
inference(superposition,[status(thm),theory(equality)],[c_101,c_13284]) ).
tff(c_13356,plain,
! [Z_155] : ( multiply(sk_c8,multiply(sk_c2,Z_155)) = Z_155 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13326]) ).
tff(c_13368,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_123,c_13356]) ).
tff(c_133,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_12361,plain,
! [X_136,Y_137,Z_138] : ( multiply(multiply(X_136,Y_137),Z_138) = multiply(X_136,multiply(Y_137,Z_138)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12406,plain,
! [Z_138] : ( multiply(sk_c8,multiply(sk_c2,Z_138)) = multiply(identity,Z_138) ),
inference(superposition,[status(thm),theory(equality)],[c_101,c_12361]) ).
tff(c_12436,plain,
! [Z_140] : ( multiply(sk_c8,multiply(sk_c2,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12406]) ).
tff(c_12448,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_123,c_12436]) ).
tff(c_12452,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_133,c_12448]) ).
tff(c_12462,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_12452,c_133]) ).
tff(c_12409,plain,
! [X_2,Z_138] : ( multiply(inverse(X_2),multiply(X_2,Z_138)) = multiply(identity,Z_138) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12361]) ).
tff(c_12421,plain,
! [X_2,Z_138] : ( multiply(inverse(X_2),multiply(X_2,Z_138)) = Z_138 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12409]) ).
tff(c_12582,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12462,c_12421]) ).
tff(c_12588,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12582]) ).
tff(c_171,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_204,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_171]) ).
tff(c_375,plain,
! [X_19,Z_20] : ( multiply(inverse(X_19),multiply(X_19,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_204]) ).
tff(c_214,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_204]) ).
tff(c_694,plain,
! [X_24,Z_25] : ( multiply(inverse(inverse(X_24)),Z_25) = multiply(X_24,Z_25) ),
inference(superposition,[status(thm),theory(equality)],[c_375,c_214]) ).
tff(c_417,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_375]) ).
tff(c_705,plain,
! [X_24] : ( multiply(X_24,identity) = X_24 ),
inference(superposition,[status(thm),theory(equality)],[c_694,c_417]) ).
tff(c_14,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_128,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_30,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_141,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_38,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_110,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_114,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_110,c_4]) ).
tff(c_198,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_171]) ).
tff(c_216,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_198]) ).
tff(c_228,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_141,c_216]) ).
tff(c_232,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_128,c_228]) ).
tff(c_80,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X2_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X2_9,sk_c8)) != sk_c7 )
| ( multiply(sk_c6,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(X4_10,sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_246,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(sk_c6,multiply(X2_9,sk_c6)) != sk_c7 )
| ( multiply(sk_c6,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( multiply(sk_c6,sk_c6) != sk_c7 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_232,c_232,c_232,c_232,c_232,c_232,c_232,c_232,c_232,c_232,c_232,c_80]) ).
tff(c_247,plain,
multiply(sk_c6,sk_c7) != sk_c6,
inference(splitLeft,[status(thm)],[c_246]) ).
tff(c_239,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_232,c_110]) ).
tff(c_234,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_232,c_141]) ).
tff(c_277,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_204]) ).
tff(c_295,plain,
multiply(inverse(sk_c1),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_234,c_277]) ).
tff(c_317,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_239,c_295]) ).
tff(c_319,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_247,c_317]) ).
tff(c_321,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_246]) ).
tff(c_405,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_321,c_375]) ).
tff(c_425,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_405]) ).
tff(c_235,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_232,c_133]) ).
tff(c_426,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_425,c_235]) ).
tff(c_241,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_232,c_97]) ).
tff(c_237,plain,
multiply(sk_c2,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_232,c_123]) ).
tff(c_436,plain,
multiply(inverse(sk_c2),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_237,c_214]) ).
tff(c_442,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_241,c_436]) ).
tff(c_480,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_426,c_442]) ).
tff(c_320,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(sk_c6,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c6) != sk_c7 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(sk_c6,multiply(X2_9,sk_c6)) != sk_c7 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_246]) ).
tff(c_8457,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_705,c_480,c_480,c_480,c_705,c_480,c_2,c_480,c_425,c_480,c_705,c_480,c_480,c_480,c_705,c_480,c_425,c_480,c_480,c_2,c_480,c_425,c_480,c_2,c_480,c_425,c_320]) ).
tff(c_8459,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8457]) ).
tff(c_488,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_480,c_239]) ).
tff(c_534,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_488,c_4]) ).
tff(c_554,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_534,c_214]) ).
tff(c_566,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_554]) ).
tff(c_571,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_566,c_488]) ).
tff(c_8461,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8459,c_571]) ).
tff(c_8462,plain,
! [X2_9,X4_10,X3_7] :
( ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_8457]) ).
tff(c_11670,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8462]) ).
tff(c_11672,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11670,c_571]) ).
tff(c_11673,plain,
! [X4_10,X2_9] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(splitRight,[status(thm)],[c_8462]) ).
tff(c_11675,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_11673]) ).
tff(c_11677,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11675,c_571]) ).
tff(c_12293,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_11673]) ).
tff(c_12295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12293,c_571]) ).
tff(c_12296,plain,
inverse(sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_12592,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12588,c_12296]) ).
tff(c_12297,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c5,sk_c6) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_12331,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_12297,c_28]) ).
tff(c_12458,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_12452,c_12331]) ).
tff(c_12726,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_12588,c_12458]) ).
tff(c_12730,plain,
multiply(inverse(sk_c5),sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12726,c_12421]) ).
tff(c_12736,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12592,c_12730]) ).
tff(c_12465,plain,
multiply(sk_c7,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12452,c_114]) ).
tff(c_12744,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12736,c_12465]) ).
tff(c_12870,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_12744,c_12421]) ).
tff(c_12882,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12870]) ).
tff(c_12461,plain,
multiply(sk_c1,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_12452,c_12297]) ).
tff(c_12740,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_12736,c_12736,c_12461]) ).
tff(c_12896,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12882,c_12740]) ).
tff(c_12898,plain,
multiply(sk_c8,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_13372,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13368,c_12898]) ).
tff(c_24,plain,
( ( multiply(sk_c3,sk_c8) = sk_c4 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_12940,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_12970,plain,
! [X_145,Y_146,Z_147] : ( multiply(multiply(X_145,Y_146),Z_147) = multiply(X_145,multiply(Y_146,Z_147)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13012,plain,
! [Z_147] : ( multiply(sk_c8,multiply(sk_c1,Z_147)) = multiply(identity,Z_147) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_12970]) ).
tff(c_13032,plain,
! [Z_148] : ( multiply(sk_c8,multiply(sk_c1,Z_148)) = Z_148 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13012]) ).
tff(c_13044,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_12940,c_13032]) ).
tff(c_13048,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_128,c_13044]) ).
tff(c_13058,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13048,c_128]) ).
tff(c_13018,plain,
! [X_2,Z_147] : ( multiply(inverse(X_2),multiply(X_2,Z_147)) = multiply(identity,Z_147) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12970]) ).
tff(c_13133,plain,
! [X_149,Z_150] : ( multiply(inverse(X_149),multiply(X_149,Z_150)) = Z_150 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13018]) ).
tff(c_13151,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13058,c_13133]) ).
tff(c_13185,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13151]) ).
tff(c_44,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_12964,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12898,c_44]) ).
tff(c_13050,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13048,c_12964]) ).
tff(c_13239,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13185,c_13050]) ).
tff(c_13057,plain,
multiply(sk_c6,sk_c6) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13048,c_12898]) ).
tff(c_13252,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13239,c_13185,c_13057]) ).
tff(c_13254,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_22,plain,
( ( multiply(sk_c8,sk_c4) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_13269,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13254,c_22]) ).
tff(c_13253,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_12910,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_12898,c_50]) ).
tff(c_12914,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12910,c_4]) ).
tff(c_13311,plain,
! [Z_153] : ( multiply(sk_c8,multiply(sk_c3,Z_153)) = multiply(identity,Z_153) ),
inference(superposition,[status(thm),theory(equality)],[c_12914,c_13284]) ).
tff(c_13380,plain,
! [Z_156] : ( multiply(sk_c8,multiply(sk_c3,Z_156)) = Z_156 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13311]) ).
tff(c_13392,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13253,c_13380]) ).
tff(c_13396,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13269,c_13392]) ).
tff(c_13398,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13372,c_13396]) ).
tff(c_13400,plain,
multiply(sk_c8,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_13418,plain,
inverse(sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_13400,c_18]) ).
tff(c_13998,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13992,c_13418]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c6) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_13445,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_13400,c_16]) ).
tff(c_13881,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13874,c_13445]) ).
tff(c_14026,plain,
multiply(sk_c5,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_13992,c_13881]) ).
tff(c_14030,plain,
multiply(inverse(sk_c5),sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14026,c_13843]) ).
tff(c_14036,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13998,c_14030]) ).
tff(c_13884,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13874,c_13400]) ).
tff(c_14014,plain,
multiply(sk_c7,sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13992,c_13884]) ).
tff(c_14041,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_14036,c_14036,c_14014]) ).
tff(c_14049,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14041]) ).
tff(c_14051,plain,
multiply(sk_c8,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_14195,plain,
sk_c8 != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14191,c_14051]) ).
tff(c_10,plain,
( ( multiply(sk_c8,sk_c4) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_14108,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13400,c_10]) ).
tff(c_13399,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_48,plain,
( ( multiply(sk_c3,sk_c8) = sk_c4 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_14091,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_14051,c_48]) ).
tff(c_14163,plain,
! [X_2,Z_174] : ( multiply(inverse(X_2),multiply(X_2,Z_174)) = multiply(identity,Z_174) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14118]) ).
tff(c_14227,plain,
! [X_177,Z_178] : ( multiply(inverse(X_177),multiply(X_177,Z_178)) = Z_178 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14163]) ).
tff(c_14266,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14091,c_14227]) ).
tff(c_14312,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14108,c_13399,c_14266]) ).
tff(c_14314,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14195,c_14312]) ).
tff(c_14316,plain,
multiply(sk_c2,sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_64,plain,
( ( multiply(sk_c5,sk_c6) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_16511,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_14316,c_64]) ).
tff(c_14315,plain,
inverse(sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_14320,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14315,c_4]) ).
tff(c_16540,plain,
! [X_226,Y_227,Z_228] : ( multiply(multiply(X_226,Y_227),Z_228) = multiply(X_226,multiply(Y_227,Z_228)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16573,plain,
! [Z_228] : ( multiply(sk_c6,multiply(sk_c5,Z_228)) = multiply(identity,Z_228) ),
inference(superposition,[status(thm),theory(equality)],[c_14320,c_16540]) ).
tff(c_16636,plain,
! [Z_231] : ( multiply(sk_c6,multiply(sk_c5,Z_231)) = Z_231 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16573]) ).
tff(c_16648,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16511,c_16636]) ).
tff(c_14328,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_15989,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_16018,plain,
! [X_211,Y_212,Z_213] : ( multiply(multiply(X_211,Y_212),Z_213) = multiply(X_211,multiply(Y_212,Z_213)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16057,plain,
! [Z_213] : ( multiply(sk_c8,multiply(sk_c1,Z_213)) = multiply(identity,Z_213) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_16018]) ).
tff(c_16092,plain,
! [Z_215] : ( multiply(sk_c8,multiply(sk_c1,Z_215)) = Z_215 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16057]) ).
tff(c_16104,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_15989,c_16092]) ).
tff(c_16108,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14328,c_16104]) ).
tff(c_16119,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16108,c_14328]) ).
tff(c_16063,plain,
! [X_2,Z_213] : ( multiply(inverse(X_2),multiply(X_2,Z_213)) = multiply(identity,Z_213) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16018]) ).
tff(c_16075,plain,
! [X_2,Z_213] : ( multiply(inverse(X_2),multiply(X_2,Z_213)) = Z_213 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16063]) ).
tff(c_16207,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16119,c_16075]) ).
tff(c_16213,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16207]) ).
tff(c_15048,plain,
! [X_188,Y_189,Z_190] : ( multiply(multiply(X_188,Y_189),Z_190) = multiply(X_188,multiply(Y_189,Z_190)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_15084,plain,
! [Z_190] : ( multiply(sk_c6,multiply(sk_c5,Z_190)) = multiply(identity,Z_190) ),
inference(superposition,[status(thm),theory(equality)],[c_14320,c_15048]) ).
tff(c_15102,plain,
! [Z_190] : ( multiply(sk_c6,multiply(sk_c5,Z_190)) = Z_190 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15084]) ).
tff(c_15019,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_14316,c_64]) ).
tff(c_15575,plain,
! [Z_204] : ( multiply(sk_c6,multiply(sk_c5,Z_204)) = Z_204 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15084]) ).
tff(c_15587,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_15019,c_15575]) ).
tff(c_56,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_15025,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14316,c_56]) ).
tff(c_15591,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15587,c_15025]) ).
tff(c_14334,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_15078,plain,
! [Z_190] : ( multiply(sk_c8,multiply(sk_c6,Z_190)) = multiply(sk_c7,Z_190) ),
inference(superposition,[status(thm),theory(equality)],[c_14334,c_15048]) ).
tff(c_15608,plain,
! [Z_205] : ( multiply(sk_c8,multiply(sk_c6,Z_205)) = multiply(sk_c6,Z_205) ),
inference(demodulation,[status(thm),theory(equality)],[c_15591,c_15078]) ).
tff(c_15623,plain,
! [Z_190] : ( multiply(sk_c6,multiply(sk_c5,Z_190)) = multiply(sk_c8,Z_190) ),
inference(superposition,[status(thm),theory(equality)],[c_15102,c_15608]) ).
tff(c_15631,plain,
! [Z_190] : ( multiply(sk_c8,Z_190) = Z_190 ),
inference(demodulation,[status(thm),theory(equality)],[c_15102,c_15623]) ).
tff(c_58,plain,
( ( multiply(sk_c8,sk_c4) = sk_c7 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_15039,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14316,c_58]) ).
tff(c_15599,plain,
multiply(sk_c8,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_15591,c_15039]) ).
tff(c_15661,plain,
sk_c6 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_15631,c_15599]) ).
tff(c_15708,plain,
multiply(sk_c4,sk_c8) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_15661,c_15661,c_15587]) ).
tff(c_15093,plain,
! [X_2,Z_190] : ( multiply(inverse(X_2),multiply(X_2,Z_190)) = multiply(identity,Z_190) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_15048]) ).
tff(c_15105,plain,
! [X_2,Z_190] : ( multiply(inverse(X_2),multiply(X_2,Z_190)) = Z_190 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15093]) ).
tff(c_15859,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_15708,c_15105]) ).
tff(c_15866,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15859]) ).
tff(c_15663,plain,
! [Z_206] : ( multiply(sk_c8,Z_206) = Z_206 ),
inference(demodulation,[status(thm),theory(equality)],[c_15102,c_15623]) ).
tff(c_15702,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_101,c_15663]) ).
tff(c_15712,plain,
multiply(sk_c2,sk_c8) != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_15661,c_14316]) ).
tff(c_15819,plain,
sk_c8 != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15702,c_15712]) ).
tff(c_15871,plain,
sk_c4 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15866,c_15819]) ).
tff(c_26,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_14343,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_14398,plain,
! [X_179,Y_180,Z_181] : ( multiply(multiply(X_179,Y_180),Z_181) = multiply(X_179,multiply(Y_180,Z_181)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14440,plain,
! [Z_181] : ( multiply(sk_c8,multiply(sk_c1,Z_181)) = multiply(identity,Z_181) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_14398]) ).
tff(c_14565,plain,
! [Z_184] : ( multiply(sk_c8,multiply(sk_c1,Z_184)) = Z_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14440]) ).
tff(c_14577,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14343,c_14565]) ).
tff(c_14581,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14328,c_14577]) ).
tff(c_14591,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_14328]) ).
tff(c_14446,plain,
! [X_2,Z_181] : ( multiply(inverse(X_2),multiply(X_2,Z_181)) = multiply(identity,Z_181) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14398]) ).
tff(c_14693,plain,
! [X_185,Z_186] : ( multiply(inverse(X_185),multiply(X_185,Z_186)) = Z_186 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14446]) ).
tff(c_14732,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14591,c_14693]) ).
tff(c_14766,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_14732]) ).
tff(c_14390,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14316,c_58]) ).
tff(c_14583,plain,
multiply(sk_c6,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_14390]) ).
tff(c_62,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_14351,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_14316,c_62]) ).
tff(c_14588,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_14351]) ).
tff(c_60,plain,
( ( multiply(sk_c3,sk_c8) = sk_c4 )
| ( multiply(sk_c2,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_14367,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_14316,c_60]) ).
tff(c_14586,plain,
multiply(sk_c3,sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_14367]) ).
tff(c_14711,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14586,c_14693]) ).
tff(c_14763,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14583,c_14588,c_14711]) ).
tff(c_14775,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14766,c_14763]) ).
tff(c_14595,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_101]) ).
tff(c_14780,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14775,c_14595]) ).
tff(c_14869,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_14780,c_2]) ).
tff(c_14592,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14581,c_14316]) ).
tff(c_14779,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_14775,c_14775,c_14592]) ).
tff(c_14989,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14869,c_14779]) ).
tff(c_14990,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_14995,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14990,c_4]) ).
tff(c_15678,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_15663,c_14995]) ).
tff(c_15013,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_14316,c_60]) ).
tff(c_15072,plain,
! [Z_190] : ( multiply(sk_c3,multiply(sk_c8,Z_190)) = multiply(sk_c4,Z_190) ),
inference(superposition,[status(thm),theory(equality)],[c_15013,c_15048]) ).
tff(c_15947,plain,
! [Z_190] : ( multiply(sk_c4,Z_190) = Z_190 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15866,c_2,c_15678,c_15072]) ).
tff(c_15869,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_15866,c_15708]) ).
tff(c_15948,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15947,c_15869]) ).
tff(c_15951,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15871,c_15948]) ).
tff(c_15953,plain,
multiply(sk_c8,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_16007,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_15953,c_44]) ).
tff(c_16111,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16108,c_16007]) ).
tff(c_16234,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16213,c_16111]) ).
tff(c_16117,plain,
multiply(sk_c6,sk_c6) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16108,c_15953]) ).
tff(c_16288,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16234,c_16213,c_16117]) ).
tff(c_16289,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_16319,plain,
! [X_219,Y_220,Z_221] : ( multiply(multiply(X_219,Y_220),Z_221) = multiply(X_219,multiply(Y_220,Z_221)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16352,plain,
! [Z_221] : ( multiply(sk_c6,multiply(sk_c5,Z_221)) = multiply(identity,Z_221) ),
inference(superposition,[status(thm),theory(equality)],[c_14320,c_16319]) ).
tff(c_16401,plain,
! [Z_224] : ( multiply(sk_c6,multiply(sk_c5,Z_224)) = Z_224 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16352]) ).
tff(c_16413,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16289,c_16401]) ).
tff(c_16302,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_15953,c_44]) ).
tff(c_16419,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16413,c_16302]) ).
tff(c_16430,plain,
multiply(sk_c8,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16419,c_14328]) ).
tff(c_16429,plain,
multiply(sk_c8,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16419,c_15953]) ).
tff(c_16470,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16430,c_16429]) ).
tff(c_16472,plain,
multiply(sk_c8,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_16505,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16472,c_8]) ).
tff(c_16652,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16648,c_16505]) ).
tff(c_16520,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16472,c_10]) ).
tff(c_16471,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_12,plain,
( ( multiply(sk_c3,sk_c8) = sk_c4 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_16525,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_16472,c_12]) ).
tff(c_16582,plain,
! [X_2,Z_228] : ( multiply(inverse(X_2),multiply(X_2,Z_228)) = multiply(identity,Z_228) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16540]) ).
tff(c_16660,plain,
! [X_232,Z_233] : ( multiply(inverse(X_232),multiply(X_232,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16582]) ).
tff(c_16696,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_16525,c_16660]) ).
tff(c_16741,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16520,c_16471,c_16696]) ).
tff(c_16500,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_16576,plain,
! [Z_228] : ( multiply(sk_c8,multiply(sk_c1,Z_228)) = multiply(identity,Z_228) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_16540]) ).
tff(c_16596,plain,
! [Z_229] : ( multiply(sk_c8,multiply(sk_c1,Z_229)) = Z_229 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16576]) ).
tff(c_16608,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_16500,c_16596]) ).
tff(c_16621,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X2_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X2_9,sk_c8)) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(X4_10,sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( sk_c8 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16608,c_16505,c_80]) ).
tff(c_16622,plain,
sk_c8 != sk_c6,
inference(splitLeft,[status(thm)],[c_16621]) ).
tff(c_16749,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16741,c_16622]) ).
tff(c_16813,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16652,c_16749]) ).
tff(c_16815,plain,
sk_c8 = sk_c6,
inference(splitRight,[status(thm)],[c_16621]) ).
tff(c_16612,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16608,c_16472]) ).
tff(c_16835,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16815,c_16612]) ).
tff(c_16836,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_16849,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_14316,c_60]) ).
tff(c_16476,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16471,c_4]) ).
tff(c_16877,plain,
! [X_235,Y_236,Z_237] : ( multiply(multiply(X_235,Y_236),Z_237) = multiply(X_235,multiply(Y_236,Z_237)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16904,plain,
! [Z_237] : ( multiply(sk_c8,multiply(sk_c3,Z_237)) = multiply(identity,Z_237) ),
inference(superposition,[status(thm),theory(equality)],[c_16476,c_16877]) ).
tff(c_16956,plain,
! [Z_240] : ( multiply(sk_c8,multiply(sk_c3,Z_240)) = Z_240 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16904]) ).
tff(c_16968,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_16849,c_16956]) ).
tff(c_16972,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16836,c_16968]) ).
tff(c_16842,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16472,c_8]) ).
tff(c_16978,plain,
multiply(sk_c6,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16972,c_16842]) ).
tff(c_16855,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_16472,c_16]) ).
tff(c_16976,plain,
multiply(sk_c5,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16972,c_16855]) ).
tff(c_16916,plain,
! [X_2,Z_237] : ( multiply(inverse(X_2),multiply(X_2,Z_237)) = multiply(identity,Z_237) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16877]) ).
tff(c_16928,plain,
! [X_2,Z_237] : ( multiply(inverse(X_2),multiply(X_2,Z_237)) = Z_237 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16916]) ).
tff(c_17110,plain,
multiply(inverse(sk_c5),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16976,c_16928]) ).
tff(c_17116,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16978,c_14315,c_17110]) ).
tff(c_16980,plain,
multiply(sk_c7,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16972,c_16836]) ).
tff(c_17094,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_16980,c_16928]) ).
tff(c_17100,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17094]) ).
tff(c_16977,plain,
multiply(sk_c3,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_16972,c_16849]) ).
tff(c_17189,plain,
multiply(sk_c3,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17116,c_17100,c_16977]) ).
tff(c_17122,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17116,c_17116,c_16978]) ).
tff(c_17128,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17116,c_16972]) ).
tff(c_16895,plain,
! [Z_237] : ( multiply(sk_c3,multiply(sk_c8,Z_237)) = multiply(sk_c4,Z_237) ),
inference(superposition,[status(thm),theory(equality)],[c_16849,c_16877]) ).
tff(c_17167,plain,
! [Z_237] : ( multiply(sk_c3,multiply(sk_c6,Z_237)) = Z_237 ),
inference(demodulation,[status(thm),theory(equality)],[c_17128,c_2,c_17100,c_16895]) ).
tff(c_17261,plain,
multiply(sk_c3,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17122,c_17167]) ).
tff(c_17270,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17189,c_17261]) ).
tff(c_16993,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(sk_c7,multiply(X2_9,sk_c7)) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c7 )
| ( multiply(sk_c7,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16972,c_16972,c_16972,c_16972,c_16972,c_16972,c_16972,c_16972,c_16972,c_16972,c_16972,c_80]) ).
tff(c_16994,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(splitLeft,[status(thm)],[c_16993]) ).
tff(c_17123,plain,
multiply(sk_c6,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17116,c_17116,c_16994]) ).
tff(c_17408,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17270,c_17123]) ).
tff(c_17410,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_16993]) ).
tff(c_16982,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16972,c_16472]) ).
tff(c_17558,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17410,c_16982]) ).
tff(c_17560,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_40,plain,
( ( multiply(sk_c5,sk_c6) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_17594,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_17560,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_17568,plain,
inverse(sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_17560,c_42]) ).
tff(c_17572,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17568,c_4]) ).
tff(c_17659,plain,
! [Z_250] : ( multiply(sk_c6,multiply(sk_c5,Z_250)) = multiply(identity,Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_17572,c_17632]) ).
tff(c_17681,plain,
! [Z_251] : ( multiply(sk_c6,multiply(sk_c5,Z_251)) = Z_251 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17659]) ).
tff(c_17693,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17594,c_17681]) ).
tff(c_18068,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17693,c_18041]) ).
tff(c_18108,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_18068]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_17599,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17560,c_32]) ).
tff(c_17697,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17693,c_17599]) ).
tff(c_34,plain,
( ( multiply(sk_c8,sk_c4) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_17609,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_17560,c_34]) ).
tff(c_17705,plain,
multiply(sk_c8,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17697,c_17609]) ).
tff(c_17559,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_36,plain,
( ( multiply(sk_c3,sk_c8) = sk_c4 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_17604,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_17560,c_36]) ).
tff(c_18077,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17604,c_18041]) ).
tff(c_18109,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17705,c_17559,c_18077]) ).
tff(c_18128,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18108,c_18109]) ).
tff(c_17564,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_17559,c_4]) ).
tff(c_17662,plain,
! [Z_250] : ( multiply(sk_c8,multiply(sk_c3,Z_250)) = multiply(identity,Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_17564,c_17632]) ).
tff(c_17733,plain,
! [Z_253] : ( multiply(sk_c8,multiply(sk_c3,Z_253)) = Z_253 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17662]) ).
tff(c_17745,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_17604,c_17733]) ).
tff(c_17749,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17705,c_17745]) ).
tff(c_17784,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17749,c_17693]) ).
tff(c_17893,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_17784,c_17679]) ).
tff(c_17899,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17893]) ).
tff(c_17718,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X2_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X2_9,sk_c8)) != sk_c6 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(X4_10,sk_c8) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17697,c_17697,c_17697,c_17697,c_17693,c_17697,c_80]) ).
tff(c_17719,plain,
multiply(sk_c8,sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_17718]) ).
tff(c_17782,plain,
multiply(sk_c6,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_17749,c_17719]) ).
tff(c_18018,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_17899,c_17782]) ).
tff(c_18019,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c6 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(X4_10,sk_c8) != sk_c6 )
| ( inverse(X2_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X2_9,sk_c8)) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_17718]) ).
tff(c_25809,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18341,c_18128,c_18108,c_18128,c_18341,c_18128,c_18108,c_2,c_18108,c_18108,c_18341,c_18128,c_18108,c_18108,c_18341,c_18128,c_18108,c_18108,c_18019]) ).
tff(c_25811,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25809]) ).
tff(c_18119,plain,
multiply(sk_c6,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18109,c_17564]) ).
tff(c_18237,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18128,c_18119]) ).
tff(c_18121,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_18109,c_17559]) ).
tff(c_18193,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18128,c_18121]) ).
tff(c_18238,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_18237,c_18193]) ).
tff(c_25813,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25811,c_18238]) ).
tff(c_25814,plain,
! [X2_9,X4_10,X3_7] :
( ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_25809]) ).
tff(c_30034,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25814]) ).
tff(c_30036,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_30034,c_18238]) ).
tff(c_30037,plain,
! [X4_10,X2_9] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(splitRight,[status(thm)],[c_25814]) ).
tff(c_30039,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_30037]) ).
tff(c_30041,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_30039,c_18238]) ).
tff(c_30790,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_30037]) ).
tff(c_30792,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_30790,c_18238]) ).
tff(c_30794,plain,
inverse(sk_c2) != sk_c8,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_76,plain,
( ( multiply(sk_c5,sk_c6) = sk_c8 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_30855,plain,
multiply(sk_c5,sk_c6) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_30794,c_76]) ).
tff(c_78,plain,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_30806,plain,
inverse(sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_30794,c_78]) ).
tff(c_30810,plain,
multiply(sk_c6,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_30806,c_4]) ).
tff(c_30909,plain,
! [Z_384] : ( multiply(sk_c6,multiply(sk_c5,Z_384)) = multiply(identity,Z_384) ),
inference(superposition,[status(thm),theory(equality)],[c_30810,c_30879]) ).
tff(c_30928,plain,
! [Z_385] : ( multiply(sk_c6,multiply(sk_c5,Z_385)) = Z_385 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30909]) ).
tff(c_30940,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_30855,c_30928]) ).
tff(c_31224,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_30940,c_31203]) ).
tff(c_31264,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_31224]) ).
tff(c_30793,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_72,plain,
( ( multiply(sk_c3,sk_c8) = sk_c4 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_30825,plain,
multiply(sk_c3,sk_c8) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_30794,c_72]) ).
tff(c_31242,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_30825,c_31203]) ).
tff(c_31266,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_30793,c_31242]) ).
tff(c_31358,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31264,c_2,c_31264,c_31266]) ).
tff(c_68,plain,
( ( multiply(sk_c6,sk_c8) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_30843,plain,
multiply(sk_c6,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_30794,c_68]) ).
tff(c_30944,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_30940,c_30843]) ).
tff(c_70,plain,
( ( multiply(sk_c8,sk_c4) = sk_c7 )
| ( inverse(sk_c2) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_30848,plain,
multiply(sk_c8,sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_30794,c_70]) ).
tff(c_31190,plain,
multiply(sk_c8,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_30944,c_30848]) ).
tff(c_31365,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31358,c_2,c_31264,c_31190]) ).
tff(c_31366,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31365,c_30944]) ).
tff(c_30954,plain,
multiply(sk_c8,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_30944,c_30848]) ).
tff(c_30798,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_30793,c_4]) ).
tff(c_30912,plain,
! [Z_384] : ( multiply(sk_c8,multiply(sk_c3,Z_384)) = multiply(identity,Z_384) ),
inference(superposition,[status(thm),theory(equality)],[c_30798,c_30879]) ).
tff(c_30989,plain,
! [Z_387] : ( multiply(sk_c8,multiply(sk_c3,Z_387)) = Z_387 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_30912]) ).
tff(c_31007,plain,
multiply(sk_c8,sk_c4) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_30825,c_30989]) ).
tff(c_31011,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_30954,c_31007]) ).
tff(c_31016,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_31011,c_30940]) ).
tff(c_31089,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_31016,c_30926]) ).
tff(c_31095,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_31089]) ).
tff(c_30952,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 )
| ( inverse(X2_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X2_9,sk_c8)) != sk_c7 )
| ( sk_c7 != sk_c6 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(X4_10,sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_30940,c_80]) ).
tff(c_30953,plain,
multiply(sk_c8,sk_c7) != sk_c6,
inference(splitLeft,[status(thm)],[c_30952]) ).
tff(c_30966,plain,
multiply(sk_c8,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_30944,c_30953]) ).
tff(c_31014,plain,
multiply(sk_c6,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_31011,c_30966]) ).
tff(c_31187,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31095,c_31014]) ).
tff(c_31188,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( sk_c7 != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c8 )
| ( multiply(X4_10,sk_c8) != sk_c6 )
| ( inverse(X2_9) != sk_c8 )
| ( multiply(sk_c8,multiply(X2_9,sk_c8)) != sk_c7 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(X5_6,sk_c6) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_30952]) ).
tff(c_38726,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_31497,c_31365,c_31264,c_31365,c_31497,c_31366,c_31264,c_2,c_31264,c_31264,c_31497,c_31365,c_31264,c_31264,c_31497,c_31366,c_31264,c_31264,c_31366,c_31365,c_31366,c_31365,c_2,c_31264,c_31188]) ).
tff(c_38728,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_38726]) ).
tff(c_31276,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31264,c_30793]) ).
tff(c_31288,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_31276,c_4]) ).
tff(c_31295,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_31288,c_30926]) ).
tff(c_31307,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_31295]) ).
tff(c_31311,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_31307,c_31276]) ).
tff(c_38730,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38728,c_31311]) ).
tff(c_38731,plain,
! [X2_9,X4_10,X3_7] :
( ( inverse(X2_9) != identity )
| ( identity != X2_9 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_38726]) ).
tff(c_41714,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_38731]) ).
tff(c_41716,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41714,c_31311]) ).
tff(c_41717,plain,
! [X4_10,X2_9] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(splitRight,[status(thm)],[c_38731]) ).
tff(c_41719,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_41717]) ).
tff(c_41721,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41719,c_31311]) ).
tff(c_42288,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_41717]) ).
tff(c_42290,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_42288,c_31311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP296-1 : TPTP v9.0.0. Released v2.5.0.
% 0.10/0.12 % 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.13/0.33 % Computer : n021.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Apr 7 21:41:43 EDT 2025
% 0.13/0.33 % CPUTime :
% 14.78/5.09 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.90/5.13
% 14.90/5.13 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------