%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS081+1 : TPTP v9.0.0. Released v3.1.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 : n016.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 07:07:17 PM UTC 2025
% Result : Unsatisfiable 16.38s 5.29s
% Output : CNFRefutation 16.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 6
% Syntax : Number of formulae : 258 ( 123 unt; 0 typ; 0 def)
% Number of atoms : 835 ( 477 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 838 ( 261 ~; 545 |; 26 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 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 : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-1 aty)
% Number of variables : 143 ( 134 !; 9 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rr > xsd_string > xsd_integer > cp5 > cp4 > cp3 > cp2 > cp1 > cp > cowlThing > cowlNothing > cUnsatisfiable > #nlpp > i2003_11_14_17_19_24236 > #skF_9 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_1 > #skF_8 > #skF_10 > #skF_13 > #skF_3 > #skF_11 > #skF_14 > #skF_12 > #skF_6
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(cp5,type,
cp5: $i > $o ).
tff(rr,type,
rr: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(i2003_11_14_17_19_24236,type,
i2003_11_14_17_19_24236: $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(cp4,type,
cp4: $i > $o ).
tff(cUnsatisfiable,type,
cUnsatisfiable: $i > $o ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(cp3,type,
cp3: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(cp,type,
cp: $i > $o ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff(cp2,type,
cp2: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(cp1,type,
cp1: $i > $o ).
tff(f_243,axiom,
cUnsatisfiable(i2003_11_14_17_19_24236),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
tff(f_205,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( rr(X,Y)
& cp3(Y) )
& ? [Y] :
( rr(X,Y)
& cp4(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp4(Y) )
& ? [Y] :
( rr(X,Y)
& cp2(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp5(Y) )
& ? [Y] :
( rr(X,Y)
& cp(Y)
& cp3(Y) )
& ? [Y] :
( rr(X,Y)
& cp1(Y) )
& ! [Y0,Y1,Y2,Y3,Y4] :
( ( rr(X,Y0)
& rr(X,Y1)
& rr(X,Y2)
& rr(X,Y3)
& rr(X,Y4) )
=> ( ( Y0 = Y1 )
| ( Y0 = Y2 )
| ( Y0 = Y3 )
| ( Y0 = Y4 )
| ( Y1 = Y2 )
| ( Y1 = Y3 )
| ( Y1 = Y4 )
| ( Y2 = Y3 )
| ( Y2 = Y4 )
| ( Y3 = Y4 ) ) )
& ? [Y] :
( rr(X,Y)
& cp1(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp2(Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
tff(f_241,axiom,
! [X] :
( cp4(X)
=> ~ cp5(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
tff(f_217,axiom,
! [X] :
( cp1(X)
=> ~ ( cp2(X)
| cp4(X)
| cp5(X)
| cp3(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
tff(f_227,axiom,
! [X] :
( cp2(X)
=> ~ ( cp4(X)
| cp5(X)
| cp3(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
tff(f_235,axiom,
! [X] :
( cp3(X)
=> ~ ( cp4(X)
| cp5(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
tff(c_132,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
inference(cnfTransformation,[status(thm)],[f_243]) ).
tff(c_42,plain,
! [X_31] :
( cp1('#skF_13'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_48,plain,
! [X_31] :
( cp1('#skF_12'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_36,plain,
! [X_31] :
( cp2('#skF_14'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_38,plain,
! [X_31] :
( rr(X_31,'#skF_14'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_70,plain,
! [X_31] :
( rr(X_31,'#skF_8'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_60,plain,
! [X_31] :
( rr(X_31,'#skF_10'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_76,plain,
! [X_31] :
( rr(X_31,'#skF_7'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_44,plain,
! [X_31] :
( rr(X_31,'#skF_13'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_50,plain,
! [X_31] :
( rr(X_31,'#skF_12'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_253,plain,
! [Y2_132,Y3_133,Y4_131,Y1_130,X_134,Y0_135] :
( ( Y4_131 = Y3_133 )
| ( Y4_131 = Y2_132 )
| ( Y3_133 = Y2_132 )
| ( Y4_131 = Y1_130 )
| ( Y3_133 = Y1_130 )
| ( Y2_132 = Y1_130 )
| ( Y4_131 = Y0_135 )
| ( Y3_133 = Y0_135 )
| ( Y2_132 = Y0_135 )
| ( Y1_130 = Y0_135 )
| ~ rr(X_134,Y4_131)
| ~ rr(X_134,Y3_133)
| ~ rr(X_134,Y2_132)
| ~ rr(X_134,Y1_130)
| ~ rr(X_134,Y0_135)
| ~ cUnsatisfiable(X_134) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_396,plain,
! [Y2_162,Y1_164,Y0_165,Y3_161,X_163] :
( ( Y3_161 = '#skF_12'(X_163) )
| ( Y2_162 = '#skF_12'(X_163) )
| ( Y3_161 = Y2_162 )
| ( Y1_164 = '#skF_12'(X_163) )
| ( Y3_161 = Y1_164 )
| ( Y2_162 = Y1_164 )
| ( Y0_165 = '#skF_12'(X_163) )
| ( Y3_161 = Y0_165 )
| ( Y2_162 = Y0_165 )
| ( Y1_164 = Y0_165 )
| ~ rr(X_163,Y3_161)
| ~ rr(X_163,Y2_162)
| ~ rr(X_163,Y1_164)
| ~ rr(X_163,Y0_165)
| ~ cUnsatisfiable(X_163) ),
inference(resolution,[status(thm)],[c_50,c_253]) ).
tff(c_1100,plain,
! [X_293,Y2_294,Y1_295,Y0_296] :
( ( '#skF_13'(X_293) = '#skF_12'(X_293) )
| ( Y2_294 = '#skF_12'(X_293) )
| ( Y2_294 = '#skF_13'(X_293) )
| ( Y1_295 = '#skF_12'(X_293) )
| ( Y1_295 = '#skF_13'(X_293) )
| ( Y2_294 = Y1_295 )
| ( Y0_296 = '#skF_12'(X_293) )
| ( Y0_296 = '#skF_13'(X_293) )
| ( Y2_294 = Y0_296 )
| ( Y1_295 = Y0_296 )
| ~ rr(X_293,Y2_294)
| ~ rr(X_293,Y1_295)
| ~ rr(X_293,Y0_296)
| ~ cUnsatisfiable(X_293) ),
inference(resolution,[status(thm)],[c_44,c_396]) ).
tff(c_2972,plain,
! [X_565,Y1_566,Y0_567] :
( ( '#skF_13'(X_565) = '#skF_12'(X_565) )
| ( '#skF_7'(X_565) = '#skF_12'(X_565) )
| ( '#skF_7'(X_565) = '#skF_13'(X_565) )
| ( Y1_566 = '#skF_12'(X_565) )
| ( Y1_566 = '#skF_13'(X_565) )
| ( Y1_566 = '#skF_7'(X_565) )
| ( Y0_567 = '#skF_12'(X_565) )
| ( Y0_567 = '#skF_13'(X_565) )
| ( Y0_567 = '#skF_7'(X_565) )
| ( Y1_566 = Y0_567 )
| ~ rr(X_565,Y1_566)
| ~ rr(X_565,Y0_567)
| ~ cUnsatisfiable(X_565) ),
inference(resolution,[status(thm)],[c_76,c_1100]) ).
tff(c_5425,plain,
! [X_765,Y0_766] :
( ( '#skF_13'(X_765) = '#skF_12'(X_765) )
| ( '#skF_7'(X_765) = '#skF_12'(X_765) )
| ( '#skF_7'(X_765) = '#skF_13'(X_765) )
| ( '#skF_10'(X_765) = '#skF_12'(X_765) )
| ( '#skF_10'(X_765) = '#skF_13'(X_765) )
| ( '#skF_7'(X_765) = '#skF_10'(X_765) )
| ( Y0_766 = '#skF_12'(X_765) )
| ( Y0_766 = '#skF_13'(X_765) )
| ( Y0_766 = '#skF_7'(X_765) )
| ( Y0_766 = '#skF_10'(X_765) )
| ~ rr(X_765,Y0_766)
| ~ cUnsatisfiable(X_765) ),
inference(resolution,[status(thm)],[c_60,c_2972]) ).
tff(c_9812,plain,
! [X_979] :
( ( '#skF_13'(X_979) = '#skF_12'(X_979) )
| ( '#skF_7'(X_979) = '#skF_12'(X_979) )
| ( '#skF_7'(X_979) = '#skF_13'(X_979) )
| ( '#skF_10'(X_979) = '#skF_12'(X_979) )
| ( '#skF_10'(X_979) = '#skF_13'(X_979) )
| ( '#skF_7'(X_979) = '#skF_10'(X_979) )
| ( '#skF_8'(X_979) = '#skF_12'(X_979) )
| ( '#skF_8'(X_979) = '#skF_13'(X_979) )
| ( '#skF_7'(X_979) = '#skF_8'(X_979) )
| ( '#skF_8'(X_979) = '#skF_10'(X_979) )
| ~ cUnsatisfiable(X_979) ),
inference(resolution,[status(thm)],[c_70,c_5425]) ).
tff(c_9816,plain,
( ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) ) ),
inference(resolution,[status(thm)],[c_132,c_9812]) ).
tff(c_9817,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_9816]) ).
tff(c_68,plain,
! [X_31] :
( cp4('#skF_8'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_9833,plain,
( cp4('#skF_10'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_9817,c_68]) ).
tff(c_9845,plain,
cp4('#skF_10'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9833]) ).
tff(c_175,plain,
! [X_96] :
( cp5('#skF_10'(X_96))
| ~ cUnsatisfiable(X_96) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_130,plain,
! [X_77] :
( ~ cp5(X_77)
| ~ cp4(X_77) ),
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_191,plain,
! [X_96] :
( ~ cp4('#skF_10'(X_96))
| ~ cUnsatisfiable(X_96) ),
inference(resolution,[status(thm)],[c_175,c_130]) ).
tff(c_9854,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_9845,c_191]) ).
tff(c_9867,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9854]) ).
tff(c_9869,plain,
'#skF_8'(i2003_11_14_17_19_24236) != '#skF_10'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_9816]) ).
tff(c_9868,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_9816]) ).
tff(c_9870,plain,
'#skF_13'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_9868]) ).
tff(c_9880,plain,
( cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_9870,c_42]) ).
tff(c_9888,plain,
cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9880]) ).
tff(c_52,plain,
! [X_31] :
( cp3('#skF_11'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_9874,plain,
( rr(i2003_11_14_17_19_24236,'#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_9870,c_44]) ).
tff(c_9884,plain,
rr(i2003_11_14_17_19_24236,'#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9874]) ).
tff(c_453,plain,
! [X_178,Y1_179,Y3_176,Y2_177,Y0_180] :
( ( Y3_176 = '#skF_8'(X_178) )
| ( Y2_177 = '#skF_8'(X_178) )
| ( Y3_176 = Y2_177 )
| ( Y1_179 = '#skF_8'(X_178) )
| ( Y3_176 = Y1_179 )
| ( Y2_177 = Y1_179 )
| ( Y0_180 = '#skF_8'(X_178) )
| ( Y3_176 = Y0_180 )
| ( Y2_177 = Y0_180 )
| ( Y1_179 = Y0_180 )
| ~ rr(X_178,Y3_176)
| ~ rr(X_178,Y2_177)
| ~ rr(X_178,Y1_179)
| ~ rr(X_178,Y0_180)
| ~ cUnsatisfiable(X_178) ),
inference(resolution,[status(thm)],[c_70,c_253]) ).
tff(c_477,plain,
! [X_31,Y2_177,Y1_179,Y0_180] :
( ( '#skF_8'(X_31) = '#skF_10'(X_31) )
| ( Y2_177 = '#skF_8'(X_31) )
| ( Y2_177 = '#skF_10'(X_31) )
| ( Y1_179 = '#skF_8'(X_31) )
| ( Y1_179 = '#skF_10'(X_31) )
| ( Y2_177 = Y1_179 )
| ( Y0_180 = '#skF_8'(X_31) )
| ( Y0_180 = '#skF_10'(X_31) )
| ( Y2_177 = Y0_180 )
| ( Y1_179 = Y0_180 )
| ~ rr(X_31,Y2_177)
| ~ rr(X_31,Y1_179)
| ~ rr(X_31,Y0_180)
| ~ cUnsatisfiable(X_31) ),
inference(resolution,[status(thm)],[c_60,c_453]) ).
tff(c_10508,plain,
! [Y1_179,Y0_180] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = Y0_180 )
| ~ rr(i2003_11_14_17_19_24236,Y1_179)
| ~ rr(i2003_11_14_17_19_24236,Y0_180)
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(resolution,[status(thm)],[c_9884,c_477]) ).
tff(c_11401,plain,
! [Y1_179,Y0_180] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = Y0_180 )
| ~ rr(i2003_11_14_17_19_24236,Y1_179)
| ~ rr(i2003_11_14_17_19_24236,Y0_180) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_10508]) ).
tff(c_11402,plain,
! [Y1_179,Y0_180] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = Y0_180 )
| ~ rr(i2003_11_14_17_19_24236,Y1_179)
| ~ rr(i2003_11_14_17_19_24236,Y0_180) ),
inference(negUnitSimplification,[status(thm)],[c_9869,c_11401]) ).
tff(c_11483,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11402]) ).
tff(c_114,plain,
! [X_74] :
( ~ cp5(X_74)
| ~ cp1(X_74) ),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_188,plain,
! [X_96] :
( ~ cp1('#skF_10'(X_96))
| ~ cUnsatisfiable(X_96) ),
inference(resolution,[status(thm)],[c_175,c_114]) ).
tff(c_11548,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11483,c_188]) ).
tff(c_11565,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9888,c_11548]) ).
tff(c_11566,plain,
! [Y1_179,Y0_180] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y1_179 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_180 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_179 = Y0_180 )
| ~ rr(i2003_11_14_17_19_24236,Y1_179)
| ~ rr(i2003_11_14_17_19_24236,Y0_180) ),
inference(splitRight,[status(thm)],[c_11402]) ).
tff(c_11568,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11566]) ).
tff(c_151,plain,
! [X_92] :
( cp4('#skF_8'(X_92))
| ~ cUnsatisfiable(X_92) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_116,plain,
! [X_74] :
( ~ cp4(X_74)
| ~ cp1(X_74) ),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_163,plain,
! [X_92] :
( ~ cp1('#skF_8'(X_92))
| ~ cUnsatisfiable(X_92) ),
inference(resolution,[status(thm)],[c_151,c_116]) ).
tff(c_11633,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11568,c_163]) ).
tff(c_11647,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9888,c_11633]) ).
tff(c_11650,plain,
! [Y1_984,Y0_985] :
( ( Y1_984 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y1_984 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y1_984 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y1_984 = Y0_985 )
| ~ rr(i2003_11_14_17_19_24236,Y1_984)
| ~ rr(i2003_11_14_17_19_24236,Y0_985) ),
inference(splitRight,[status(thm)],[c_11566]) ).
tff(c_11655,plain,
! [Y0_985] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_985)
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(resolution,[status(thm)],[c_38,c_11650]) ).
tff(c_11686,plain,
! [Y0_985] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_985) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11655]) ).
tff(c_11770,plain,
'#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11686]) ).
tff(c_206,plain,
! [X_99] :
( cp2('#skF_14'(X_99))
| ~ cUnsatisfiable(X_99) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_118,plain,
! [X_74] :
( ~ cp2(X_74)
| ~ cp1(X_74) ),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_210,plain,
! [X_99] :
( ~ cp1('#skF_14'(X_99))
| ~ cUnsatisfiable(X_99) ),
inference(resolution,[status(thm)],[c_206,c_118]) ).
tff(c_11777,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11770,c_210]) ).
tff(c_11787,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9888,c_11777]) ).
tff(c_11788,plain,
! [Y0_985] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_985) ),
inference(splitRight,[status(thm)],[c_11686]) ).
tff(c_11797,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11788]) ).
tff(c_124,plain,
! [X_75] :
( ~ cp4(X_75)
| ~ cp2(X_75) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_161,plain,
! [X_92] :
( ~ cp2('#skF_8'(X_92))
| ~ cUnsatisfiable(X_92) ),
inference(resolution,[status(thm)],[c_151,c_124]) ).
tff(c_11810,plain,
( ~ cp2('#skF_14'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11797,c_161]) ).
tff(c_11824,plain,
~ cp2('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11810]) ).
tff(c_11832,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_36,c_11824]) ).
tff(c_11836,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11832]) ).
tff(c_11837,plain,
! [Y0_985] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_985 = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_985) ),
inference(splitRight,[status(thm)],[c_11788]) ).
tff(c_11846,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11837]) ).
tff(c_122,plain,
! [X_75] :
( ~ cp5(X_75)
| ~ cp2(X_75) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_189,plain,
! [X_96] :
( ~ cp2('#skF_10'(X_96))
| ~ cUnsatisfiable(X_96) ),
inference(resolution,[status(thm)],[c_175,c_122]) ).
tff(c_11856,plain,
( ~ cp2('#skF_14'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11846,c_189]) ).
tff(c_11874,plain,
~ cp2('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11856]) ).
tff(c_11886,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_36,c_11874]) ).
tff(c_11890,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11886]) ).
tff(c_11900,plain,
! [Y0_990] :
( ( Y0_990 = '#skF_8'(i2003_11_14_17_19_24236) )
| ( Y0_990 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_990 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_990 = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_990) ),
inference(splitRight,[status(thm)],[c_11837]) ).
tff(c_11915,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(resolution,[status(thm)],[c_76,c_11900]) ).
tff(c_11956,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11915]) ).
tff(c_11980,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11956]) ).
tff(c_192,plain,
! [X_97] :
( cp4('#skF_7'(X_97))
| ~ cUnsatisfiable(X_97) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_202,plain,
! [X_97] :
( ~ cp2('#skF_7'(X_97))
| ~ cUnsatisfiable(X_97) ),
inference(resolution,[status(thm)],[c_192,c_124]) ).
tff(c_11988,plain,
( ~ cp2('#skF_14'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11980,c_202]) ).
tff(c_12006,plain,
~ cp2('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11988]) ).
tff(c_12018,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_36,c_12006]) ).
tff(c_12022,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_12018]) ).
tff(c_12023,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_11956]) ).
tff(c_12032,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_12023]) ).
tff(c_11649,plain,
'#skF_8'(i2003_11_14_17_19_24236) != '#skF_12'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_11566]) ).
tff(c_56,plain,
! [X_31] :
( rr(X_31,'#skF_11'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_80,plain,
! [X_31] :
( rr(X_31,'#skF_6'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_1982,plain,
! [X_467,Y2_468,Y1_469,Y0_470] :
( ( '#skF_8'(X_467) = '#skF_6'(X_467) )
| ( Y2_468 = '#skF_8'(X_467) )
| ( Y2_468 = '#skF_6'(X_467) )
| ( Y1_469 = '#skF_8'(X_467) )
| ( Y1_469 = '#skF_6'(X_467) )
| ( Y2_468 = Y1_469 )
| ( Y0_470 = '#skF_8'(X_467) )
| ( Y0_470 = '#skF_6'(X_467) )
| ( Y2_468 = Y0_470 )
| ( Y1_469 = Y0_470 )
| ~ rr(X_467,Y2_468)
| ~ rr(X_467,Y1_469)
| ~ rr(X_467,Y0_470)
| ~ cUnsatisfiable(X_467) ),
inference(resolution,[status(thm)],[c_80,c_453]) ).
tff(c_2352,plain,
! [X_505,Y1_506,Y0_507] :
( ( '#skF_8'(X_505) = '#skF_6'(X_505) )
| ( '#skF_8'(X_505) = '#skF_12'(X_505) )
| ( '#skF_12'(X_505) = '#skF_6'(X_505) )
| ( Y1_506 = '#skF_8'(X_505) )
| ( Y1_506 = '#skF_6'(X_505) )
| ( Y1_506 = '#skF_12'(X_505) )
| ( Y0_507 = '#skF_8'(X_505) )
| ( Y0_507 = '#skF_6'(X_505) )
| ( Y0_507 = '#skF_12'(X_505) )
| ( Y1_506 = Y0_507 )
| ~ rr(X_505,Y1_506)
| ~ rr(X_505,Y0_507)
| ~ cUnsatisfiable(X_505) ),
inference(resolution,[status(thm)],[c_50,c_1982]) ).
tff(c_5220,plain,
! [X_755,Y0_756] :
( ( '#skF_8'(X_755) = '#skF_6'(X_755) )
| ( '#skF_8'(X_755) = '#skF_12'(X_755) )
| ( '#skF_12'(X_755) = '#skF_6'(X_755) )
| ( '#skF_7'(X_755) = '#skF_8'(X_755) )
| ( '#skF_7'(X_755) = '#skF_6'(X_755) )
| ( '#skF_7'(X_755) = '#skF_12'(X_755) )
| ( Y0_756 = '#skF_8'(X_755) )
| ( Y0_756 = '#skF_6'(X_755) )
| ( Y0_756 = '#skF_12'(X_755) )
| ( Y0_756 = '#skF_7'(X_755) )
| ~ rr(X_755,Y0_756)
| ~ cUnsatisfiable(X_755) ),
inference(resolution,[status(thm)],[c_76,c_2352]) ).
tff(c_9890,plain,
! [X_981] :
( ( '#skF_8'(X_981) = '#skF_6'(X_981) )
| ( '#skF_8'(X_981) = '#skF_12'(X_981) )
| ( '#skF_12'(X_981) = '#skF_6'(X_981) )
| ( '#skF_7'(X_981) = '#skF_8'(X_981) )
| ( '#skF_7'(X_981) = '#skF_6'(X_981) )
| ( '#skF_7'(X_981) = '#skF_12'(X_981) )
| ( '#skF_8'(X_981) = '#skF_11'(X_981) )
| ( '#skF_11'(X_981) = '#skF_6'(X_981) )
| ( '#skF_11'(X_981) = '#skF_12'(X_981) )
| ( '#skF_7'(X_981) = '#skF_11'(X_981) )
| ~ cUnsatisfiable(X_981) ),
inference(resolution,[status(thm)],[c_56,c_5220]) ).
tff(c_9894,plain,
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_12'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) ) ),
inference(resolution,[status(thm)],[c_132,c_9890]) ).
tff(c_11718,plain,
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_12'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_6'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) ) ),
inference(negUnitSimplification,[status(thm)],[c_11649,c_9894]) ).
tff(c_11719,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_11718]) ).
tff(c_128,plain,
! [X_76] :
( ~ cp4(X_76)
| ~ cp3(X_76) ),
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_203,plain,
! [X_97] :
( ~ cp3('#skF_7'(X_97))
| ~ cUnsatisfiable(X_97) ),
inference(resolution,[status(thm)],[c_192,c_128]) ).
tff(c_11732,plain,
( ~ cp3('#skF_11'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_11719,c_203]) ).
tff(c_11748,plain,
~ cp3('#skF_11'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11732]) ).
tff(c_11756,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_52,c_11748]) ).
tff(c_11760,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_11756]) ).
tff(c_11762,plain,
'#skF_7'(i2003_11_14_17_19_24236) != '#skF_11'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_11718]) ).
tff(c_12034,plain,
'#skF_8'(i2003_11_14_17_19_24236) != '#skF_11'(i2003_11_14_17_19_24236),
inference(demodulation,[status(thm),theory(equality)],[c_12032,c_11762]) ).
tff(c_11838,plain,
'#skF_8'(i2003_11_14_17_19_24236) != '#skF_14'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_11788]) ).
tff(c_11789,plain,
'#skF_14'(i2003_11_14_17_19_24236) != '#skF_12'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_11686]) ).
tff(c_11567,plain,
'#skF_10'(i2003_11_14_17_19_24236) != '#skF_12'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_11402]) ).
tff(c_11892,plain,
'#skF_10'(i2003_11_14_17_19_24236) != '#skF_14'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_11837]) ).
tff(c_12038,plain,
( rr(i2003_11_14_17_19_24236,'#skF_8'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_12032,c_76]) ).
tff(c_12057,plain,
rr(i2003_11_14_17_19_24236,'#skF_8'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_12038]) ).
tff(c_511,plain,
! [Y2_187,Y0_190,Y3_186,X_188,Y1_189] :
( ( Y3_186 = '#skF_10'(X_188) )
| ( Y2_187 = '#skF_10'(X_188) )
| ( Y3_186 = Y2_187 )
| ( Y1_189 = '#skF_10'(X_188) )
| ( Y3_186 = Y1_189 )
| ( Y2_187 = Y1_189 )
| ( Y0_190 = '#skF_10'(X_188) )
| ( Y3_186 = Y0_190 )
| ( Y2_187 = Y0_190 )
| ( Y1_189 = Y0_190 )
| ~ rr(X_188,Y3_186)
| ~ rr(X_188,Y2_187)
| ~ rr(X_188,Y1_189)
| ~ rr(X_188,Y0_190)
| ~ cUnsatisfiable(X_188) ),
inference(resolution,[status(thm)],[c_60,c_253]) ).
tff(c_774,plain,
! [X_237,Y2_238,Y1_239,Y0_240] :
( ( '#skF_10'(X_237) = '#skF_14'(X_237) )
| ( Y2_238 = '#skF_10'(X_237) )
| ( Y2_238 = '#skF_14'(X_237) )
| ( Y1_239 = '#skF_10'(X_237) )
| ( Y1_239 = '#skF_14'(X_237) )
| ( Y2_238 = Y1_239 )
| ( Y0_240 = '#skF_10'(X_237) )
| ( Y0_240 = '#skF_14'(X_237) )
| ( Y2_238 = Y0_240 )
| ( Y1_239 = Y0_240 )
| ~ rr(X_237,Y2_238)
| ~ rr(X_237,Y1_239)
| ~ rr(X_237,Y0_240)
| ~ cUnsatisfiable(X_237) ),
inference(resolution,[status(thm)],[c_38,c_511]) ).
tff(c_4212,plain,
! [X_685,Y1_686,Y0_687] :
( ( '#skF_10'(X_685) = '#skF_14'(X_685) )
| ( '#skF_10'(X_685) = '#skF_12'(X_685) )
| ( '#skF_14'(X_685) = '#skF_12'(X_685) )
| ( Y1_686 = '#skF_10'(X_685) )
| ( Y1_686 = '#skF_14'(X_685) )
| ( Y1_686 = '#skF_12'(X_685) )
| ( Y0_687 = '#skF_10'(X_685) )
| ( Y0_687 = '#skF_14'(X_685) )
| ( Y0_687 = '#skF_12'(X_685) )
| ( Y1_686 = Y0_687 )
| ~ rr(X_685,Y1_686)
| ~ rr(X_685,Y0_687)
| ~ cUnsatisfiable(X_685) ),
inference(resolution,[status(thm)],[c_50,c_774]) ).
tff(c_4235,plain,
! [X_31,Y0_687] :
( ( '#skF_10'(X_31) = '#skF_14'(X_31) )
| ( '#skF_10'(X_31) = '#skF_12'(X_31) )
| ( '#skF_14'(X_31) = '#skF_12'(X_31) )
| ( '#skF_10'(X_31) = '#skF_11'(X_31) )
| ( '#skF_11'(X_31) = '#skF_14'(X_31) )
| ( '#skF_11'(X_31) = '#skF_12'(X_31) )
| ( Y0_687 = '#skF_10'(X_31) )
| ( Y0_687 = '#skF_14'(X_31) )
| ( Y0_687 = '#skF_12'(X_31) )
| ( Y0_687 = '#skF_11'(X_31) )
| ~ rr(X_31,Y0_687)
| ~ cUnsatisfiable(X_31) ),
inference(resolution,[status(thm)],[c_56,c_4212]) ).
tff(c_12199,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) )
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(resolution,[status(thm)],[c_12057,c_4235]) ).
tff(c_12922,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_12199]) ).
tff(c_12923,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) ) ),
inference(negUnitSimplification,[status(thm)],[c_12034,c_11649,c_11838,c_9869,c_11789,c_11567,c_11892,c_12922]) ).
tff(c_13914,plain,
'#skF_11'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_12923]) ).
tff(c_165,plain,
! [X_94] :
( cp3('#skF_11'(X_94))
| ~ cUnsatisfiable(X_94) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_112,plain,
! [X_74] :
( ~ cp3(X_74)
| ~ cp1(X_74) ),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_172,plain,
! [X_94] :
( ~ cp1('#skF_11'(X_94))
| ~ cUnsatisfiable(X_94) ),
inference(resolution,[status(thm)],[c_165,c_112]) ).
tff(c_13925,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_13914,c_172]) ).
tff(c_13940,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9888,c_13925]) ).
tff(c_13941,plain,
( ( '#skF_11'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_12923]) ).
tff(c_13950,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_11'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_13941]) ).
tff(c_126,plain,
! [X_76] :
( ~ cp5(X_76)
| ~ cp3(X_76) ),
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_190,plain,
! [X_96] :
( ~ cp3('#skF_10'(X_96))
| ~ cUnsatisfiable(X_96) ),
inference(resolution,[status(thm)],[c_175,c_126]) ).
tff(c_13965,plain,
( ~ cp3('#skF_11'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_13950,c_190]) ).
tff(c_13982,plain,
~ cp3('#skF_11'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_13965]) ).
tff(c_14015,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_52,c_13982]) ).
tff(c_14019,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14015]) ).
tff(c_14020,plain,
'#skF_11'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_13941]) ).
tff(c_120,plain,
! [X_75] :
( ~ cp3(X_75)
| ~ cp2(X_75) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_173,plain,
! [X_94] :
( ~ cp2('#skF_11'(X_94))
| ~ cUnsatisfiable(X_94) ),
inference(resolution,[status(thm)],[c_165,c_120]) ).
tff(c_14031,plain,
( ~ cp2('#skF_14'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_14020,c_173]) ).
tff(c_14046,plain,
~ cp2('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14031]) ).
tff(c_14056,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_36,c_14046]) ).
tff(c_14060,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14056]) ).
tff(c_14061,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_12023]) ).
tff(c_14070,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_14061]) ).
tff(c_204,plain,
! [X_97] :
( ~ cp1('#skF_7'(X_97))
| ~ cUnsatisfiable(X_97) ),
inference(resolution,[status(thm)],[c_192,c_116]) ).
tff(c_14083,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_14070,c_204]) ).
tff(c_14101,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_9888,c_14083]) ).
tff(c_14102,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_14061]) ).
tff(c_74,plain,
! [X_31] :
( cp4('#skF_7'(X_31))
| ~ cUnsatisfiable(X_31) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_14132,plain,
( cp4('#skF_10'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_14102,c_74]) ).
tff(c_14146,plain,
cp4('#skF_10'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14132]) ).
tff(c_14157,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_14146,c_191]) ).
tff(c_14170,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14157]) ).
tff(c_14172,plain,
'#skF_13'(i2003_11_14_17_19_24236) != '#skF_12'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_9868]) ).
tff(c_14171,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_9868]) ).
tff(c_14173,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_8'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_14171]) ).
tff(c_14184,plain,
( rr(i2003_11_14_17_19_24236,'#skF_8'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_14173,c_76]) ).
tff(c_14203,plain,
rr(i2003_11_14_17_19_24236,'#skF_8'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14184]) ).
tff(c_1394,plain,
! [X_351,Y2_352,Y1_353,Y0_354] :
( ( '#skF_10'(X_351) = '#skF_12'(X_351) )
| ( Y2_352 = '#skF_10'(X_351) )
| ( Y2_352 = '#skF_12'(X_351) )
| ( Y1_353 = '#skF_10'(X_351) )
| ( Y1_353 = '#skF_12'(X_351) )
| ( Y2_352 = Y1_353 )
| ( Y0_354 = '#skF_10'(X_351) )
| ( Y0_354 = '#skF_12'(X_351) )
| ( Y2_352 = Y0_354 )
| ( Y1_353 = Y0_354 )
| ~ rr(X_351,Y2_352)
| ~ rr(X_351,Y1_353)
| ~ rr(X_351,Y0_354)
| ~ cUnsatisfiable(X_351) ),
inference(resolution,[status(thm)],[c_50,c_511]) ).
tff(c_1419,plain,
! [X_31,Y1_353,Y0_354] :
( ( '#skF_10'(X_31) = '#skF_12'(X_31) )
| ( '#skF_10'(X_31) = '#skF_13'(X_31) )
| ( '#skF_13'(X_31) = '#skF_12'(X_31) )
| ( Y1_353 = '#skF_10'(X_31) )
| ( Y1_353 = '#skF_12'(X_31) )
| ( Y1_353 = '#skF_13'(X_31) )
| ( Y0_354 = '#skF_10'(X_31) )
| ( Y0_354 = '#skF_12'(X_31) )
| ( Y0_354 = '#skF_13'(X_31) )
| ( Y1_353 = Y0_354 )
| ~ rr(X_31,Y1_353)
| ~ rr(X_31,Y0_354)
| ~ cUnsatisfiable(X_31) ),
inference(resolution,[status(thm)],[c_44,c_1394]) ).
tff(c_14731,plain,
! [Y0_354] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_354)
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(resolution,[status(thm)],[c_14203,c_1419]) ).
tff(c_15632,plain,
! [Y0_354] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_354) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14731]) ).
tff(c_15633,plain,
! [Y0_354] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_354) ),
inference(negUnitSimplification,[status(thm)],[c_9869,c_14172,c_15632]) ).
tff(c_15908,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_15633]) ).
tff(c_14190,plain,
( ~ cp1('#skF_8'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_14173,c_204]) ).
tff(c_14207,plain,
~ cp1('#skF_8'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14190]) ).
tff(c_15919,plain,
~ cp1('#skF_13'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_15908,c_14207]) ).
tff(c_15966,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_42,c_15919]) ).
tff(c_15970,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_15966]) ).
tff(c_15971,plain,
! [Y0_354] :
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_354) ),
inference(splitRight,[status(thm)],[c_15633]) ).
tff(c_15979,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_15971]) ).
tff(c_15993,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_15979,c_188]) ).
tff(c_16009,plain,
~ cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_15993]) ).
tff(c_16039,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_48,c_16009]) ).
tff(c_16043,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16039]) ).
tff(c_16044,plain,
! [Y0_354] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_354) ),
inference(splitRight,[status(thm)],[c_15971]) ).
tff(c_16052,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16044]) ).
tff(c_16058,plain,
~ cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_16052,c_14207]) ).
tff(c_16105,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_48,c_16058]) ).
tff(c_16109,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16105]) ).
tff(c_16110,plain,
! [Y0_354] :
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_354 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_354) ),
inference(splitRight,[status(thm)],[c_16044]) ).
tff(c_16112,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16110]) ).
tff(c_16134,plain,
( ~ cp1('#skF_13'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16112,c_188]) ).
tff(c_16150,plain,
~ cp1('#skF_13'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16134]) ).
tff(c_16181,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_42,c_16150]) ).
tff(c_16185,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16181]) ).
tff(c_16188,plain,
! [Y0_1008] :
( ( Y0_1008 = '#skF_10'(i2003_11_14_17_19_24236) )
| ( Y0_1008 = '#skF_12'(i2003_11_14_17_19_24236) )
| ( Y0_1008 = '#skF_13'(i2003_11_14_17_19_24236) )
| ( Y0_1008 = '#skF_8'(i2003_11_14_17_19_24236) )
| ~ rr(i2003_11_14_17_19_24236,Y0_1008) ),
inference(splitRight,[status(thm)],[c_16110]) ).
tff(c_16195,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(resolution,[status(thm)],[c_38,c_16188]) ).
tff(c_16234,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16195]) ).
tff(c_16268,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16234]) ).
tff(c_14199,plain,
( cp4('#skF_8'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_14173,c_74]) ).
tff(c_14213,plain,
cp4('#skF_8'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_14199]) ).
tff(c_16280,plain,
cp4('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_16268,c_14213]) ).
tff(c_16325,plain,
~ cp2('#skF_14'(i2003_11_14_17_19_24236)),
inference(resolution,[status(thm)],[c_16280,c_124]) ).
tff(c_16330,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_36,c_16325]) ).
tff(c_16334,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16330]) ).
tff(c_16335,plain,
( ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) )
| ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16234]) ).
tff(c_16337,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16335]) ).
tff(c_16348,plain,
( ~ cp2('#skF_14'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16337,c_189]) ).
tff(c_16366,plain,
~ cp2('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16348]) ).
tff(c_16378,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_36,c_16366]) ).
tff(c_16382,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16378]) ).
tff(c_16383,plain,
( ( '#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_13'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16335]) ).
tff(c_16392,plain,
'#skF_13'(i2003_11_14_17_19_24236) = '#skF_14'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16383]) ).
tff(c_16406,plain,
( cp1('#skF_14'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16392,c_42]) ).
tff(c_16414,plain,
cp1('#skF_14'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16406]) ).
tff(c_16425,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_16414,c_210]) ).
tff(c_16429,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16425]) ).
tff(c_16430,plain,
'#skF_14'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_16383]) ).
tff(c_16441,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16430,c_210]) ).
tff(c_16450,plain,
~ cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16441]) ).
tff(c_16456,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_48,c_16450]) ).
tff(c_16460,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16456]) ).
tff(c_16461,plain,
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_14171]) ).
tff(c_16470,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16461]) ).
tff(c_16481,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16470,c_204]) ).
tff(c_16498,plain,
~ cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16481]) ).
tff(c_16527,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_48,c_16498]) ).
tff(c_16531,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16527]) ).
tff(c_16532,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16461]) ).
tff(c_16534,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16532]) ).
tff(c_16556,plain,
( ~ cp1('#skF_13'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16534,c_163]) ).
tff(c_16569,plain,
~ cp1('#skF_13'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16556]) ).
tff(c_16593,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_42,c_16569]) ).
tff(c_16597,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16593]) ).
tff(c_16598,plain,
( ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16532]) ).
tff(c_16600,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16598]) ).
tff(c_16612,plain,
( ~ cp1('#skF_13'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16600,c_204]) ).
tff(c_16629,plain,
~ cp1('#skF_13'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16612]) ).
tff(c_16658,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_42,c_16629]) ).
tff(c_16662,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16658]) ).
tff(c_16663,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16598]) ).
tff(c_16665,plain,
'#skF_8'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16663]) ).
tff(c_16681,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16665,c_163]) ).
tff(c_16694,plain,
~ cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16681]) ).
tff(c_16719,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_48,c_16694]) ).
tff(c_16723,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16719]) ).
tff(c_16724,plain,
( ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16663]) ).
tff(c_16733,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_12'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16724]) ).
tff(c_16747,plain,
( ~ cp1('#skF_12'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16733,c_188]) ).
tff(c_16763,plain,
~ cp1('#skF_12'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16747]) ).
tff(c_16778,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_48,c_16763]) ).
tff(c_16782,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16778]) ).
tff(c_16783,plain,
( ( '#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236) )
| ( '#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236) ) ),
inference(splitRight,[status(thm)],[c_16724]) ).
tff(c_16785,plain,
'#skF_7'(i2003_11_14_17_19_24236) = '#skF_10'(i2003_11_14_17_19_24236),
inference(splitLeft,[status(thm)],[c_16783]) ).
tff(c_16814,plain,
( cp4('#skF_10'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16785,c_74]) ).
tff(c_16828,plain,
cp4('#skF_10'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16814]) ).
tff(c_16839,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_16828,c_191]) ).
tff(c_16852,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16839]) ).
tff(c_16853,plain,
'#skF_10'(i2003_11_14_17_19_24236) = '#skF_13'(i2003_11_14_17_19_24236),
inference(splitRight,[status(thm)],[c_16783]) ).
tff(c_16869,plain,
( ~ cp1('#skF_13'(i2003_11_14_17_19_24236))
| ~ cUnsatisfiable(i2003_11_14_17_19_24236) ),
inference(superposition,[status(thm),theory(equality)],[c_16853,c_188]) ).
tff(c_16885,plain,
~ cp1('#skF_13'(i2003_11_14_17_19_24236)),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16869]) ).
tff(c_16916,plain,
~ cUnsatisfiable(i2003_11_14_17_19_24236),
inference(resolution,[status(thm)],[c_42,c_16885]) ).
tff(c_16920,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_132,c_16916]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS081+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/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.32 % Computer : n016.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.33 % CPULimit : 300
% 0.18/0.33 % WCLimit : 300
% 0.18/0.33 % DateTime : Tue Apr 8 02:58:23 EDT 2025
% 0.18/0.33 % CPUTime :
% 16.38/5.29 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.48/5.31
% 16.48/5.31 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------