%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP085-1 : TPTP v9.0.0. Bugfixed v2.7.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 : n003.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:24:57 PM UTC 2025
% Result : Unsatisfiable 18.06s 6.45s
% Output : CNFRefutation 18.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 2
% Syntax : Number of formulae : 80 ( 76 unt; 0 typ; 0 def)
% Number of atoms : 89 ( 85 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 31 ( 22 ~; 9 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 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 : 144 ( 144 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > c3 > b4 > b3 > b2 > b1 > a4 > a3 > a2 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
tff(b2,type,
b2: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b1,type,
b1: $i ).
tff(b4,type,
b4: $i ).
tff(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(a4,type,
a4: $i ).
tff(f_27,axiom,
! [X,Y,Z] : ( multiply(multiply(multiply(X,Y),Z),inverse(multiply(X,Z))) = Y ),
file(unknown,unknown) ).
tff(f_38,axiom,
( ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(a4,b4) != multiply(b4,a4) ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] : ( multiply(multiply(multiply(X_1,Y_2),Z_3),inverse(multiply(X_1,Z_3))) = Y_2 ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_5,plain,
! [X_4,Y_5,Z_6] : ( multiply(multiply(multiply(X_4,Y_5),Z_6),inverse(multiply(X_4,Z_6))) = Y_5 ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_70,plain,
! [X_10,Y_11,Z_12,Y_13] : ( multiply(multiply(multiply(multiply(multiply(X_10,Y_11),Z_12),Y_13),inverse(multiply(X_10,Z_12))),inverse(Y_11)) = Y_13 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_14,plain,
! [X_4,Y_5,Z_6,Y_2] : ( multiply(multiply(multiply(multiply(multiply(X_4,Y_5),Z_6),Y_2),inverse(multiply(X_4,Z_6))),inverse(Y_5)) = Y_2 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_79,plain,
! [Y_13,X_10,Y_11,Z_12] : ( multiply(multiply(Y_13,inverse(multiply(multiply(multiply(X_10,Y_11),Z_12),inverse(multiply(X_10,Z_12))))),inverse(Y_13)) = inverse(Y_11) ),
inference(superposition,[status(thm),theory(equality)],[c_70,c_14]) ).
tff(c_142,plain,
! [Y_13,Y_11] : ( multiply(multiply(Y_13,inverse(Y_11)),inverse(Y_13)) = inverse(Y_11) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79]) ).
tff(c_146,plain,
! [Y_14,Y_15] : ( multiply(multiply(Y_14,inverse(Y_15)),inverse(Y_14)) = inverse(Y_15) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79]) ).
tff(c_10981,plain,
! [Y_117,Y_118] : ( multiply(inverse(Y_117),inverse(multiply(Y_118,inverse(Y_117)))) = inverse(Y_118) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_146]) ).
tff(c_11,plain,
! [Y_5,X_4,Z_6] : ( multiply(Y_5,inverse(multiply(multiply(X_4,Y_5),inverse(multiply(X_4,Z_6))))) = Z_6 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_11006,plain,
! [X_4,Z_6] : ( inverse(multiply(X_4,inverse(multiply(X_4,Z_6)))) = Z_6 ),
inference(superposition,[status(thm),theory(equality)],[c_10981,c_11]) ).
tff(c_187,plain,
! [Y_11,Y_13] : ( multiply(inverse(Y_11),inverse(multiply(Y_13,inverse(Y_11)))) = inverse(Y_13) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_146]) ).
tff(c_11037,plain,
! [X_119,Z_120] : ( inverse(multiply(X_119,inverse(multiply(X_119,Z_120)))) = Z_120 ),
inference(superposition,[status(thm),theory(equality)],[c_10981,c_11]) ).
tff(c_12911,plain,
! [Y_145] : ( inverse(inverse(inverse(Y_145))) = inverse(Y_145) ),
inference(superposition,[status(thm),theory(equality)],[c_187,c_11037]) ).
tff(c_12947,plain,
! [X_4,Z_6] : ( inverse(multiply(X_4,inverse(multiply(X_4,Z_6)))) = inverse(inverse(Z_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_11006,c_12911]) ).
tff(c_12957,plain,
! [Z_6] : ( inverse(inverse(Z_6)) = Z_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_11006,c_12947]) ).
tff(c_11049,plain,
! [X_119,Z_120,Y_13] : ( multiply(inverse(multiply(X_119,inverse(multiply(X_119,Z_120)))),inverse(multiply(Y_13,Z_120))) = inverse(Y_13) ),
inference(superposition,[status(thm),theory(equality)],[c_11037,c_187]) ).
tff(c_14010,plain,
! [Z_162,Y_163] : ( multiply(Z_162,inverse(multiply(Y_163,Z_162))) = inverse(Y_163) ),
inference(demodulation,[status(thm),theory(equality)],[c_11006,c_11049]) ).
tff(c_14057,plain,
! [Y_5,Y_163] : ( multiply(Y_5,inverse(inverse(Y_163))) = multiply(Y_163,Y_5) ),
inference(superposition,[status(thm),theory(equality)],[c_14010,c_11]) ).
tff(c_14129,plain,
! [Y_5,Y_163] : ( multiply(Y_5,Y_163) = multiply(Y_163,Y_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_12957,c_14057]) ).
tff(c_14291,plain,
! [Y_167,Y_166] : ( multiply(Y_167,Y_166) = multiply(Y_166,Y_167) ),
inference(demodulation,[status(thm),theory(equality)],[c_12957,c_14057]) ).
tff(c_18731,plain,
! [Y_210,X_211,Y_212] : ( multiply(multiply(Y_210,multiply(X_211,Y_212)),inverse(multiply(X_211,Y_210))) = Y_212 ),
inference(superposition,[status(thm),theory(equality)],[c_14291,c_2]) ).
tff(c_11055,plain,
! [Y_13,Z_120,X_119] : ( multiply(multiply(Y_13,Z_120),inverse(Y_13)) = inverse(multiply(X_119,inverse(multiply(X_119,Z_120)))) ),
inference(superposition,[status(thm),theory(equality)],[c_11037,c_142]) ).
tff(c_11103,plain,
! [Y_13,Z_120] : ( multiply(multiply(Y_13,Z_120),inverse(Y_13)) = Z_120 ),
inference(demodulation,[status(thm),theory(equality)],[c_11006,c_11055]) ).
tff(c_14348,plain,
! [Y_166,Y_167] : ( multiply(multiply(Y_166,Y_167),inverse(Y_167)) = Y_166 ),
inference(superposition,[status(thm),theory(equality)],[c_14291,c_11103]) ).
tff(c_18776,plain,
! [Y_212,X_211,Y_210] : ( multiply(Y_212,inverse(inverse(multiply(X_211,Y_210)))) = multiply(Y_210,multiply(X_211,Y_212)) ),
inference(superposition,[status(thm),theory(equality)],[c_18731,c_14348]) ).
tff(c_40353,plain,
! [Y_320,X_319,Y_318] : ( multiply(Y_320,multiply(X_319,Y_318)) = multiply(Y_318,multiply(X_319,Y_320)) ),
inference(demodulation,[status(thm),theory(equality)],[c_12957,c_18776]) ).
tff(c_41565,plain,
! [Y_318,Y_163,Y_5] : ( multiply(Y_318,multiply(Y_163,Y_5)) = multiply(Y_163,multiply(Y_5,Y_318)) ),
inference(superposition,[status(thm),theory(equality)],[c_14129,c_40353]) ).
tff(c_19052,plain,
! [Y_212,X_211,Y_210] : ( multiply(Y_212,multiply(X_211,Y_210)) = multiply(Y_210,multiply(X_211,Y_212)) ),
inference(demodulation,[status(thm),theory(equality)],[c_12957,c_18776]) ).
tff(c_12999,plain,
! [Y_147,Z_148] : ( multiply(multiply(Y_147,Z_148),inverse(Y_147)) = Z_148 ),
inference(demodulation,[status(thm),theory(equality)],[c_11006,c_11055]) ).
tff(c_13124,plain,
! [Z_149,Y_150] : ( multiply(Z_149,inverse(multiply(Y_150,inverse(Y_150)))) = Z_149 ),
inference(superposition,[status(thm),theory(equality)],[c_12999,c_2]) ).
tff(c_13290,plain,
! [Y_151,Z_152] : ( multiply(multiply(Y_151,inverse(Y_151)),Z_152) = Z_152 ),
inference(superposition,[status(thm),theory(equality)],[c_11103,c_13124]) ).
tff(c_13389,plain,
! [Z_6,Z_152] : ( multiply(multiply(inverse(Z_6),Z_6),Z_152) = Z_152 ),
inference(superposition,[status(thm),theory(equality)],[c_12957,c_13290]) ).
tff(c_11107,plain,
! [Y_121] : ( inverse(inverse(inverse(Y_121))) = inverse(Y_121) ),
inference(superposition,[status(thm),theory(equality)],[c_187,c_11037]) ).
tff(c_11143,plain,
! [X_4,Z_6] : ( inverse(multiply(X_4,inverse(multiply(X_4,Z_6)))) = inverse(inverse(Z_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_11006,c_11107]) ).
tff(c_11153,plain,
! [Z_6] : ( inverse(inverse(Z_6)) = Z_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_11006,c_11143]) ).
tff(c_11277,plain,
! [Y_125,Z_126] : ( multiply(multiply(Y_125,Z_126),inverse(Y_125)) = Z_126 ),
inference(demodulation,[status(thm),theory(equality)],[c_11006,c_11055]) ).
tff(c_11762,plain,
! [Z_132,Y_133] : ( multiply(Z_132,inverse(multiply(Y_133,inverse(Y_133)))) = Z_132 ),
inference(superposition,[status(thm),theory(equality)],[c_11277,c_2]) ).
tff(c_11788,plain,
! [Y_133,Z_120] : ( multiply(multiply(Y_133,inverse(Y_133)),Z_120) = Z_120 ),
inference(superposition,[status(thm),theory(equality)],[c_11762,c_11103]) ).
tff(c_11926,plain,
! [Y_134,Z_135] : ( multiply(multiply(Y_134,inverse(Y_134)),Z_135) = Z_135 ),
inference(superposition,[status(thm),theory(equality)],[c_11762,c_11103]) ).
tff(c_12011,plain,
! [Y_134,Y_2,Z_135] : ( multiply(multiply(multiply(multiply(Y_134,inverse(Y_134)),Y_2),Z_135),inverse(Z_135)) = Y_2 ),
inference(superposition,[status(thm),theory(equality)],[c_11926,c_2]) ).
tff(c_12677,plain,
! [Y_143,Z_144] : ( multiply(multiply(Y_143,Z_144),inverse(Z_144)) = Y_143 ),
inference(demodulation,[status(thm),theory(equality)],[c_11788,c_12011]) ).
tff(c_12812,plain,
! [Z_120,Y_13] : ( multiply(Z_120,inverse(inverse(Y_13))) = multiply(Y_13,Z_120) ),
inference(superposition,[status(thm),theory(equality)],[c_11103,c_12677]) ).
tff(c_12865,plain,
! [Z_120,Y_13] : ( multiply(Z_120,Y_13) = multiply(Y_13,Z_120) ),
inference(demodulation,[status(thm),theory(equality)],[c_11153,c_12812]) ).
tff(c_210,plain,
! [Y_16,Y_17] : ( multiply(inverse(Y_16),inverse(multiply(Y_17,inverse(Y_16)))) = inverse(Y_17) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_146]) ).
tff(c_235,plain,
! [X_4,Z_6] : ( inverse(multiply(X_4,inverse(multiply(X_4,Z_6)))) = Z_6 ),
inference(superposition,[status(thm),theory(equality)],[c_210,c_11]) ).
tff(c_319,plain,
! [X_20,Z_21] : ( inverse(multiply(X_20,inverse(multiply(X_20,Z_21)))) = Z_21 ),
inference(superposition,[status(thm),theory(equality)],[c_210,c_11]) ).
tff(c_343,plain,
! [Y_13,Z_21,X_20] : ( multiply(multiply(Y_13,Z_21),inverse(Y_13)) = inverse(multiply(X_20,inverse(multiply(X_20,Z_21)))) ),
inference(superposition,[status(thm),theory(equality)],[c_319,c_142]) ).
tff(c_396,plain,
! [Y_13,Z_21] : ( multiply(multiply(Y_13,Z_21),inverse(Y_13)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_235,c_343]) ).
tff(c_400,plain,
! [Y_22] : ( inverse(inverse(inverse(Y_22))) = inverse(Y_22) ),
inference(superposition,[status(thm),theory(equality)],[c_187,c_319]) ).
tff(c_442,plain,
! [X_4,Z_6] : ( inverse(multiply(X_4,inverse(multiply(X_4,Z_6)))) = inverse(inverse(Z_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_235,c_400]) ).
tff(c_453,plain,
! [Z_6] : ( inverse(inverse(Z_6)) = Z_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_235,c_442]) ).
tff(c_177,plain,
! [Y_15,Y_14] : ( multiply(inverse(Y_15),inverse(multiply(Y_14,inverse(Y_14)))) = inverse(Y_15) ),
inference(superposition,[status(thm),theory(equality)],[c_146,c_2]) ).
tff(c_328,plain,
! [Z_21,Y_14,X_20] : ( multiply(Z_21,inverse(multiply(Y_14,inverse(Y_14)))) = inverse(multiply(X_20,inverse(multiply(X_20,Z_21)))) ),
inference(superposition,[status(thm),theory(equality)],[c_319,c_177]) ).
tff(c_649,plain,
! [Z_28,Y_29] : ( multiply(Z_28,inverse(multiply(Y_29,inverse(Y_29)))) = Z_28 ),
inference(demodulation,[status(thm),theory(equality)],[c_235,c_328]) ).
tff(c_688,plain,
! [Z_28,Z_6,Y_2,Y_29] : ( multiply(multiply(multiply(multiply(Z_28,Z_6),Y_2),inverse(multiply(Z_28,Z_6))),inverse(inverse(multiply(Y_29,inverse(Y_29))))) = Y_2 ),
inference(superposition,[status(thm),theory(equality)],[c_649,c_14]) ).
tff(c_796,plain,
! [Y_30,Y_31] : ( multiply(Y_30,multiply(Y_31,inverse(Y_31))) = Y_30 ),
inference(demodulation,[status(thm),theory(equality)],[c_396,c_453,c_688]) ).
tff(c_810,plain,
! [Y_31,Y_30] : ( multiply(Y_31,inverse(Y_31)) = multiply(Y_30,inverse(Y_30)) ),
inference(superposition,[status(thm),theory(equality)],[c_796,c_396]) ).
tff(c_872,plain,
! [Y_32,Z_33] : ( multiply(multiply(Y_32,inverse(Y_32)),Z_33) = Z_33 ),
inference(superposition,[status(thm),theory(equality)],[c_396,c_649]) ).
tff(c_927,plain,
! [Z_33,X_4,Y_5] : ( multiply(multiply(Z_33,inverse(multiply(X_4,inverse(multiply(X_4,Y_5))))),inverse(Y_5)) = Z_33 ),
inference(superposition,[status(thm),theory(equality)],[c_872,c_14]) ).
tff(c_1373,plain,
! [Z_40,Y_41] : ( multiply(multiply(Z_40,Y_41),inverse(Y_41)) = Z_40 ),
inference(demodulation,[status(thm),theory(equality)],[c_235,c_927]) ).
tff(c_1496,plain,
! [Z_21,Y_13] : ( multiply(Z_21,inverse(inverse(Y_13))) = multiply(Y_13,Z_21) ),
inference(superposition,[status(thm),theory(equality)],[c_396,c_1373]) ).
tff(c_1540,plain,
! [Z_21,Y_13] : ( multiply(Z_21,Y_13) = multiply(Y_13,Z_21) ),
inference(demodulation,[status(thm),theory(equality)],[c_453,c_1496]) ).
tff(c_4,plain,
( ( multiply(b4,a4) != multiply(a4,b4) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_208,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(splitLeft,[status(thm)],[c_4]) ).
tff(c_1547,plain,
multiply(b1,inverse(b1)) != multiply(a1,inverse(a1)),
inference(demodulation,[status(thm),theory(equality)],[c_1540,c_1540,c_208]) ).
tff(c_9047,plain,
! [Y_31] : ( multiply(a1,inverse(a1)) != multiply(Y_31,inverse(Y_31)) ),
inference(superposition,[status(thm),theory(equality)],[c_810,c_1547]) ).
tff(c_10955,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_9047]) ).
tff(c_10956,plain,
( ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(b4,a4) != multiply(a4,b4) ) ),
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_11106,plain,
multiply(b4,a4) != multiply(a4,b4),
inference(splitLeft,[status(thm)],[c_10956]) ).
tff(c_12883,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12865,c_11106]) ).
tff(c_12884,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 ) ),
inference(splitRight,[status(thm)],[c_10956]) ).
tff(c_12997,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(splitLeft,[status(thm)],[c_12884]) ).
tff(c_13671,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13389,c_12997]) ).
tff(c_13672,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitRight,[status(thm)],[c_12884]) ).
tff(c_14284,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_14129,c_13672]) ).
tff(c_40352,plain,
multiply(b3,multiply(a3,c3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_19052,c_14284]) ).
tff(c_42637,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_41565,c_40352]) ).
tff(c_42644,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14129,c_42637]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GRP085-1 : TPTP v9.0.0. Bugfixed v2.7.0.
% 0.06/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.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 21:16:03 EDT 2025
% 0.12/0.33 % CPUTime :
% 18.06/6.45 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.06/6.46
% 18.06/6.46 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------