%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ134_2 : TPTP v9.0.0. Released v5.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 : n026.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 08:25:21 PM UTC 2025
% Result : Theorem 4.33s 2.01s
% Output : CNFRefutation 4.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of formulae : 44 ( 26 unt; 0 typ; 0 def)
% Number of atoms : 82 ( 28 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 65 ( 27 ~; 31 |; 5 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-1 aty)
% Number of variables : 21 ( 20 !; 1 ?; 21 :)
% Comments :
%------------------------------------------------------------------------------
%$ greater > #nlpp > job_of > age_of > synthetic_food_nutitionist > space_planner > lunar_energy_engineer > e > d > communications_consultant > c > b > airfoil_technician > a > #skF_1
%Foreground sorts:
tff(knowheyan,type,
knowheyan: $tType ).
tff(job,type,
job: $tType ).
tff(age,type,
age: $tType ).
%Background operators:
%Foreground operators:
tff(airfoil_technician,type,
airfoil_technician: job ).
tff(lunar_energy_engineer,type,
lunar_energy_engineer: job ).
tff(job_of,type,
job_of: knowheyan > job ).
tff(communications_consultant,type,
communications_consultant: job ).
tff(greater,type,
greater: ( age * age ) > $o ).
tff(d,type,
d: knowheyan ).
tff(age_of,type,
age_of: knowheyan > age ).
tff(space_planner,type,
space_planner: job ).
tff('#skF_1',type,
'#skF_1': knowheyan ).
tff(synthetic_food_nutitionist,type,
synthetic_food_nutitionist: job ).
tff(b,type,
b: knowheyan ).
tff(a,type,
a: knowheyan ).
tff(e,type,
e: knowheyan ).
tff(c,type,
c: knowheyan ).
tff(f_128,axiom,
! [X: age,Y: age] :
( ( X != Y )
<=> ( greater(X,Y)
| greater(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_greater) ).
tff(f_141,axiom,
greater(age_of(b),age_of(c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_info4) ).
tff(f_155,axiom,
? [X: knowheyan] : greater(age_of(c),age_of(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_not_youngest) ).
tff(f_116,axiom,
! [X: age,Y: age,Z: age] :
( ( greater(X,Y)
& greater(Y,Z) )
=> greater(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_transitive) ).
tff(f_88,axiom,
! [X: knowheyan] :
( ( X = a )
| ( X = b )
| ( X = c )
| ( X = d )
| ( X = e ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',only_knowheyans) ).
tff(f_135,axiom,
greater(age_of(a),age_of(d)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_info1) ).
tff(f_136,axiom,
greater(age_of(d),age_of(b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_info2) ).
tff(f_163,negated_conjecture,
~ ( greater(age_of(a),age_of(d))
& greater(age_of(d),age_of(b))
& greater(age_of(b),age_of(c))
& greater(age_of(c),age_of(e)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_order) ).
tff(f_121,axiom,
! [X: age,Y: age] :
~ ( greater(X,Y)
& greater(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',age_irreflexive) ).
tff(c_58,plain,
! [Y_13: age] : ~ greater(Y_13,Y_13),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_68,plain,
greater(age_of(b),age_of(c)),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_74,plain,
greater(age_of(c),age_of('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_206,plain,
! [X_34: age,Z_35: age,Y_36: age] :
( greater(X_34,Z_35)
| ~ greater(Y_36,Z_35)
| ~ greater(X_34,Y_36) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_452,plain,
! [X_56: age] :
( greater(X_56,age_of('#skF_1'))
| ~ greater(X_56,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_206]) ).
tff(c_470,plain,
greater(age_of(b),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_68,c_452]) ).
tff(c_267,plain,
! [X_38: knowheyan] :
( ( e = X_38 )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_62,plain,
greater(age_of(a),age_of(d)),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_64,plain,
greater(age_of(d),age_of(b)),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_76,plain,
( ~ greater(age_of(c),age_of(e))
| ~ greater(age_of(b),age_of(c))
| ~ greater(age_of(d),age_of(b))
| ~ greater(age_of(a),age_of(d)) ),
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_78,plain,
( ~ greater(age_of(c),age_of(e))
| ~ greater(age_of(d),age_of(b))
| ~ greater(age_of(a),age_of(d)) ),
inference(demodulation,[status(thm),theory(equality)],[c_68,c_76]) ).
tff(c_80,plain,
( ~ greater(age_of(c),age_of(e))
| ~ greater(age_of(a),age_of(d)) ),
inference(demodulation,[status(thm),theory(equality)],[c_64,c_78]) ).
tff(c_82,plain,
~ greater(age_of(c),age_of(e)),
inference(demodulation,[status(thm),theory(equality)],[c_62,c_80]) ).
tff(c_364,plain,
! [X_53: knowheyan] :
( ~ greater(age_of(c),age_of(X_53))
| ( d = X_53 )
| ( c = X_53 )
| ( b = X_53 )
| ( a = X_53 ) ),
inference(superposition,[status(thm),theory(equality)],[c_267,c_82]) ).
tff(c_390,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(resolution,[status(thm)],[c_74,c_364]) ).
tff(c_588,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_390]) ).
tff(c_228,plain,
! [X_37: age] :
( greater(X_37,age_of(b))
| ~ greater(X_37,age_of(d)) ),
inference(resolution,[status(thm)],[c_64,c_206]) ).
tff(c_242,plain,
greater(age_of(a),age_of(b)),
inference(resolution,[status(thm)],[c_62,c_228]) ).
tff(c_52,plain,
! [Y_11: age,X_10: age] :
( ~ greater(Y_11,X_10)
| ~ greater(X_10,Y_11) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_328,plain,
~ greater(age_of(b),age_of(a)),
inference(resolution,[status(thm)],[c_242,c_52]) ).
tff(c_591,plain,
~ greater(age_of(b),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_588,c_328]) ).
tff(c_602,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_470,c_591]) ).
tff(c_603,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_390]) ).
tff(c_646,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_603]) ).
tff(c_84,plain,
! [Y_23: age,X_24: age] :
( ~ greater(Y_23,X_24)
| ~ greater(X_24,Y_23) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_94,plain,
~ greater(age_of(b),age_of(d)),
inference(resolution,[status(thm)],[c_64,c_84]) ).
tff(c_654,plain,
~ greater(age_of(b),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_646,c_94]) ).
tff(c_663,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_470,c_654]) ).
tff(c_664,plain,
( ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_603]) ).
tff(c_666,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_664]) ).
tff(c_732,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_666,c_470]) ).
tff(c_753,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_732]) ).
tff(c_754,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_664]) ).
tff(c_765,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_754,c_74]) ).
tff(c_773,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_765]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : PUZ134_2 : TPTP v9.0.0. Released v5.1.0.
% 0.12/0.13 % 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.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 17:30:23 EDT 2025
% 0.21/0.34 % CPUTime :
% 4.33/2.01 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.33/2.01
% 4.33/2.01 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------