%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS103+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/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 : n018.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:20 PM UTC 2025
% Result : Unsatisfiable 5.81s 2.14s
% Output : CNFRefutation 6.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 25
% Syntax : Number of formulae : 94 ( 4 unt; 0 typ; 0 def)
% Number of atoms : 317 ( 0 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 359 ( 136 ~; 199 |; 8 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 91 ( 91 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ xsd_string > xsd_integer > cplus9 > cplus8 > cplus7 > cplus6 > cplus5 > cplus4 > cplus3 > cplus2 > cplus1 > cowlThing > cowlNothing > cminus9 > cminus8 > cminus7 > cminus6 > cminus5 > cminus4 > cminus3 > cminus2 > cminus1 > cTest > #nlpp > i2003_11_14_17_20_46476
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(cminus7,type,
cminus7: $i > $o ).
tff(cplus1,type,
cplus1: $i > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(cplus8,type,
cplus8: $i > $o ).
tff(cminus8,type,
cminus8: $i > $o ).
tff(cminus3,type,
cminus3: $i > $o ).
tff(cplus9,type,
cplus9: $i > $o ).
tff(cplus5,type,
cplus5: $i > $o ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff(cplus7,type,
cplus7: $i > $o ).
tff(cTest,type,
cTest: $i > $o ).
tff(i2003_11_14_17_20_46476,type,
i2003_11_14_17_20_46476: $i ).
tff(cplus3,type,
cplus3: $i > $o ).
tff(cminus6,type,
cminus6: $i > $o ).
tff(cplus2,type,
cplus2: $i > $o ).
tff(cminus1,type,
cminus1: $i > $o ).
tff(cminus5,type,
cminus5: $i > $o ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff(cminus4,type,
cminus4: $i > $o ).
tff(cminus9,type,
cminus9: $i > $o ).
tff(cminus2,type,
cminus2: $i > $o ).
tff(cplus4,type,
cplus4: $i > $o ).
tff(cplus6,type,
cplus6: $i > $o ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(f_291,axiom,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cminus3(X)
| cminus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
tff(f_111,axiom,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cminus4(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
tff(f_309,axiom,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cminus8(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_31) ).
tff(f_456,axiom,
! [X] :
~ ( cminus9(X)
& cplus9(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_49) ).
tff(f_66,axiom,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cplus7(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
tff(f_451,axiom,
! [X] :
~ ( cminus8(X)
& cplus8(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_48) ).
tff(f_466,axiom,
! [X] :
~ ( cminus7(X)
& cplus7(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_51) ).
tff(f_219,axiom,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus4(X)
| cminus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
tff(f_461,axiom,
! [X] :
~ ( cplus4(X)
& cminus4(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_50) ).
tff(f_228,axiom,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus6(X)
| cminus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_22) ).
tff(f_491,axiom,
! [X] :
~ ( cplus6(X)
& cminus6(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_56) ).
tff(f_327,axiom,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cminus2(X)
| cplus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_33) ).
tff(f_192,axiom,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus6(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
tff(f_84,axiom,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cminus7(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
tff(f_471,axiom,
! [X] :
~ ( cplus3(X)
& cminus3(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_52) ).
tff(f_336,axiom,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cplus9(X)
| cplus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_34) ).
tff(f_282,axiom,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cplus3(X)
| cplus4(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_28) ).
tff(f_255,axiom,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cplus4(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_25) ).
tff(f_57,axiom,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cminus5(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
tff(f_210,axiom,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cplus2(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_20) ).
tff(f_481,axiom,
! [X] :
~ ( cminus2(X)
& cplus2(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_54) ).
tff(f_165,axiom,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cplus5(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
tff(f_476,axiom,
! [X] :
~ ( cplus5(X)
& cminus5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_53) ).
tff(f_435,axiom,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cplus2(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_45) ).
tff(f_446,axiom,
cTest(i2003_11_14_17_20_46476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_47) ).
tff(c_64,plain,
! [X_30] :
( cminus7(X_30)
| cminus3(X_30)
| cminus4(X_30)
| ~ cTest(X_30) ),
inference(cnfTransformation,[status(thm)],[f_291]) ).
tff(c_24,plain,
! [X_10] :
( cminus8(X_10)
| cminus4(X_10)
| cminus9(X_10)
| ~ cTest(X_10) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_284,plain,
! [X_102] :
( cplus9(X_102)
| cminus8(X_102)
| cminus4(X_102)
| ~ cTest(X_102) ),
inference(cnfTransformation,[status(thm)],[f_309]) ).
tff(c_104,plain,
! [X_49] :
( ~ cplus9(X_49)
| ~ cminus9(X_49) ),
inference(cnfTransformation,[status(thm)],[f_456]) ).
tff(c_520,plain,
! [X_154] :
( ~ cminus9(X_154)
| cminus8(X_154)
| cminus4(X_154)
| ~ cTest(X_154) ),
inference(resolution,[status(thm)],[c_284,c_104]) ).
tff(c_544,plain,
! [X_10] :
( cminus8(X_10)
| cminus4(X_10)
| ~ cTest(X_10) ),
inference(resolution,[status(thm)],[c_24,c_520]) ).
tff(c_294,plain,
! [X_104] :
( cplus8(X_104)
| cplus7(X_104)
| cminus3(X_104)
| ~ cTest(X_104) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_102,plain,
! [X_48] :
( ~ cplus8(X_48)
| ~ cminus8(X_48) ),
inference(cnfTransformation,[status(thm)],[f_451]) ).
tff(c_417,plain,
! [X_131] :
( ~ cminus8(X_131)
| cplus7(X_131)
| cminus3(X_131)
| ~ cTest(X_131) ),
inference(resolution,[status(thm)],[c_294,c_102]) ).
tff(c_108,plain,
! [X_51] :
( ~ cplus7(X_51)
| ~ cminus7(X_51) ),
inference(cnfTransformation,[status(thm)],[f_466]) ).
tff(c_599,plain,
! [X_161] :
( ~ cminus7(X_161)
| ~ cminus8(X_161)
| cminus3(X_161)
| ~ cTest(X_161) ),
inference(resolution,[status(thm)],[c_417,c_108]) ).
tff(c_923,plain,
! [X_185] :
( ~ cminus7(X_185)
| cminus3(X_185)
| cminus4(X_185)
| ~ cTest(X_185) ),
inference(resolution,[status(thm)],[c_544,c_599]) ).
tff(c_935,plain,
! [X_30] :
( cminus3(X_30)
| cminus4(X_30)
| ~ cTest(X_30) ),
inference(resolution,[status(thm)],[c_64,c_923]) ).
tff(c_172,plain,
! [X_78] :
( cminus6(X_78)
| cplus4(X_78)
| cminus2(X_78)
| ~ cTest(X_78) ),
inference(cnfTransformation,[status(thm)],[f_219]) ).
tff(c_106,plain,
! [X_50] :
( ~ cminus4(X_50)
| ~ cplus4(X_50) ),
inference(cnfTransformation,[status(thm)],[f_461]) ).
tff(c_176,plain,
! [X_78] :
( ~ cminus4(X_78)
| cminus6(X_78)
| cminus2(X_78)
| ~ cTest(X_78) ),
inference(resolution,[status(thm)],[c_172,c_106]) ).
tff(c_177,plain,
! [X_79] :
( cminus7(X_79)
| cplus6(X_79)
| cminus2(X_79)
| ~ cTest(X_79) ),
inference(cnfTransformation,[status(thm)],[f_228]) ).
tff(c_118,plain,
! [X_56] :
( ~ cminus6(X_56)
| ~ cplus6(X_56) ),
inference(cnfTransformation,[status(thm)],[f_491]) ).
tff(c_181,plain,
! [X_79] :
( ~ cminus6(X_79)
| cminus7(X_79)
| cminus2(X_79)
| ~ cTest(X_79) ),
inference(resolution,[status(thm)],[c_177,c_118]) ).
tff(c_137,plain,
! [X_71] :
( cplus7(X_71)
| cminus2(X_71)
| cminus9(X_71)
| ~ cTest(X_71) ),
inference(cnfTransformation,[status(thm)],[f_327]) ).
tff(c_141,plain,
! [X_71] :
( ~ cminus7(X_71)
| cminus2(X_71)
| cminus9(X_71)
| ~ cTest(X_71) ),
inference(resolution,[status(thm)],[c_137,c_108]) ).
tff(c_214,plain,
! [X_88] :
( cplus9(X_88)
| cplus6(X_88)
| cminus2(X_88)
| ~ cTest(X_88) ),
inference(cnfTransformation,[status(thm)],[f_192]) ).
tff(c_469,plain,
! [X_143] :
( ~ cminus9(X_143)
| cplus6(X_143)
| cminus2(X_143)
| ~ cTest(X_143) ),
inference(resolution,[status(thm)],[c_214,c_104]) ).
tff(c_897,plain,
! [X_183] :
( ~ cminus6(X_183)
| ~ cminus9(X_183)
| cminus2(X_183)
| ~ cTest(X_183) ),
inference(resolution,[status(thm)],[c_469,c_118]) ).
tff(c_947,plain,
! [X_189] :
( ~ cminus6(X_189)
| ~ cminus7(X_189)
| cminus2(X_189)
| ~ cTest(X_189) ),
inference(resolution,[status(thm)],[c_141,c_897]) ).
tff(c_960,plain,
! [X_190] :
( ~ cminus6(X_190)
| cminus2(X_190)
| ~ cTest(X_190) ),
inference(resolution,[status(thm)],[c_181,c_947]) ).
tff(c_978,plain,
! [X_192] :
( ~ cminus4(X_192)
| cminus2(X_192)
| ~ cTest(X_192) ),
inference(resolution,[status(thm)],[c_176,c_960]) ).
tff(c_988,plain,
! [X_30] :
( cminus2(X_30)
| cminus3(X_30)
| ~ cTest(X_30) ),
inference(resolution,[status(thm)],[c_935,c_978]) ).
tff(c_324,plain,
! [X_110] :
( cplus8(X_110)
| cminus7(X_110)
| cplus3(X_110)
| ~ cTest(X_110) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_432,plain,
! [X_134] :
( ~ cminus8(X_134)
| cminus7(X_134)
| cplus3(X_134)
| ~ cTest(X_134) ),
inference(resolution,[status(thm)],[c_324,c_102]) ).
tff(c_110,plain,
! [X_52] :
( ~ cminus3(X_52)
| ~ cplus3(X_52) ),
inference(cnfTransformation,[status(thm)],[f_471]) ).
tff(c_785,plain,
! [X_175] :
( ~ cminus3(X_175)
| ~ cminus8(X_175)
| cminus7(X_175)
| ~ cTest(X_175) ),
inference(resolution,[status(thm)],[c_432,c_110]) ).
tff(c_1196,plain,
! [X_214] :
( ~ cminus3(X_214)
| cminus7(X_214)
| cminus4(X_214)
| ~ cTest(X_214) ),
inference(resolution,[status(thm)],[c_544,c_785]) ).
tff(c_197,plain,
! [X_83] :
( cplus7(X_83)
| cplus9(X_83)
| cminus4(X_83)
| ~ cTest(X_83) ),
inference(cnfTransformation,[status(thm)],[f_336]) ).
tff(c_490,plain,
! [X_148] :
( ~ cminus9(X_148)
| cplus7(X_148)
| cminus4(X_148)
| ~ cTest(X_148) ),
inference(resolution,[status(thm)],[c_197,c_104]) ).
tff(c_551,plain,
! [X_157] :
( ~ cminus7(X_157)
| ~ cminus9(X_157)
| cminus4(X_157)
| ~ cTest(X_157) ),
inference(resolution,[status(thm)],[c_490,c_108]) ).
tff(c_567,plain,
! [X_71] :
( cminus4(X_71)
| ~ cminus7(X_71)
| cminus2(X_71)
| ~ cTest(X_71) ),
inference(resolution,[status(thm)],[c_141,c_551]) ).
tff(c_1269,plain,
! [X_219] :
( cminus2(X_219)
| ~ cminus3(X_219)
| cminus4(X_219)
| ~ cTest(X_219) ),
inference(resolution,[status(thm)],[c_1196,c_567]) ).
tff(c_224,plain,
! [X_90] :
( cplus4(X_90)
| cplus3(X_90)
| cminus9(X_90)
| ~ cTest(X_90) ),
inference(cnfTransformation,[status(thm)],[f_282]) ).
tff(c_453,plain,
! [X_139] :
( ~ cminus4(X_139)
| cplus3(X_139)
| cminus9(X_139)
| ~ cTest(X_139) ),
inference(resolution,[status(thm)],[c_224,c_106]) ).
tff(c_457,plain,
! [X_139] :
( ~ cminus3(X_139)
| ~ cminus4(X_139)
| cminus9(X_139)
| ~ cTest(X_139) ),
inference(resolution,[status(thm)],[c_453,c_110]) ).
tff(c_254,plain,
! [X_96] :
( cplus9(X_96)
| cplus4(X_96)
| cplus3(X_96)
| ~ cTest(X_96) ),
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_437,plain,
! [X_135] :
( ~ cminus9(X_135)
| cplus4(X_135)
| cplus3(X_135)
| ~ cTest(X_135) ),
inference(resolution,[status(thm)],[c_254,c_104]) ).
tff(c_749,plain,
! [X_171] :
( ~ cminus4(X_171)
| ~ cminus9(X_171)
| cplus3(X_171)
| ~ cTest(X_171) ),
inference(resolution,[status(thm)],[c_437,c_106]) ).
tff(c_1085,plain,
! [X_203] :
( ~ cminus3(X_203)
| ~ cminus4(X_203)
| ~ cminus9(X_203)
| ~ cTest(X_203) ),
inference(resolution,[status(thm)],[c_749,c_110]) ).
tff(c_1101,plain,
! [X_139] :
( ~ cminus3(X_139)
| ~ cminus4(X_139)
| ~ cTest(X_139) ),
inference(resolution,[status(thm)],[c_457,c_1085]) ).
tff(c_1278,plain,
! [X_220] :
( cminus2(X_220)
| ~ cminus3(X_220)
| ~ cTest(X_220) ),
inference(resolution,[status(thm)],[c_1269,c_1101]) ).
tff(c_1283,plain,
! [X_221] :
( cminus2(X_221)
| ~ cTest(X_221) ),
inference(resolution,[status(thm)],[c_988,c_1278]) ).
tff(c_12,plain,
! [X_4] :
( cminus8(X_4)
| cminus5(X_4)
| cminus3(X_4)
| ~ cTest(X_4) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_182,plain,
! [X_80] :
( cplus8(X_80)
| cplus2(X_80)
| cminus3(X_80)
| ~ cTest(X_80) ),
inference(cnfTransformation,[status(thm)],[f_210]) ).
tff(c_515,plain,
! [X_153] :
( ~ cminus8(X_153)
| cplus2(X_153)
| cminus3(X_153)
| ~ cTest(X_153) ),
inference(resolution,[status(thm)],[c_182,c_102]) ).
tff(c_114,plain,
! [X_54] :
( ~ cplus2(X_54)
| ~ cminus2(X_54) ),
inference(cnfTransformation,[status(thm)],[f_481]) ).
tff(c_810,plain,
! [X_176] :
( ~ cminus2(X_176)
| ~ cminus8(X_176)
| cminus3(X_176)
| ~ cTest(X_176) ),
inference(resolution,[status(thm)],[c_515,c_114]) ).
tff(c_834,plain,
! [X_4] :
( ~ cminus2(X_4)
| cminus5(X_4)
| cminus3(X_4)
| ~ cTest(X_4) ),
inference(resolution,[status(thm)],[c_12,c_810]) ).
tff(c_329,plain,
! [X_111] :
( cminus8(X_111)
| cplus5(X_111)
| cminus3(X_111)
| ~ cTest(X_111) ),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_112,plain,
! [X_53] :
( ~ cminus5(X_53)
| ~ cplus5(X_53) ),
inference(cnfTransformation,[status(thm)],[f_476]) ).
tff(c_333,plain,
! [X_111] :
( ~ cminus5(X_111)
| cminus8(X_111)
| cminus3(X_111)
| ~ cTest(X_111) ),
inference(resolution,[status(thm)],[c_329,c_112]) ).
tff(c_1146,plain,
! [X_208] :
( ~ cminus2(X_208)
| ~ cminus5(X_208)
| cminus3(X_208)
| ~ cTest(X_208) ),
inference(resolution,[status(thm)],[c_333,c_810]) ).
tff(c_1151,plain,
! [X_209] :
( ~ cminus2(X_209)
| cminus3(X_209)
| ~ cTest(X_209) ),
inference(resolution,[status(thm)],[c_834,c_1146]) ).
tff(c_162,plain,
! [X_76] :
( cplus8(X_76)
| cplus2(X_76)
| cminus4(X_76)
| ~ cTest(X_76) ),
inference(cnfTransformation,[status(thm)],[f_435]) ).
tff(c_382,plain,
! [X_124] :
( ~ cminus8(X_124)
| cplus2(X_124)
| cminus4(X_124)
| ~ cTest(X_124) ),
inference(resolution,[status(thm)],[c_162,c_102]) ).
tff(c_861,plain,
! [X_179] :
( ~ cminus2(X_179)
| ~ cminus8(X_179)
| cminus4(X_179)
| ~ cTest(X_179) ),
inference(resolution,[status(thm)],[c_382,c_114]) ).
tff(c_881,plain,
! [X_10] :
( ~ cminus2(X_10)
| cminus4(X_10)
| ~ cTest(X_10) ),
inference(resolution,[status(thm)],[c_544,c_861]) ).
tff(c_1106,plain,
! [X_204] :
( ~ cminus3(X_204)
| ~ cminus4(X_204)
| ~ cTest(X_204) ),
inference(resolution,[status(thm)],[c_457,c_1085]) ).
tff(c_1117,plain,
! [X_10] :
( ~ cminus3(X_10)
| ~ cminus2(X_10)
| ~ cTest(X_10) ),
inference(resolution,[status(thm)],[c_881,c_1106]) ).
tff(c_1159,plain,
! [X_209] :
( ~ cminus2(X_209)
| ~ cTest(X_209) ),
inference(resolution,[status(thm)],[c_1151,c_1117]) ).
tff(c_1287,plain,
! [X_221] : ~ cTest(X_221),
inference(resolution,[status(thm)],[c_1283,c_1159]) ).
tff(c_100,plain,
cTest(i2003_11_14_17_20_46476),
inference(cnfTransformation,[status(thm)],[f_446]) ).
tff(c_1289,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1287,c_100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : KRS103+1 : TPTP v9.0.0. Released v3.1.0.
% 0.00/0.07 % 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.07/0.26 % Computer : n018.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:02 EDT 2025
% 0.07/0.26 % CPUTime :
% 5.81/2.14 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.81/2.15
% 5.81/2.15 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------