%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN014-1 : TPTP v9.0.0. Released v1.0.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 : 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 10:01:52 PM UTC 2025
% Result : Unsatisfiable 3.79s 2.02s
% Output : CNFRefutation 4.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 15
% Syntax : Number of formulae : 86 ( 27 unt; 0 typ; 0 def)
% Number of atoms : 212 ( 136 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 196 ( 70 ~; 126 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-1 aty)
% Number of variables : 43 ( 43 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ element > #nlpp > g > f > n > m > k > j
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(m,type,
m: $i ).
tff(j,type,
j: $i ).
tff(element,type,
element: ( $i * $i ) > $o ).
tff(k,type,
k: $i ).
tff(f,type,
f: $i > $i ).
tff(g,type,
g: $i > $i ).
tff(n,type,
n: $i ).
tff(f_37,axiom,
! [Y] :
( ( Y = j )
| ( Y != k )
| element(Y,j) ),
file(unknown,unknown) ).
tff(f_30,axiom,
( ( n = k )
| ( m = k ) ),
file(unknown,unknown) ).
tff(f_27,axiom,
m != n,
file(unknown,unknown) ).
tff(f_136,axiom,
! [Y] :
( ( Y = k )
| ( Y != m )
| element(Y,k) ),
file(unknown,unknown) ).
tff(f_44,axiom,
! [Y] :
( ( Y = j )
| ( Y = k )
| ~ element(Y,j) ),
file(unknown,unknown) ).
tff(f_95,axiom,
! [Y] :
( ( Y = n )
| element(Y,n)
| ( g(Y) != n ) ),
file(unknown,unknown) ).
tff(f_114,axiom,
! [Y] :
( ( Y = n )
| element(Y,n)
| element(g(Y),Y) ),
file(unknown,unknown) ).
tff(f_152,axiom,
! [Y] :
( ( Y = k )
| ( Y = m )
| ( Y = n )
| ~ element(Y,k) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [Y] :
( ( Y = m )
| ~ element(Y,m)
| ( f(Y) != Y ) ),
file(unknown,unknown) ).
tff(f_52,axiom,
! [Y] :
( ( Y = m )
| ~ element(Y,m)
| ( f(Y) != m ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
! [Y] :
( ( Y = m )
| ~ element(Y,m)
| element(f(Y),Y) ),
file(unknown,unknown) ).
tff(f_102,axiom,
! [Y] :
( ( Y = n )
| element(Y,n)
| ( g(Y) != Y ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
! [Y] :
( ( Y = k )
| ( Y != n )
| element(Y,k) ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [Y] :
( ( Y = m )
| ~ element(Y,m)
| element(Y,f(Y)) ),
file(unknown,unknown) ).
tff(f_88,axiom,
! [Y,V1] :
( ( Y = m )
| element(Y,m)
| ( V1 = m )
| ( V1 = Y )
| ~ element(Y,V1)
| ~ element(V1,Y) ),
file(unknown,unknown) ).
tff(c_6,plain,
( element(k,j)
| ( k = j ) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_43,plain,
k = j,
inference(splitLeft,[status(thm)],[c_6]) ).
tff(c_4,plain,
( ( m = k )
| ( n = k ) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_35,plain,
n = k,
inference(splitLeft,[status(thm)],[c_4]) ).
tff(c_2,plain,
n != m,
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_36,plain,
m != k,
inference(demodulation,[status(thm),theory(equality)],[c_35,c_2]) ).
tff(c_45,plain,
m != j,
inference(demodulation,[status(thm),theory(equality)],[c_43,c_36]) ).
tff(c_30,plain,
( element(m,k)
| ( m = k ) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_42,plain,
element(m,k),
inference(negUnitSimplification,[status(thm)],[c_36,c_30]) ).
tff(c_44,plain,
element(m,j),
inference(demodulation,[status(thm),theory(equality)],[c_43,c_42]) ).
tff(c_8,plain,
! [Y_2] :
( ~ element(Y_2,j)
| ( k = Y_2 )
| ( j = Y_2 ) ),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_51,plain,
! [Y_2] :
( ~ element(Y_2,j)
| ( j = Y_2 )
| ( j = Y_2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43,c_8]) ).
tff(c_59,plain,
m = j,
inference(resolution,[status(thm)],[c_44,c_51]) ).
tff(c_63,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_45,c_45,c_59]) ).
tff(c_65,plain,
k != j,
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_20,plain,
! [Y_9] :
( ( g(Y_9) != n )
| element(Y_9,n)
| ( n = Y_9 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_78,plain,
! [Y_9] :
( ( g(Y_9) != k )
| element(Y_9,k)
| ( k = Y_9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35,c_35,c_35,c_20]) ).
tff(c_64,plain,
element(k,j),
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_26,plain,
! [Y_12] :
( element(g(Y_12),Y_12)
| element(Y_12,n)
| ( n = Y_12 ) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_101,plain,
! [Y_28] :
( element(g(Y_28),Y_28)
| element(Y_28,k)
| ( k = Y_28 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35,c_35,c_26]) ).
tff(c_117,plain,
( ( g(j) = k )
| ( g(j) = j )
| element(j,k)
| ( k = j ) ),
inference(resolution,[status(thm)],[c_101,c_8]) ).
tff(c_128,plain,
( ( g(j) = k )
| ( g(j) = j )
| element(j,k) ),
inference(negUnitSimplification,[status(thm)],[c_65,c_117]) ).
tff(c_156,plain,
element(j,k),
inference(splitLeft,[status(thm)],[c_128]) ).
tff(c_34,plain,
! [Y_17] :
( ~ element(Y_17,k)
| ( n = Y_17 )
| ( m = Y_17 )
| ( k = Y_17 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_80,plain,
! [Y_17] :
( ~ element(Y_17,k)
| ( k = Y_17 )
| ( m = Y_17 )
| ( k = Y_17 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35,c_34]) ).
tff(c_159,plain,
( ( m = j )
| ( k = j ) ),
inference(resolution,[status(thm)],[c_156,c_80]) ).
tff(c_162,plain,
m = j,
inference(negUnitSimplification,[status(thm)],[c_65,c_65,c_159]) ).
tff(c_12,plain,
! [Y_4] :
( ( f(Y_4) != Y_4 )
| ~ element(Y_4,m)
| ( m = Y_4 ) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_223,plain,
! [Y_36] :
( ( f(Y_36) != Y_36 )
| ~ element(Y_36,j)
| ( j = Y_36 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_162,c_162,c_12]) ).
tff(c_230,plain,
( ( f(k) != k )
| ( k = j ) ),
inference(resolution,[status(thm)],[c_64,c_223]) ).
tff(c_236,plain,
f(k) != k,
inference(negUnitSimplification,[status(thm)],[c_65,c_230]) ).
tff(c_10,plain,
! [Y_3] :
( ( f(Y_3) != m )
| ~ element(Y_3,m)
| ( m = Y_3 ) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_209,plain,
! [Y_35] :
( ( f(Y_35) != j )
| ~ element(Y_35,j)
| ( j = Y_35 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_162,c_162,c_162,c_10]) ).
tff(c_216,plain,
( ( f(k) != j )
| ( k = j ) ),
inference(resolution,[status(thm)],[c_64,c_209]) ).
tff(c_222,plain,
f(k) != j,
inference(negUnitSimplification,[status(thm)],[c_65,c_216]) ).
tff(c_131,plain,
! [Y_30] :
( element(f(Y_30),Y_30)
| ~ element(Y_30,m)
| ( m = Y_30 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_135,plain,
( ( f(k) = m )
| ( f(k) = k )
| ~ element(k,m)
| ( m = k ) ),
inference(resolution,[status(thm)],[c_131,c_80]) ).
tff(c_150,plain,
( ( f(k) = m )
| ( f(k) = k )
| ~ element(k,m) ),
inference(negUnitSimplification,[status(thm)],[c_36,c_135]) ).
tff(c_270,plain,
( ( f(k) = j )
| ( f(k) = k ) ),
inference(demodulation,[status(thm),theory(equality)],[c_64,c_162,c_162,c_150]) ).
tff(c_271,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_236,c_222,c_270]) ).
tff(c_273,plain,
~ element(j,k),
inference(splitRight,[status(thm)],[c_128]) ).
tff(c_276,plain,
( ( g(j) != k )
| ( k = j ) ),
inference(resolution,[status(thm)],[c_78,c_273]) ).
tff(c_282,plain,
g(j) != k,
inference(negUnitSimplification,[status(thm)],[c_65,c_276]) ).
tff(c_22,plain,
! [Y_10] :
( ( g(Y_10) != Y_10 )
| element(Y_10,n)
| ( n = Y_10 ) ),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_74,plain,
! [Y_10] :
( ( g(Y_10) != Y_10 )
| element(Y_10,k)
| ( k = Y_10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35,c_35,c_22]) ).
tff(c_279,plain,
( ( g(j) != j )
| ( k = j ) ),
inference(resolution,[status(thm)],[c_74,c_273]) ).
tff(c_285,plain,
g(j) != j,
inference(negUnitSimplification,[status(thm)],[c_65,c_279]) ).
tff(c_272,plain,
( ( g(j) = j )
| ( g(j) = k ) ),
inference(splitRight,[status(thm)],[c_128]) ).
tff(c_318,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_282,c_285,c_272]) ).
tff(c_320,plain,
n != k,
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_32,plain,
( element(n,k)
| ( n = k ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_353,plain,
element(n,k),
inference(negUnitSimplification,[status(thm)],[c_320,c_32]) ).
tff(c_319,plain,
m = k,
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_364,plain,
! [Y_43] :
( ( f(Y_43) != k )
| ~ element(Y_43,k)
| ( k = Y_43 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_319,c_319,c_10]) ).
tff(c_367,plain,
( ( f(n) != k )
| ( n = k ) ),
inference(resolution,[status(thm)],[c_353,c_364]) ).
tff(c_370,plain,
f(n) != k,
inference(negUnitSimplification,[status(thm)],[c_320,c_367]) ).
tff(c_374,plain,
! [Y_46] :
( ( f(Y_46) != Y_46 )
| ~ element(Y_46,k)
| ( k = Y_46 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_319,c_12]) ).
tff(c_377,plain,
( ( f(n) != n )
| ( n = k ) ),
inference(resolution,[status(thm)],[c_353,c_374]) ).
tff(c_380,plain,
f(n) != n,
inference(negUnitSimplification,[status(thm)],[c_320,c_377]) ).
tff(c_16,plain,
! [Y_6] :
( element(f(Y_6),Y_6)
| ~ element(Y_6,m)
| ( m = Y_6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_383,plain,
! [Y_6] :
( element(f(Y_6),Y_6)
| ~ element(Y_6,k)
| ( k = Y_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_319,c_16]) ).
tff(c_14,plain,
! [Y_5] :
( element(Y_5,f(Y_5))
| ~ element(Y_5,m)
| ( m = Y_5 ) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_381,plain,
! [Y_5] :
( element(Y_5,f(Y_5))
| ~ element(Y_5,k)
| ( k = Y_5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_319,c_14]) ).
tff(c_18,plain,
! [V1_8,Y_7] :
( ~ element(V1_8,Y_7)
| ~ element(Y_7,V1_8)
| ( Y_7 = V1_8 )
| ( m = V1_8 )
| element(Y_7,m)
| ( m = Y_7 ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_508,plain,
! [V1_54,Y_55] :
( ~ element(V1_54,Y_55)
| ~ element(Y_55,V1_54)
| ( Y_55 = V1_54 )
| ( k = V1_54 )
| element(Y_55,k)
| ( k = Y_55 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_319,c_319,c_18]) ).
tff(c_574,plain,
! [Y_56] :
( ~ element(f(Y_56),Y_56)
| ( f(Y_56) = Y_56 )
| element(f(Y_56),k)
| ( f(Y_56) = k )
| ~ element(Y_56,k)
| ( k = Y_56 ) ),
inference(resolution,[status(thm)],[c_381,c_508]) ).
tff(c_634,plain,
! [Y_59] :
( ( f(Y_59) = Y_59 )
| element(f(Y_59),k)
| ( f(Y_59) = k )
| ~ element(Y_59,k)
| ( k = Y_59 ) ),
inference(resolution,[status(thm)],[c_383,c_574]) ).
tff(c_404,plain,
! [Y_17] :
( ~ element(Y_17,k)
| ( n = Y_17 )
| ( k = Y_17 )
| ( k = Y_17 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_34]) ).
tff(c_657,plain,
! [Y_60] :
( ( f(Y_60) = n )
| ( f(Y_60) = Y_60 )
| ( f(Y_60) = k )
| ~ element(Y_60,k)
| ( k = Y_60 ) ),
inference(resolution,[status(thm)],[c_634,c_404]) ).
tff(c_671,plain,
( ( f(n) = n )
| ( f(n) = k )
| ( n = k ) ),
inference(resolution,[status(thm)],[c_353,c_657]) ).
tff(c_681,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_320,c_370,c_380,c_380,c_671]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN014-1 : TPTP v9.0.0. Released v1.0.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.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 : Wed Apr 9 06:51:44 EDT 2025
% 0.13/0.33 % CPUTime :
% 3.79/2.02 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.79/2.03
% 3.79/2.03 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------