%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN551+1 : TPTP v9.0.0. Bugfixed 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 : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 10:03:53 PM UTC 2025
% Result : Theorem 4.16s 2.56s
% Output : CNFRefutation 4.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 1
% Syntax : Number of formulae : 253 ( 174 unt; 0 typ; 0 def)
% Number of atoms : 422 ( 380 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 354 ( 185 ~; 162 |; 4 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 167 ( 165 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ #nlpp > g > f > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(f,type,
f: $i > $i ).
tff(g,type,
g: $i > $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(f_49,negated_conjecture,
~ ( ( ? [X] : ( X = f(g(X)) )
& ! [Y,Z] :
( ( ( Y = f(g(Y)) )
& ( Z = f(g(Z)) ) )
=> ( Y = Z ) ) )
<=> ( ? [X] : ( X = g(f(X)) )
& ! [Y,Z] :
( ( ( Y = g(f(Y)) )
& ( Z = g(f(Z)) ) )
=> ( Y = Z ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_cute_thing) ).
tff(c_4,plain,
! [X_6] :
( ( f(g('#skF_1')) = '#skF_1' )
| ( '#skF_5' != '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_57,plain,
'#skF_5' != '#skF_6',
inference(splitLeft,[status(thm)],[c_4]) ).
tff(c_44,plain,
( ( f(g('#skF_1')) = '#skF_1' )
| ( g(f('#skF_4')) = '#skF_4' ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_51,plain,
g(f('#skF_4')) = '#skF_4',
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_24,plain,
! [X_6] :
( ( f(g('#skF_1')) = '#skF_1' )
| ( f(g('#skF_5')) = '#skF_5' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_60,plain,
! [X_7] : ( f(g(X_7)) != X_7 ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_65,plain,
$false,
inference(superposition,[status(thm),theory(equality)],[c_51,c_60]) ).
tff(c_66,plain,
( ( f(g('#skF_5')) = '#skF_5' )
| ( f(g('#skF_1')) = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_67,plain,
f(g('#skF_1')) = '#skF_1',
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_22,plain,
! [Z_2,Y_1,X_6] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( f(g('#skF_5')) = '#skF_5' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_506,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_508,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_506,c_67]) ).
tff(c_509,plain,
! [Z_2,Y_1] :
( ( f(g('#skF_5')) = '#skF_5' )
| ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 ) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_510,plain,
f(g('#skF_5')) = '#skF_5',
inference(splitLeft,[status(thm)],[c_509]) ).
tff(c_18,plain,
! [X_3,X_6] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_6')) = '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_77,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_79,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_77,c_67]) ).
tff(c_80,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( f(g('#skF_6')) = '#skF_6' )
| ( g(f('#skF_3')) = '#skF_3' ) ),
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_81,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_80]) ).
tff(c_83,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_81,c_51]) ).
tff(c_84,plain,
( ( g(f('#skF_3')) = '#skF_3' )
| ( f(g('#skF_6')) = '#skF_6' ) ),
inference(splitRight,[status(thm)],[c_80]) ).
tff(c_85,plain,
f(g('#skF_6')) = '#skF_6',
inference(splitLeft,[status(thm)],[c_84]) ).
tff(c_38,plain,
! [X_3,Z_5,Y_4] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_106,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_108,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_106,c_51]) ).
tff(c_109,plain,
! [Z_5,Y_4] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_110,plain,
g(f('#skF_3')) = '#skF_3',
inference(splitLeft,[status(thm)],[c_109]) ).
tff(c_28,plain,
! [X_3,X_6] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_5')) = '#skF_5' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_91,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_94,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_91,c_85]) ).
tff(c_95,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( f(g('#skF_5')) = '#skF_5' )
| ( g(f('#skF_3')) = '#skF_3' ) ),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_96,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_95]) ).
tff(c_98,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_96,c_51]) ).
tff(c_99,plain,
( ( g(f('#skF_3')) = '#skF_3' )
| ( f(g('#skF_5')) = '#skF_5' ) ),
inference(splitRight,[status(thm)],[c_95]) ).
tff(c_100,plain,
f(g('#skF_5')) = '#skF_5',
inference(splitLeft,[status(thm)],[c_99]) ).
tff(c_16,plain,
! [X_3,X_6] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_6')) = '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_74,plain,
'#skF_2' != '#skF_3',
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_40,plain,
! [X_3,Z_5,Y_4] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_111,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_118,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_111,c_110]) ).
tff(c_119,plain,
! [Z_5,Y_4] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_124,plain,
g(f('#skF_2')) = '#skF_2',
inference(splitLeft,[status(thm)],[c_119]) ).
tff(c_32,plain,
! [Z_2,Y_1,Z_5,Y_4] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_132,plain,
! [Z_8,Y_9] :
( ( Z_8 = Y_9 )
| ( g(f(Z_8)) != Z_8 )
| ( g(f(Y_9)) != Y_9 ) ),
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_151,plain,
! [Y_10] :
( ( Y_10 = '#skF_2' )
| ( g(f(Y_10)) != Y_10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_132]) ).
tff(c_157,plain,
'#skF_2' = '#skF_3',
inference(superposition,[status(thm),theory(equality)],[c_110,c_151]) ).
tff(c_175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_157]) ).
tff(c_177,plain,
! [Z_11,Y_12] :
( ( Z_11 = Y_12 )
| ( f(g(Z_11)) != Z_11 )
| ( f(g(Y_12)) != Y_12 ) ),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_196,plain,
! [Y_13] :
( ( Y_13 = '#skF_5' )
| ( f(g(Y_13)) != Y_13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_100,c_177]) ).
tff(c_208,plain,
'#skF_5' = '#skF_6',
inference(superposition,[status(thm),theory(equality)],[c_85,c_196]) ).
tff(c_222,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57,c_208]) ).
tff(c_225,plain,
! [Z_14,Y_15] :
( ( Z_14 = Y_15 )
| ( g(f(Z_14)) != Z_14 )
| ( g(f(Y_15)) != Y_15 ) ),
inference(splitRight,[status(thm)],[c_119]) ).
tff(c_241,plain,
! [Y_16] :
( ( Y_16 = '#skF_3' )
| ( g(f(Y_16)) != Y_16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_110,c_225]) ).
tff(c_262,plain,
'#skF_3' = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_51,c_241]) ).
tff(c_260,plain,
g('#skF_6') = '#skF_3',
inference(superposition,[status(thm),theory(equality)],[c_85,c_241]) ).
tff(c_272,plain,
g('#skF_6') = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_262,c_260]) ).
tff(c_273,plain,
f('#skF_4') = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_272,c_85]) ).
tff(c_259,plain,
g('#skF_5') = '#skF_3',
inference(superposition,[status(thm),theory(equality)],[c_100,c_241]) ).
tff(c_279,plain,
g('#skF_5') = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_262,c_259]) ).
tff(c_280,plain,
f('#skF_4') = '#skF_5',
inference(demodulation,[status(thm),theory(equality)],[c_279,c_100]) ).
tff(c_295,plain,
'#skF_5' = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_273,c_280]) ).
tff(c_296,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57,c_295]) ).
tff(c_299,plain,
! [Z_17,Y_18] :
( ( Z_17 = Y_18 )
| ( g(f(Z_17)) != Z_17 )
| ( g(f(Y_18)) != Y_18 ) ),
inference(splitRight,[status(thm)],[c_109]) ).
tff(c_313,plain,
! [Y_19] :
( ( Y_19 = '#skF_4' )
| ( g(f(Y_19)) != Y_19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_51,c_299]) ).
tff(c_327,plain,
g('#skF_6') = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_85,c_313]) ).
tff(c_336,plain,
f('#skF_4') = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_327,c_85]) ).
tff(c_326,plain,
g('#skF_5') = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_100,c_313]) ).
tff(c_331,plain,
f('#skF_4') = '#skF_5',
inference(demodulation,[status(thm),theory(equality)],[c_326,c_100]) ).
tff(c_359,plain,
'#skF_5' = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_336,c_331]) ).
tff(c_360,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57,c_359]) ).
tff(c_362,plain,
f(g('#skF_5')) != '#skF_5',
inference(splitRight,[status(thm)],[c_99]) ).
tff(c_384,plain,
! [Z_2,Y_1,X_6] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( f(g(X_6)) != X_6 ) ),
inference(negUnitSimplification,[status(thm)],[c_362,c_22]) ).
tff(c_385,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_384]) ).
tff(c_388,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_385,c_85]) ).
tff(c_390,plain,
! [Z_20,Y_21] :
( ( Z_20 = Y_21 )
| ( f(g(Z_20)) != Z_20 )
| ( f(g(Y_21)) != Y_21 ) ),
inference(splitRight,[status(thm)],[c_384]) ).
tff(c_406,plain,
! [Y_22] :
( ( Y_22 = '#skF_6' )
| ( f(g(Y_22)) != Y_22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_390]) ).
tff(c_426,plain,
'#skF_6' = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_67,c_406]) ).
tff(c_427,plain,
f('#skF_4') = '#skF_6',
inference(superposition,[status(thm),theory(equality)],[c_51,c_406]) ).
tff(c_443,plain,
f('#skF_4') = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_426,c_427]) ).
tff(c_444,plain,
g('#skF_1') = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_443,c_51]) ).
tff(c_30,plain,
! [X_3,X_6] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_5')) = '#skF_5' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_367,plain,
! [X_3,X_6] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( f(g(X_6)) != X_6 ) ),
inference(negUnitSimplification,[status(thm)],[c_362,c_30]) ).
tff(c_368,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_367]) ).
tff(c_371,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_368,c_85]) ).
tff(c_372,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( g(f('#skF_2')) = '#skF_2' ) ),
inference(splitRight,[status(thm)],[c_367]) ).
tff(c_373,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_372]) ).
tff(c_361,plain,
g(f('#skF_3')) = '#skF_3',
inference(splitRight,[status(thm)],[c_99]) ).
tff(c_376,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_373,c_361]) ).
tff(c_377,plain,
g(f('#skF_2')) = '#skF_2',
inference(splitRight,[status(thm)],[c_372]) ).
tff(c_422,plain,
f('#skF_2') = '#skF_6',
inference(superposition,[status(thm),theory(equality)],[c_377,c_406]) ).
tff(c_449,plain,
f('#skF_2') = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_426,c_422]) ).
tff(c_450,plain,
g('#skF_1') = '#skF_2',
inference(demodulation,[status(thm),theory(equality)],[c_449,c_377]) ).
tff(c_465,plain,
'#skF_2' = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_444,c_450]) ).
tff(c_467,plain,
'#skF_3' != '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_465,c_74]) ).
tff(c_423,plain,
f('#skF_3') = '#skF_6',
inference(superposition,[status(thm),theory(equality)],[c_361,c_406]) ).
tff(c_437,plain,
f('#skF_3') = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_426,c_423]) ).
tff(c_438,plain,
g('#skF_1') = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_437,c_361]) ).
tff(c_480,plain,
'#skF_3' = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_444,c_438]) ).
tff(c_481,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_467,c_480]) ).
tff(c_483,plain,
f(g('#skF_6')) != '#skF_6',
inference(splitRight,[status(thm)],[c_84]) ).
tff(c_12,plain,
! [Z_2,Y_1,X_6] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( f(g('#skF_6')) = '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_515,plain,
! [Z_2,Y_1,X_6] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( f(g(X_6)) != X_6 ) ),
inference(negUnitSimplification,[status(thm)],[c_483,c_12]) ).
tff(c_516,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_515]) ).
tff(c_519,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_516,c_510]) ).
tff(c_521,plain,
! [Z_24,Y_25] :
( ( Z_24 = Y_25 )
| ( f(g(Z_24)) != Z_24 )
| ( f(g(Y_25)) != Y_25 ) ),
inference(splitRight,[status(thm)],[c_515]) ).
tff(c_537,plain,
! [Y_26] :
( ( Y_26 = '#skF_5' )
| ( f(g(Y_26)) != Y_26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_510,c_521]) ).
tff(c_557,plain,
'#skF_5' = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_67,c_537]) ).
tff(c_558,plain,
f('#skF_4') = '#skF_5',
inference(superposition,[status(thm),theory(equality)],[c_51,c_537]) ).
tff(c_567,plain,
f('#skF_4') = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_557,c_558]) ).
tff(c_568,plain,
g('#skF_1') = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_567,c_51]) ).
tff(c_20,plain,
! [X_3,X_6] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_6')) = '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_488,plain,
! [X_3,X_6] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( f(g(X_6)) != X_6 ) ),
inference(negUnitSimplification,[status(thm)],[c_483,c_20]) ).
tff(c_489,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_488]) ).
tff(c_491,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_489,c_67]) ).
tff(c_492,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( g(f('#skF_2')) = '#skF_2' ) ),
inference(splitRight,[status(thm)],[c_488]) ).
tff(c_493,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_492]) ).
tff(c_482,plain,
g(f('#skF_3')) = '#skF_3',
inference(splitRight,[status(thm)],[c_84]) ).
tff(c_496,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_493,c_482]) ).
tff(c_497,plain,
g(f('#skF_2')) = '#skF_2',
inference(splitRight,[status(thm)],[c_492]) ).
tff(c_555,plain,
f('#skF_2') = '#skF_5',
inference(superposition,[status(thm),theory(equality)],[c_497,c_537]) ).
tff(c_573,plain,
f('#skF_2') = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_557,c_555]) ).
tff(c_574,plain,
g('#skF_1') = '#skF_2',
inference(demodulation,[status(thm),theory(equality)],[c_573,c_497]) ).
tff(c_589,plain,
'#skF_2' = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_568,c_574]) ).
tff(c_591,plain,
'#skF_3' != '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_589,c_74]) ).
tff(c_556,plain,
f('#skF_3') = '#skF_5',
inference(superposition,[status(thm),theory(equality)],[c_482,c_537]) ).
tff(c_608,plain,
f('#skF_3') = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_557,c_556]) ).
tff(c_609,plain,
g('#skF_1') = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_608,c_482]) ).
tff(c_610,plain,
'#skF_3' = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_568,c_609]) ).
tff(c_612,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_591,c_610]) ).
tff(c_615,plain,
! [Z_28,Y_29] :
( ( Z_28 = Y_29 )
| ( f(g(Z_28)) != Z_28 )
| ( f(g(Y_29)) != Y_29 ) ),
inference(splitRight,[status(thm)],[c_509]) ).
tff(c_629,plain,
! [Y_30] :
( ( Y_30 = '#skF_1' )
| ( f(g(Y_30)) != Y_30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_67,c_615]) ).
tff(c_646,plain,
f('#skF_4') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_51,c_629]) ).
tff(c_652,plain,
g('#skF_1') = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_646,c_51]) ).
tff(c_642,plain,
f('#skF_2') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_497,c_629]) ).
tff(c_647,plain,
g('#skF_1') = '#skF_2',
inference(demodulation,[status(thm),theory(equality)],[c_642,c_497]) ).
tff(c_673,plain,
'#skF_2' = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_652,c_647]) ).
tff(c_689,plain,
'#skF_3' != '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_673,c_74]) ).
tff(c_643,plain,
f('#skF_3') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_482,c_629]) ).
tff(c_695,plain,
g('#skF_1') = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_643,c_482]) ).
tff(c_696,plain,
'#skF_3' = '#skF_4',
inference(demodulation,[status(thm),theory(equality)],[c_652,c_695]) ).
tff(c_698,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_689,c_696]) ).
tff(c_699,plain,
! [X_6,X_3] :
( ( f(g(X_6)) != X_6 )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_6')) = '#skF_6' ) ),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_705,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_699]) ).
tff(c_707,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_705,c_51]) ).
tff(c_708,plain,
! [X_6] :
( ( f(g(X_6)) != X_6 )
| ( f(g('#skF_6')) = '#skF_6' ) ),
inference(splitRight,[status(thm)],[c_699]) ).
tff(c_709,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_708]) ).
tff(c_711,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_709,c_67]) ).
tff(c_712,plain,
f(g('#skF_6')) = '#skF_6',
inference(splitRight,[status(thm)],[c_708]) ).
tff(c_700,plain,
'#skF_2' = '#skF_3',
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_36,plain,
! [X_3,Z_5,Y_4] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_737,plain,
! [X_3,Z_5,Y_4] :
( ( g(f(X_3)) != X_3 )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_700,c_36]) ).
tff(c_738,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_737]) ).
tff(c_740,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_738,c_51]) ).
tff(c_742,plain,
! [Z_31,Y_32] :
( ( Z_31 = Y_32 )
| ( g(f(Z_31)) != Z_31 )
| ( g(f(Y_32)) != Y_32 ) ),
inference(splitRight,[status(thm)],[c_737]) ).
tff(c_756,plain,
! [Y_33] :
( ( Y_33 = '#skF_4' )
| ( g(f(Y_33)) != Y_33 ) ),
inference(superposition,[status(thm),theory(equality)],[c_51,c_742]) ).
tff(c_770,plain,
g('#skF_6') = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_712,c_756]) ).
tff(c_779,plain,
f('#skF_4') = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_770,c_712]) ).
tff(c_26,plain,
! [X_3,X_6] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( f(g('#skF_5')) = '#skF_5' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_719,plain,
! [X_3,X_6] :
( ( g(f(X_3)) != X_3 )
| ( f(g('#skF_5')) = '#skF_5' )
| ( f(g(X_6)) != X_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_700,c_26]) ).
tff(c_720,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_719]) ).
tff(c_723,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_720,c_712]) ).
tff(c_724,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( f(g('#skF_5')) = '#skF_5' ) ),
inference(splitRight,[status(thm)],[c_719]) ).
tff(c_726,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_724]) ).
tff(c_728,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_726,c_51]) ).
tff(c_729,plain,
f(g('#skF_5')) = '#skF_5',
inference(splitRight,[status(thm)],[c_724]) ).
tff(c_769,plain,
g('#skF_5') = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_729,c_756]) ).
tff(c_774,plain,
f('#skF_4') = '#skF_5',
inference(demodulation,[status(thm),theory(equality)],[c_769,c_729]) ).
tff(c_806,plain,
'#skF_5' = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_779,c_774]) ).
tff(c_808,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57,c_806]) ).
tff(c_810,plain,
f(g('#skF_1')) != '#skF_1',
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_14,plain,
! [X_6] :
( ( f(g('#skF_1')) = '#skF_1' )
| ( f(g('#skF_6')) = '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_816,plain,
! [X_6] :
( ( f(g('#skF_6')) = '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(negUnitSimplification,[status(thm)],[c_810,c_14]) ).
tff(c_817,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_816]) ).
tff(c_809,plain,
f(g('#skF_5')) = '#skF_5',
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_819,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_817,c_809]) ).
tff(c_820,plain,
f(g('#skF_6')) = '#skF_6',
inference(splitRight,[status(thm)],[c_816]) ).
tff(c_34,plain,
! [Z_5,Y_4] :
( ( f(g('#skF_1')) = '#skF_1' )
| ( Z_5 = Y_4 )
| ( g(f(Z_5)) != Z_5 )
| ( g(f(Y_4)) != Y_4 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_827,plain,
! [Z_34,Y_35] :
( ( Z_34 = Y_35 )
| ( g(f(Z_34)) != Z_34 )
| ( g(f(Y_35)) != Y_35 ) ),
inference(negUnitSimplification,[status(thm)],[c_810,c_34]) ).
tff(c_837,plain,
! [Y_36] :
( ( Y_36 = '#skF_4' )
| ( g(f(Y_36)) != Y_36 ) ),
inference(superposition,[status(thm),theory(equality)],[c_51,c_827]) ).
tff(c_847,plain,
g('#skF_6') = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_820,c_837]) ).
tff(c_851,plain,
f('#skF_4') = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_847,c_820]) ).
tff(c_848,plain,
g('#skF_5') = '#skF_4',
inference(superposition,[status(thm),theory(equality)],[c_809,c_837]) ).
tff(c_857,plain,
f('#skF_4') = '#skF_5',
inference(demodulation,[status(thm),theory(equality)],[c_848,c_809]) ).
tff(c_878,plain,
'#skF_5' = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_851,c_857]) ).
tff(c_879,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57,c_878]) ).
tff(c_881,plain,
'#skF_5' = '#skF_6',
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_6,plain,
! [X_3,X_6] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( '#skF_5' != '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_901,plain,
! [X_3,X_6] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( f(g(X_6)) != X_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_881,c_6]) ).
tff(c_902,plain,
'#skF_2' != '#skF_3',
inference(splitLeft,[status(thm)],[c_901]) ).
tff(c_8,plain,
! [X_3,X_6] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( '#skF_5' != '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_906,plain,
! [X_3,X_6] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( f(g(X_6)) != X_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_881,c_8]) ).
tff(c_907,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_906]) ).
tff(c_880,plain,
! [X_6] :
( ( f(g(X_6)) != X_6 )
| ( f(g('#skF_1')) = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_887,plain,
! [X_37] : ( f(g(X_37)) != X_37 ),
inference(splitLeft,[status(thm)],[c_880]) ).
tff(c_892,plain,
$false,
inference(superposition,[status(thm),theory(equality)],[c_51,c_887]) ).
tff(c_893,plain,
f(g('#skF_1')) = '#skF_1',
inference(splitRight,[status(thm)],[c_880]) ).
tff(c_909,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_907,c_893]) ).
tff(c_910,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( g(f('#skF_3')) = '#skF_3' ) ),
inference(splitRight,[status(thm)],[c_906]) ).
tff(c_911,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_910]) ).
tff(c_913,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_911,c_51]) ).
tff(c_914,plain,
g(f('#skF_3')) = '#skF_3',
inference(splitRight,[status(thm)],[c_910]) ).
tff(c_2,plain,
! [Z_2,Y_1,X_6] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( '#skF_5' != '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_940,plain,
! [Z_2,Y_1,X_6] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( f(g(X_6)) != X_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_881,c_2]) ).
tff(c_941,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_940]) ).
tff(c_943,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_941,c_893]) ).
tff(c_945,plain,
! [Z_38,Y_39] :
( ( Z_38 = Y_39 )
| ( f(g(Z_38)) != Z_38 )
| ( f(g(Y_39)) != Y_39 ) ),
inference(splitRight,[status(thm)],[c_940]) ).
tff(c_958,plain,
! [Y_40] :
( ( Y_40 = '#skF_1' )
| ( f(g(Y_40)) != Y_40 ) ),
inference(superposition,[status(thm),theory(equality)],[c_893,c_945]) ).
tff(c_972,plain,
f('#skF_3') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_914,c_958]) ).
tff(c_983,plain,
g('#skF_1') = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_972,c_914]) ).
tff(c_10,plain,
! [X_3,X_6] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( '#skF_5' != '#skF_6' )
| ( f(g(X_6)) != X_6 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_921,plain,
! [X_3,X_6] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( f(g(X_6)) != X_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_881,c_10]) ).
tff(c_922,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitLeft,[status(thm)],[c_921]) ).
tff(c_924,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_922,c_893]) ).
tff(c_925,plain,
! [X_3] :
( ( g(f(X_3)) != X_3 )
| ( g(f('#skF_2')) = '#skF_2' ) ),
inference(splitRight,[status(thm)],[c_921]) ).
tff(c_926,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_925]) ).
tff(c_929,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_926,c_914]) ).
tff(c_930,plain,
g(f('#skF_2')) = '#skF_2',
inference(splitRight,[status(thm)],[c_925]) ).
tff(c_971,plain,
f('#skF_2') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_930,c_958]) ).
tff(c_976,plain,
g('#skF_1') = '#skF_2',
inference(demodulation,[status(thm),theory(equality)],[c_971,c_930]) ).
tff(c_1012,plain,
'#skF_2' = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_983,c_976]) ).
tff(c_1014,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_902,c_1012]) ).
tff(c_1015,plain,
! [X_6,X_3] :
( ( f(g(X_6)) != X_6 )
| ( g(f(X_3)) != X_3 ) ),
inference(splitRight,[status(thm)],[c_901]) ).
tff(c_1021,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_1015]) ).
tff(c_1023,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1021,c_51]) ).
tff(c_1024,plain,
! [X_6] : ( f(g(X_6)) != X_6 ),
inference(splitRight,[status(thm)],[c_1015]) ).
tff(c_1026,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1024,c_893]) ).
tff(c_1027,plain,
f(g('#skF_1')) = '#skF_1',
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_1028,plain,
g(f('#skF_4')) != '#skF_4',
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_46,plain,
! [X_3] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( g(f('#skF_4')) = '#skF_4' ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_1034,plain,
! [X_3] :
( ( '#skF_2' != '#skF_3' )
| ( g(f(X_3)) != X_3 ) ),
inference(negUnitSimplification,[status(thm)],[c_1028,c_46]) ).
tff(c_1035,plain,
'#skF_2' != '#skF_3',
inference(splitLeft,[status(thm)],[c_1034]) ).
tff(c_48,plain,
! [X_3] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 )
| ( g(f('#skF_4')) = '#skF_4' ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_1036,plain,
! [X_3] :
( ( g(f('#skF_3')) = '#skF_3' )
| ( g(f(X_3)) != X_3 ) ),
inference(negUnitSimplification,[status(thm)],[c_1028,c_48]) ).
tff(c_1038,plain,
! [X_41] : ( g(f(X_41)) != X_41 ),
inference(splitLeft,[status(thm)],[c_1036]) ).
tff(c_1043,plain,
$false,
inference(superposition,[status(thm),theory(equality)],[c_1027,c_1038]) ).
tff(c_1044,plain,
g(f('#skF_3')) = '#skF_3',
inference(splitRight,[status(thm)],[c_1036]) ).
tff(c_42,plain,
! [Z_2,Y_1] :
( ( Z_2 = Y_1 )
| ( f(g(Z_2)) != Z_2 )
| ( f(g(Y_1)) != Y_1 )
| ( g(f('#skF_4')) = '#skF_4' ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_1063,plain,
! [Z_42,Y_43] :
( ( Z_42 = Y_43 )
| ( f(g(Z_42)) != Z_42 )
| ( f(g(Y_43)) != Y_43 ) ),
inference(negUnitSimplification,[status(thm)],[c_1028,c_42]) ).
tff(c_1074,plain,
! [Y_44] :
( ( Y_44 = '#skF_1' )
| ( f(g(Y_44)) != Y_44 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1027,c_1063]) ).
tff(c_1085,plain,
f('#skF_3') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_1044,c_1074]) ).
tff(c_1093,plain,
g('#skF_1') = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_1085,c_1044]) ).
tff(c_50,plain,
! [X_3] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 )
| ( g(f('#skF_4')) = '#skF_4' ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_1050,plain,
! [X_3] :
( ( g(f('#skF_2')) = '#skF_2' )
| ( g(f(X_3)) != X_3 ) ),
inference(negUnitSimplification,[status(thm)],[c_1028,c_50]) ).
tff(c_1051,plain,
! [X_3] : ( g(f(X_3)) != X_3 ),
inference(splitLeft,[status(thm)],[c_1050]) ).
tff(c_1053,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1051,c_1044]) ).
tff(c_1054,plain,
g(f('#skF_2')) = '#skF_2',
inference(splitRight,[status(thm)],[c_1050]) ).
tff(c_1084,plain,
f('#skF_2') = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_1054,c_1074]) ).
tff(c_1088,plain,
g('#skF_1') = '#skF_2',
inference(demodulation,[status(thm),theory(equality)],[c_1084,c_1054]) ).
tff(c_1116,plain,
'#skF_2' = '#skF_3',
inference(demodulation,[status(thm),theory(equality)],[c_1093,c_1088]) ).
tff(c_1118,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1035,c_1116]) ).
tff(c_1125,plain,
! [X_45] : ( g(f(X_45)) != X_45 ),
inference(splitRight,[status(thm)],[c_1034]) ).
tff(c_1130,plain,
$false,
inference(superposition,[status(thm),theory(equality)],[c_1027,c_1125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : SYN551+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% 0.03/0.10 % 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.09/0.32 % Computer : n031.cluster.edu
% 0.09/0.32 % Model : x86_64 x86_64
% 0.09/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.32 % Memory : 8042.1875MB
% 0.09/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.32 % CPULimit : 300
% 0.09/0.32 % WCLimit : 300
% 0.09/0.32 % DateTime : Wed Apr 9 07:59:52 EDT 2025
% 0.09/0.32 % CPUTime :
% 4.16/2.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.46/2.60
% 4.46/2.60 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------