%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS082+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 : n004.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 4.54s 2.17s
% Output : CNFRefutation 4.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 7
% Syntax : Number of formulae : 32 ( 4 unt; 0 typ; 0 def)
% Number of atoms : 94 ( 0 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 107 ( 45 ~; 38 |; 10 &)
% ( 4 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-2 aty)
% Number of variables : 62 ( 57 !; 5 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rs > rr > rp > rinvS > rinvR > rinvP > xsd_string > xsd_integer > cowlThing > cowlNothing > cc > ca > cUnsatisfiable > #nlpp > i2003_11_14_17_19_28752 > #skF_7 > #skF_5 > #skF_2 > #skF_1 > #skF_8 > #skF_3 > #skF_6 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(rinvR,type,
rinvR: ( $i * $i ) > $o ).
tff(rr,type,
rr: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff(cc,type,
cc: $i > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(rinvS,type,
rinvS: ( $i * $i ) > $o ).
tff(rinvP,type,
rinvP: ( $i * $i ) > $o ).
tff(rs,type,
rs: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(i2003_11_14_17_19_28752,type,
i2003_11_14_17_19_28752: $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff(cUnsatisfiable,type,
cUnsatisfiable: $i > $o ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff(ca,type,
ca: $i > $o ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff(rp,type,
rp: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(f_89,axiom,
! [X] :
( cUnsatisfiable(X)
=> ca(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
tff(f_84,axiom,
! [X] :
( cUnsatisfiable(X)
=> ? [Y] :
( rs(X,Y)
& ? [Z] :
( rp(Y,Z)
& cowlThing(Z) )
& ! [Z] :
( rr(Y,Z)
=> cc(Z) )
& ! [Z] :
( rp(Y,Z)
=> ? [W] :
( rr(Z,W)
& cowlThing(W) ) )
& ! [Z] :
( rp(Y,Z)
=> ? [W] :
( rp(Z,W)
& cowlThing(W) ) )
& ! [Z] :
( rp(Y,Z)
=> ! [W] :
( rr(Z,W)
=> cc(W) ) )
& ? [Z] :
( rr(Y,Z)
& cowlThing(Z) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
tff(f_114,axiom,
! [X,Y] :
( rinvR(X,Y)
<=> rr(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
tff(f_109,axiom,
! [X,Y] :
( rinvP(X,Y)
<=> rp(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
tff(f_119,axiom,
! [X,Y] :
( rinvS(X,Y)
<=> rs(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
tff(f_104,axiom,
! [X] :
( cc(X)
<=> ! [Y] :
( rinvR(X,Y)
=> ! [Z] :
( rinvP(Y,Z)
=> ! [W] :
( rinvS(Z,W)
=> ~ ca(W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
tff(f_128,axiom,
cUnsatisfiable(i2003_11_14_17_19_28752),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
tff(c_32,plain,
! [X_49] :
( ca(X_49)
| ~ cUnsatisfiable(X_49) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_20,plain,
! [X_3] :
( rp('#skF_1'(X_3),'#skF_2'(X_3))
| ~ cUnsatisfiable(X_3) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_160,plain,
! [Z_128,X_129] :
( rr(Z_128,'#skF_3'(X_129,Z_128))
| ~ rp('#skF_1'(X_129),Z_128)
| ~ cUnsatisfiable(X_129) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_50,plain,
! [X_78,Y_79] :
( rinvR(X_78,Y_79)
| ~ rr(Y_79,X_78) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_281,plain,
! [X_152,Z_153] :
( rinvR('#skF_3'(X_152,Z_153),Z_153)
| ~ rp('#skF_1'(X_152),Z_153)
| ~ cUnsatisfiable(X_152) ),
inference(resolution,[status(thm)],[c_160,c_50]) ).
tff(c_302,plain,
! [X_3] :
( rinvR('#skF_3'(X_3,'#skF_2'(X_3)),'#skF_2'(X_3))
| ~ cUnsatisfiable(X_3) ),
inference(resolution,[status(thm)],[c_20,c_281]) ).
tff(c_48,plain,
! [Y_79,X_78] :
( rr(Y_79,X_78)
| ~ rinvR(X_78,Y_79) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_266,plain,
! [W_146,Z_147,X_148] :
( cc(W_146)
| ~ rr(Z_147,W_146)
| ~ rp('#skF_1'(X_148),Z_147)
| ~ cUnsatisfiable(X_148) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_331,plain,
! [X_161,X_162,Y_163] :
( cc(X_161)
| ~ rp('#skF_1'(X_162),Y_163)
| ~ cUnsatisfiable(X_162)
| ~ rinvR(X_161,Y_163) ),
inference(resolution,[status(thm)],[c_48,c_266]) ).
tff(c_358,plain,
! [X_164,X_165] :
( cc(X_164)
| ~ rinvR(X_164,'#skF_2'(X_165))
| ~ cUnsatisfiable(X_165) ),
inference(resolution,[status(thm)],[c_20,c_331]) ).
tff(c_362,plain,
! [X_3] :
( cc('#skF_3'(X_3,'#skF_2'(X_3)))
| ~ cUnsatisfiable(X_3) ),
inference(resolution,[status(thm)],[c_302,c_358]) ).
tff(c_97,plain,
! [X_105] :
( rp('#skF_1'(X_105),'#skF_2'(X_105))
| ~ cUnsatisfiable(X_105) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_46,plain,
! [X_76,Y_77] :
( rinvP(X_76,Y_77)
| ~ rp(Y_77,X_76) ),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_101,plain,
! [X_105] :
( rinvP('#skF_2'(X_105),'#skF_1'(X_105))
| ~ cUnsatisfiable(X_105) ),
inference(resolution,[status(thm)],[c_97,c_46]) ).
tff(c_22,plain,
! [X_3] :
( rs(X_3,'#skF_1'(X_3))
| ~ cUnsatisfiable(X_3) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_78,plain,
! [X_99,Y_100] :
( rinvS(X_99,Y_100)
| ~ rs(Y_100,X_99) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_86,plain,
! [X_3] :
( rinvS('#skF_1'(X_3),X_3)
| ~ cUnsatisfiable(X_3) ),
inference(resolution,[status(thm)],[c_22,c_78]) ).
tff(c_324,plain,
! [W_157,Z_158,Y_159,X_160] :
( ~ ca(W_157)
| ~ rinvS(Z_158,W_157)
| ~ rinvP(Y_159,Z_158)
| ~ rinvR(X_160,Y_159)
| ~ cc(X_160) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_641,plain,
! [X_208,Y_209,X_210] :
( ~ ca(X_208)
| ~ rinvP(Y_209,'#skF_1'(X_208))
| ~ rinvR(X_210,Y_209)
| ~ cc(X_210)
| ~ cUnsatisfiable(X_208) ),
inference(resolution,[status(thm)],[c_86,c_324]) ).
tff(c_709,plain,
! [X_214,X_215] :
( ~ ca(X_214)
| ~ rinvR(X_215,'#skF_2'(X_214))
| ~ cc(X_215)
| ~ cUnsatisfiable(X_214) ),
inference(resolution,[status(thm)],[c_101,c_641]) ).
tff(c_724,plain,
! [X_216] :
( ~ ca(X_216)
| ~ cc('#skF_3'(X_216,'#skF_2'(X_216)))
| ~ cUnsatisfiable(X_216) ),
inference(resolution,[status(thm)],[c_302,c_709]) ).
tff(c_729,plain,
! [X_217] :
( ~ ca(X_217)
| ~ cUnsatisfiable(X_217) ),
inference(resolution,[status(thm)],[c_362,c_724]) ).
tff(c_737,plain,
! [X_49] : ~ cUnsatisfiable(X_49),
inference(resolution,[status(thm)],[c_32,c_729]) ).
tff(c_58,plain,
cUnsatisfiable(i2003_11_14_17_19_28752),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_739,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_737,c_58]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : KRS082+1 : TPTP v9.0.0. Released v3.1.0.
% 0.12/0.14 % 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.14/0.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Tue Apr 8 02:58:08 EDT 2025
% 0.14/0.35 % CPUTime :
% 4.54/2.17 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.54/2.17
% 4.54/2.17 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------