%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP092-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n024.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:58 PM UTC 2025
% Result : Unsatisfiable 21.26s 8.34s
% Output : CNFRefutation 21.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 5
% Syntax : Number of formulae : 55 ( 51 unt; 0 typ; 0 def)
% Number of atoms : 64 ( 62 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 25 ( 16 ~; 9 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 4 ( 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 : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 95 ( 95 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > identity > 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(divide,type,
divide: ( $i * $i ) > $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(identity,type,
identity: $i ).
tff(f_35,axiom,
! [X] : ( identity = divide(X,X) ),
file(unknown,unknown) ).
tff(f_32,axiom,
! [X,Z] : ( inverse(X) = divide(divide(Z,Z),X) ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [X,Y,Z] : ( multiply(X,Y) = divide(X,divide(divide(Z,Z),Y)) ),
file(unknown,unknown) ).
tff(f_26,axiom,
! [X,Y,Z] : ( divide(divide(X,Y),divide(divide(X,Z),Y)) = Z ),
file(unknown,unknown) ).
tff(f_46,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_8,plain,
! [X_9] : ( divide(X_9,X_9) = identity ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_6,plain,
! [Z_8,X_7] : ( divide(divide(Z_8,Z_8),X_7) = inverse(X_7) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_11,plain,
! [X_7] : ( divide(identity,X_7) = inverse(X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_4,plain,
! [X_4,Z_6,Y_5] : ( divide(X_4,divide(divide(Z_6,Z_6),Y_5)) = multiply(X_4,Y_5) ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_12,plain,
! [X_4,Y_5] : ( divide(X_4,inverse(Y_5)) = multiply(X_4,Y_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_11,c_8,c_4]) ).
tff(c_70,plain,
! [X_14,Y_15,Z_16] : ( divide(divide(X_14,Y_15),divide(divide(X_14,Z_16),Y_15)) = Z_16 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_116,plain,
! [X_9,Y_15] : ( divide(divide(X_9,Y_15),divide(identity,Y_15)) = X_9 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_70]) ).
tff(c_205,plain,
! [X_21,Y_22] : ( multiply(divide(X_21,Y_22),Y_22) = X_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_11,c_116]) ).
tff(c_223,plain,
! [X_9] : ( multiply(identity,X_9) = X_9 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_205]) ).
tff(c_42,plain,
! [X_12,Y_13] : ( divide(X_12,inverse(Y_13)) = multiply(X_12,Y_13) ),
inference(demodulation,[status(thm),theory(equality)],[c_11,c_8,c_4]) ).
tff(c_63,plain,
! [Y_13] : ( inverse(inverse(Y_13)) = multiply(identity,Y_13) ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_42]) ).
tff(c_238,plain,
! [Y_13] : ( inverse(inverse(Y_13)) = Y_13 ),
inference(demodulation,[status(thm),theory(equality)],[c_223,c_63]) ).
tff(c_110,plain,
! [Y_15,X_7] : ( divide(divide(identity,Y_15),divide(inverse(X_7),Y_15)) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_70]) ).
tff(c_429,plain,
! [Y_30,X_31] : ( divide(inverse(Y_30),divide(inverse(X_31),Y_30)) = X_31 ),
inference(demodulation,[status(thm),theory(equality)],[c_11,c_110]) ).
tff(c_473,plain,
! [X_31] : ( divide(inverse(inverse(X_31)),identity) = X_31 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_429]) ).
tff(c_480,plain,
! [X_31] : ( divide(X_31,identity) = X_31 ),
inference(demodulation,[status(thm),theory(equality)],[c_238,c_473]) ).
tff(c_483,plain,
! [X_32] : ( divide(X_32,identity) = X_32 ),
inference(demodulation,[status(thm),theory(equality)],[c_238,c_473]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] : ( divide(divide(X_1,Y_2),divide(divide(X_1,Z_3),Y_2)) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_503,plain,
! [X_32,Z_3] : ( divide(X_32,divide(divide(X_32,Z_3),identity)) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_483,c_2]) ).
tff(c_583,plain,
! [X_34,Z_35] : ( divide(X_34,divide(X_34,Z_35)) = Z_35 ),
inference(demodulation,[status(thm),theory(equality)],[c_480,c_503]) ).
tff(c_127,plain,
! [X_9,Y_15] : ( multiply(divide(X_9,Y_15),Y_15) = X_9 ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_11,c_116]) ).
tff(c_603,plain,
! [Z_35,X_34] : ( multiply(Z_35,divide(X_34,Z_35)) = X_34 ),
inference(superposition,[status(thm),theory(equality)],[c_583,c_127]) ).
tff(c_463,plain,
! [Y_5,X_31] : ( divide(inverse(inverse(Y_5)),multiply(inverse(X_31),Y_5)) = X_31 ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_429]) ).
tff(c_854,plain,
! [Y_41,X_42] : ( divide(Y_41,multiply(inverse(X_42),Y_41)) = X_42 ),
inference(demodulation,[status(thm),theory(equality)],[c_238,c_463]) ).
tff(c_900,plain,
! [X_34,X_42] : ( divide(divide(X_34,inverse(X_42)),X_34) = X_42 ),
inference(superposition,[status(thm),theory(equality)],[c_603,c_854]) ).
tff(c_932,plain,
! [X_43,X_44] : ( divide(multiply(X_43,X_44),X_43) = X_44 ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_900]) ).
tff(c_954,plain,
! [X_44,X_43] : ( multiply(X_44,X_43) = multiply(X_43,X_44) ),
inference(superposition,[status(thm),theory(equality)],[c_932,c_127]) ).
tff(c_217,plain,
! [X_4,Y_5] : ( multiply(multiply(X_4,Y_5),inverse(Y_5)) = X_4 ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_205]) ).
tff(c_113,plain,
! [X_9,Z_16] : ( divide(identity,divide(divide(X_9,Z_16),X_9)) = Z_16 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_70]) ).
tff(c_438,plain,
! [X_31,Y_30] : ( divide(identity,divide(X_31,inverse(Y_30))) = divide(inverse(X_31),Y_30) ),
inference(superposition,[status(thm),theory(equality)],[c_429,c_113]) ).
tff(c_475,plain,
! [X_31,Y_30] : ( divide(inverse(X_31),Y_30) = inverse(multiply(X_31,Y_30)) ),
inference(demodulation,[status(thm),theory(equality)],[c_11,c_12,c_438]) ).
tff(c_4190,plain,
! [X_97,Y_98,Y_99,Z_100] : ( divide(divide(divide(X_97,Y_98),Y_99),divide(Z_100,Y_99)) = divide(divide(X_97,Z_100),Y_98) ),
inference(superposition,[status(thm),theory(equality)],[c_70,c_2]) ).
tff(c_4488,plain,
! [X_7,Y_99,Z_100] : ( divide(divide(inverse(X_7),Y_99),divide(Z_100,Y_99)) = divide(divide(identity,Z_100),X_7) ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_4190]) ).
tff(c_4537,plain,
! [X_7,Y_99,Z_100] : ( divide(divide(inverse(X_7),Y_99),divide(Z_100,Y_99)) = divide(inverse(Z_100),X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_11,c_4488]) ).
tff(c_32434,plain,
! [X_271,Y_272,Z_273] : ( inverse(multiply(multiply(X_271,Y_272),divide(Z_273,Y_272))) = inverse(multiply(Z_273,X_271)) ),
inference(demodulation,[status(thm),theory(equality)],[c_475,c_475,c_475,c_4537]) ).
tff(c_32572,plain,
! [X_271,Y_272,Z_273] : ( multiply(multiply(X_271,Y_272),divide(Z_273,Y_272)) = inverse(inverse(multiply(Z_273,X_271))) ),
inference(superposition,[status(thm),theory(equality)],[c_32434,c_238]) ).
tff(c_33547,plain,
! [X_277,Y_278,Z_279] : ( multiply(multiply(X_277,Y_278),divide(Z_279,Y_278)) = multiply(Z_279,X_277) ),
inference(demodulation,[status(thm),theory(equality)],[c_238,c_32572]) ).
tff(c_33971,plain,
! [X_4,Z_279,Y_5] : ( multiply(X_4,divide(Z_279,inverse(Y_5))) = multiply(Z_279,multiply(X_4,Y_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_217,c_33547]) ).
tff(c_34121,plain,
! [Z_279,X_4,Y_5] : ( multiply(Z_279,multiply(X_4,Y_5)) = multiply(X_4,multiply(Z_279,Y_5)) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_33971]) ).
tff(c_172,plain,
! [X_19,Y_20] : ( multiply(divide(X_19,Y_20),Y_20) = X_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_11,c_116]) ).
tff(c_190,plain,
! [X_9] : ( multiply(identity,X_9) = X_9 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_172]) ).
tff(c_53,plain,
! [Y_13] : ( multiply(inverse(Y_13),Y_13) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_42,c_8]) ).
tff(c_10,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_46]) ).
tff(c_144,plain,
( ( multiply(b4,a4) != multiply(a4,b4) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(identity,a2) != a2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_53,c_53,c_53,c_10]) ).
tff(c_145,plain,
multiply(identity,a2) != a2,
inference(splitLeft,[status(thm)],[c_144]) ).
tff(c_198,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_190,c_145]) ).
tff(c_199,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(b4,a4) != multiply(a4,b4) ) ),
inference(splitRight,[status(thm)],[c_144]) ).
tff(c_5589,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_954,c_954,c_199]) ).
tff(c_36210,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_34121,c_5589]) ).
tff(c_36213,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_954,c_36210]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GRP092-1 : TPTP v9.0.0. Bugfixed v2.7.0.
% 0.00/0.10 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.30 % Computer : n024.cluster.edu
% 0.08/0.30 % Model : x86_64 x86_64
% 0.08/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.30 % Memory : 8042.1875MB
% 0.08/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.30 % CPULimit : 300
% 0.08/0.30 % WCLimit : 300
% 0.08/0.30 % DateTime : Mon Apr 7 21:16:51 EDT 2025
% 0.08/0.30 % CPUTime :
% 21.26/8.34 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.26/8.34
% 21.26/8.34 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------