%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS107+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 : n020.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:21 PM UTC 2025
% Result : Unsatisfiable 4.65s 1.96s
% Output : CNFRefutation 4.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 9
% Syntax : Number of formulae : 41 ( 12 unt; 0 typ; 0 def)
% Number of atoms : 82 ( 5 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 74 ( 33 ~; 26 |; 7 &)
% ( 5 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 23 ( 21 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 42 ( 37 !; 5 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rrxa > rrx4a > rrx4 > rrx3a > rrx3 > rrx2a > rrx2 > rrx1a > rrx1 > rrx > ra_Px1 > xsd_string > xsd_integer > cowlThing > cowlNothing > cc2 > cc1 > ca_Cx1xcomp > ca_Cx1 > ca_Ax2 > cUnsatisfiable > #nlpp > i2003_11_14_17_21_01226 > #skF_5 > #skF_2 > #skF_4 > #skF_1 > #skF_3
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(rrxa,type,
rrxa: ( $i * $i ) > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(i2003_11_14_17_21_01226,type,
i2003_11_14_17_21_01226: $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(rrx2,type,
rrx2: ( $i * $i ) > $o ).
tff(ca_Ax2,type,
ca_Ax2: $i > $o ).
tff(rrx1a,type,
rrx1a: ( $i * $i ) > $o ).
tff(rrx,type,
rrx: ( $i * $i ) > $o ).
tff(cc1,type,
cc1: $i > $o ).
tff(ca_Cx1xcomp,type,
ca_Cx1xcomp: $i > $o ).
tff(rrx2a,type,
rrx2a: ( $i * $i ) > $o ).
tff(cUnsatisfiable,type,
cUnsatisfiable: $i > $o ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff(rrx4,type,
rrx4: ( $i * $i ) > $o ).
tff(rrx3a,type,
rrx3a: ( $i * $i ) > $o ).
tff(rrx4a,type,
rrx4a: ( $i * $i ) > $o ).
tff(rrx1,type,
rrx1: ( $i * $i ) > $o ).
tff(ra_Px1,type,
ra_Px1: ( $i * $i ) > $o ).
tff(rrx3,type,
rrx3: ( $i * $i ) > $o ).
tff(ca_Cx1,type,
ca_Cx1: $i > $o ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff(cc2,type,
cc2: $i > $o ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(f_311,axiom,
cUnsatisfiable(i2003_11_14_17_21_01226),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
tff(f_246,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( rrx3(X,Y)
& cc1(Y) )
& ? [Y] :
( rrx4(X,Y)
& cc2(Y) )
& ca_Cx1(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
tff(f_331,axiom,
! [X,Y] :
( rrx4(X,Y)
=> rrx(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_17) ).
tff(f_343,axiom,
! [X,Y] :
( rrx3(X,Y)
=> rrx(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
tff(f_281,axiom,
! [X,Y,Z] :
( ( rrx(X,Y)
& rrx(X,Z) )
=> ( Y = Z ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
tff(f_253,axiom,
! [X] :
( ca_Ax2(X)
<=> ( cc2(X)
& cc1(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
tff(f_267,axiom,
! [X] :
( ca_Cx1xcomp(X)
<=> ? [Y] :
( rrx3(X,Y)
& ca_Ax2(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
tff(f_259,axiom,
! [X] :
( ca_Cx1(X)
<=> ? [Y0] : ra_Px1(X,Y0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
tff(f_274,axiom,
! [X] :
( ca_Cx1xcomp(X)
<=> ~ ? [Y] : ra_Px1(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
tff(c_116,plain,
cUnsatisfiable(i2003_11_14_17_21_01226),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_76,plain,
! [X_89] :
( ca_Cx1(X_89)
| ~ cUnsatisfiable(X_89) ),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_82,plain,
! [X_89] :
( cc1('#skF_1'(X_89))
| ~ cUnsatisfiable(X_89) ),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_201,plain,
! [X_172] :
( rrx4(X_172,'#skF_2'(X_172))
| ~ cUnsatisfiable(X_172) ),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_126,plain,
! [X_132,Y_133] :
( rrx(X_132,Y_133)
| ~ rrx4(X_132,Y_133) ),
inference(cnfTransformation,[status(thm)],[f_331]) ).
tff(c_208,plain,
! [X_172] :
( rrx(X_172,'#skF_2'(X_172))
| ~ cUnsatisfiable(X_172) ),
inference(resolution,[status(thm)],[c_201,c_126]) ).
tff(c_84,plain,
! [X_89] :
( rrx3(X_89,'#skF_1'(X_89))
| ~ cUnsatisfiable(X_89) ),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_173,plain,
! [X_166,Y_167] :
( rrx(X_166,Y_167)
| ~ rrx3(X_166,Y_167) ),
inference(cnfTransformation,[status(thm)],[f_343]) ).
tff(c_181,plain,
! [X_89] :
( rrx(X_89,'#skF_1'(X_89))
| ~ cUnsatisfiable(X_89) ),
inference(resolution,[status(thm)],[c_84,c_173]) ).
tff(c_234,plain,
! [Z_190,Y_191,X_192] :
( ( Z_190 = Y_191 )
| ~ rrx(X_192,Z_190)
| ~ rrx(X_192,Y_191) ),
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_310,plain,
! [Y_215,X_216] :
( ( Y_215 = '#skF_1'(X_216) )
| ~ rrx(X_216,Y_215)
| ~ cUnsatisfiable(X_216) ),
inference(resolution,[status(thm)],[c_181,c_234]) ).
tff(c_324,plain,
! [X_217] :
( ( '#skF_2'(X_217) = '#skF_1'(X_217) )
| ~ cUnsatisfiable(X_217) ),
inference(resolution,[status(thm)],[c_208,c_310]) ).
tff(c_328,plain,
'#skF_2'(i2003_11_14_17_21_01226) = '#skF_1'(i2003_11_14_17_21_01226),
inference(resolution,[status(thm)],[c_116,c_324]) ).
tff(c_78,plain,
! [X_89] :
( cc2('#skF_2'(X_89))
| ~ cUnsatisfiable(X_89) ),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_344,plain,
( cc2('#skF_1'(i2003_11_14_17_21_01226))
| ~ cUnsatisfiable(i2003_11_14_17_21_01226) ),
inference(superposition,[status(thm),theory(equality)],[c_328,c_78]) ).
tff(c_356,plain,
cc2('#skF_1'(i2003_11_14_17_21_01226)),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_344]) ).
tff(c_86,plain,
! [X_96] :
( ca_Ax2(X_96)
| ~ cc1(X_96)
| ~ cc2(X_96) ),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_361,plain,
( ca_Ax2('#skF_1'(i2003_11_14_17_21_01226))
| ~ cc1('#skF_1'(i2003_11_14_17_21_01226)) ),
inference(resolution,[status(thm)],[c_356,c_86]) ).
tff(c_420,plain,
~ cc1('#skF_1'(i2003_11_14_17_21_01226)),
inference(splitLeft,[status(thm)],[c_361]) ).
tff(c_423,plain,
~ cUnsatisfiable(i2003_11_14_17_21_01226),
inference(resolution,[status(thm)],[c_82,c_420]) ).
tff(c_430,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_116,c_423]) ).
tff(c_431,plain,
ca_Ax2('#skF_1'(i2003_11_14_17_21_01226)),
inference(splitRight,[status(thm)],[c_361]) ).
tff(c_217,plain,
! [X_178,Y_179] :
( ca_Cx1xcomp(X_178)
| ~ ca_Ax2(Y_179)
| ~ rrx3(X_178,Y_179) ),
inference(cnfTransformation,[status(thm)],[f_267]) ).
tff(c_225,plain,
! [X_89] :
( ca_Cx1xcomp(X_89)
| ~ ca_Ax2('#skF_1'(X_89))
| ~ cUnsatisfiable(X_89) ),
inference(resolution,[status(thm)],[c_84,c_217]) ).
tff(c_435,plain,
( ca_Cx1xcomp(i2003_11_14_17_21_01226)
| ~ cUnsatisfiable(i2003_11_14_17_21_01226) ),
inference(resolution,[status(thm)],[c_431,c_225]) ).
tff(c_438,plain,
ca_Cx1xcomp(i2003_11_14_17_21_01226),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_435]) ).
tff(c_149,plain,
! [X_154] :
( ra_Px1(X_154,'#skF_3'(X_154))
| ~ ca_Cx1(X_154) ),
inference(cnfTransformation,[status(thm)],[f_259]) ).
tff(c_102,plain,
! [X_105,Y_108] :
( ~ ra_Px1(X_105,Y_108)
| ~ ca_Cx1xcomp(X_105) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_157,plain,
! [X_154] :
( ~ ca_Cx1xcomp(X_154)
| ~ ca_Cx1(X_154) ),
inference(resolution,[status(thm)],[c_149,c_102]) ).
tff(c_448,plain,
~ ca_Cx1(i2003_11_14_17_21_01226),
inference(resolution,[status(thm)],[c_438,c_157]) ).
tff(c_451,plain,
~ cUnsatisfiable(i2003_11_14_17_21_01226),
inference(resolution,[status(thm)],[c_76,c_448]) ).
tff(c_455,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_116,c_451]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.07 % Problem : KRS107+1 : TPTP v9.0.0. Released v3.1.0.
% 0.06/0.08 % 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.07/0.26 % Computer : n020.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 300
% 0.07/0.26 % DateTime : Tue Apr 8 02:59:03 EDT 2025
% 0.07/0.26 % CPUTime :
% 4.65/1.96 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.65/1.97
% 4.65/1.97 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------