%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ134_1 : 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/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 : n002.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:20 PM UTC 2025
% Result : Theorem 40.59s 25.90s
% Output : CNFRefutation 40.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 24
% Syntax : Number of formulae : 776 ( 476 unt; 0 typ; 0 def)
% Number of atoms : 1450 (1114 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 1113 ( 439 ~; 659 |; 8 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 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 : 249 ( 247 !; 2 ?; 249 :)
% 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_48,axiom,
b != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_c) ).
tff(f_128,axiom,
! [X: age,Y: age] :
( ( X != Y )
<=> ( greater(X,Y)
| greater(Y,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_greater) ).
tff(f_141,axiom,
greater(age_of(b),age_of(c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info4) ).
tff(f_155,axiom,
? [X: knowheyan] : greater(age_of(c),age_of(X)),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',age_transitive) ).
tff(f_140,axiom,
! [X: knowheyan] :
( ( job_of(X) = lunar_energy_engineer )
=> greater(age_of(X),age_of(b)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info3) ).
tff(f_121,axiom,
! [X: age,Y: age] :
~ ( greater(X,Y)
& greater(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_irreflexive) ).
tff(f_136,axiom,
greater(age_of(d),age_of(b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info2) ).
tff(f_134,axiom,
! [X: knowheyan] :
( ( job_of(X) = communications_consultant )
=> ~ ? [Y: knowheyan] : greater(age_of(Y),age_of(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_younger) ).
tff(f_88,axiom,
! [X: knowheyan] :
( ( X = a )
| ( X = b )
| ( X = c )
| ( X = d )
| ( X = e ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_knowheyans) ).
tff(f_52,axiom,
b != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_e) ).
tff(f_46,axiom,
a != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_e) ).
tff(f_153,axiom,
! [X: knowheyan,Y: knowheyan] :
( ( ( job_of(X) = space_planner )
& ( job_of(Y) = synthetic_food_nutitionist ) )
=> greater(age_of(X),age_of(Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_job2) ).
tff(f_56,axiom,
c != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_e) ).
tff(f_98,axiom,
! [X: job] :
( ( X = airfoil_technician )
| ( X = communications_consultant )
| ( X = space_planner )
| ( X = lunar_energy_engineer )
| ( X = synthetic_food_nutitionist ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_jobs) ).
tff(f_147,axiom,
! [X: knowheyan,Y: knowheyan] :
( ( ( job_of(X) = airfoil_technician )
& ( job_of(Y) = space_planner ) )
=> greater(age_of(X),age_of(Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_job1) ).
tff(f_135,axiom,
greater(age_of(a),age_of(d)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info1) ).
tff(f_50,axiom,
b != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_d) ).
tff(f_110,axiom,
! [X: knowheyan,Y: knowheyan] :
( ( X != Y )
=> ( job_of(X) != job_of(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_jobs) ).
tff(f_44,axiom,
a != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_d) ).
tff(f_54,axiom,
c != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_d) ).
tff(f_40,axiom,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_b) ).
tff(f_165,negated_conjecture,
~ ( ( job_of(a) = communications_consultant )
& ( job_of(d) = lunar_energy_engineer )
& ( job_of(b) = airfoil_technician )
& ( job_of(c) = space_planner )
& ( job_of(e) = synthetic_food_nutitionist ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',known_jobs) ).
tff(f_58,axiom,
d != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_not_e) ).
tff(c_10,plain,
c != b,
inference(cnfTransformation,[status(thm)],[f_48]) ).
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_547839,plain,
! [X_6996: age,Z_6997: age,Y_6998: age] :
( greater(X_6996,Z_6997)
| ~ greater(Y_6998,Z_6997)
| ~ greater(X_6996,Y_6998) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_548037,plain,
! [X_7002: age] :
( greater(X_7002,age_of('#skF_1'))
| ~ greater(X_7002,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_547839]) ).
tff(c_548051,plain,
greater(age_of(b),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_68,c_548037]) ).
tff(c_547796,plain,
! [X_6993: knowheyan] :
( greater(age_of(X_6993),age_of(b))
| ( job_of(X_6993) != lunar_energy_engineer ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
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_547807,plain,
! [X_6993: knowheyan] :
( ~ greater(age_of(b),age_of(X_6993))
| ( job_of(X_6993) != lunar_energy_engineer ) ),
inference(resolution,[status(thm)],[c_547796,c_52]) ).
tff(c_548062,plain,
job_of('#skF_1') != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_548051,c_547807]) ).
tff(c_64,plain,
greater(age_of(d),age_of(b)),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_547809,plain,
! [Y_6994: knowheyan,X_6995: knowheyan] :
( ~ greater(age_of(Y_6994),age_of(X_6995))
| ( job_of(X_6995) != communications_consultant ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_547837,plain,
job_of(b) != communications_consultant,
inference(resolution,[status(thm)],[c_64,c_547809]) ).
tff(c_547808,plain,
job_of(b) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_547796,c_58]) ).
tff(c_547838,plain,
job_of('#skF_1') != communications_consultant,
inference(resolution,[status(thm)],[c_74,c_547809]) ).
tff(c_547927,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_14,plain,
e != b,
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_8,plain,
e != a,
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_483024,plain,
! [X_6137: knowheyan,Y_6138: knowheyan] :
( greater(age_of(X_6137),age_of(Y_6138))
| ( job_of(Y_6138) != synthetic_food_nutitionist )
| ( job_of(X_6137) != space_planner ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_482511,plain,
! [Y_6056: age,X_6057: age] :
( ~ greater(Y_6056,X_6057)
| ~ greater(X_6057,Y_6056) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_482523,plain,
~ greater(age_of('#skF_1'),age_of(c)),
inference(resolution,[status(thm)],[c_74,c_482511]) ).
tff(c_483077,plain,
( ( job_of(c) != synthetic_food_nutitionist )
| ( job_of('#skF_1') != space_planner ) ),
inference(resolution,[status(thm)],[c_483024,c_482523]) ).
tff(c_544796,plain,
job_of('#skF_1') != space_planner,
inference(splitLeft,[status(thm)],[c_483077]) ).
tff(c_66,plain,
! [X_17: knowheyan] :
( greater(age_of(X_17),age_of(b))
| ( job_of(X_17) != lunar_energy_engineer ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_482626,plain,
! [X_6065: age,Z_6066: age,Y_6067: age] :
( greater(X_6065,Z_6066)
| ~ greater(Y_6067,Z_6066)
| ~ greater(X_6065,Y_6067) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_482893,plain,
! [X_6124: age] :
( greater(X_6124,age_of(c))
| ~ greater(X_6124,age_of(b)) ),
inference(resolution,[status(thm)],[c_68,c_482626]) ).
tff(c_482911,plain,
~ greater(age_of('#skF_1'),age_of(b)),
inference(resolution,[status(thm)],[c_482893,c_482523]) ).
tff(c_482919,plain,
job_of('#skF_1') != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_66,c_482911]) ).
tff(c_544474,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_482961,plain,
! [X_6132: age] :
( greater(X_6132,age_of('#skF_1'))
| ~ greater(X_6132,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_482626]) ).
tff(c_482979,plain,
greater(age_of(b),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_68,c_482961]) ).
tff(c_18,plain,
e != c,
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_482597,plain,
! [Y_6063: knowheyan,X_6064: knowheyan] :
( ~ greater(age_of(Y_6063),age_of(X_6064))
| ( job_of(X_6064) != communications_consultant ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_482622,plain,
job_of(c) != communications_consultant,
inference(resolution,[status(thm)],[c_68,c_482597]) ).
tff(c_482520,plain,
~ greater(age_of(c),age_of(b)),
inference(resolution,[status(thm)],[c_68,c_482511]) ).
tff(c_483078,plain,
( ( job_of(b) != synthetic_food_nutitionist )
| ( job_of(c) != space_planner ) ),
inference(resolution,[status(thm)],[c_483024,c_482520]) ).
tff(c_483181,plain,
job_of(c) != space_planner,
inference(splitLeft,[status(thm)],[c_483078]) ).
tff(c_482584,plain,
! [X_6062: knowheyan] :
( greater(age_of(X_6062),age_of(b))
| ( job_of(X_6062) != lunar_energy_engineer ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_482594,plain,
job_of(c) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_482584,c_482520]) ).
tff(c_44,plain,
! [X_2: job] :
( ( synthetic_food_nutitionist = X_2 )
| ( lunar_energy_engineer = X_2 )
| ( space_planner = X_2 )
| ( communications_consultant = X_2 )
| ( airfoil_technician = X_2 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_483186,plain,
! [X_6148: knowheyan,Y_6149: knowheyan] :
( greater(age_of(X_6148),age_of(Y_6149))
| ( job_of(Y_6149) != space_planner )
| ( job_of(X_6148) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_482522,plain,
~ greater(age_of(b),age_of(d)),
inference(resolution,[status(thm)],[c_64,c_482511]) ).
tff(c_483248,plain,
( ( job_of(d) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_483186,c_482522]) ).
tff(c_483393,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_483248]) ).
tff(c_482624,plain,
job_of(b) != communications_consultant,
inference(resolution,[status(thm)],[c_64,c_482597]) ).
tff(c_70,plain,
! [X_18: knowheyan,Y_19: knowheyan] :
( greater(age_of(X_18),age_of(Y_19))
| ( job_of(Y_19) != space_planner )
| ( job_of(X_18) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_482644,plain,
! [X_6065: age] :
( greater(X_6065,age_of(c))
| ~ greater(X_6065,age_of(b)) ),
inference(resolution,[status(thm)],[c_68,c_482626]) ).
tff(c_483485,plain,
! [X_6163: age] :
( greater(X_6163,age_of('#skF_1'))
| ~ greater(X_6163,age_of(b)) ),
inference(resolution,[status(thm)],[c_482644,c_482961]) ).
tff(c_483521,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_483485]) ).
tff(c_528756,plain,
~ greater(age_of('#skF_1'),age_of(d)),
inference(resolution,[status(thm)],[c_483521,c_52]) ).
tff(c_528768,plain,
( ( job_of(d) != space_planner )
| ( job_of('#skF_1') != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_70,c_528756]) ).
tff(c_528788,plain,
job_of('#skF_1') != airfoil_technician,
inference(splitLeft,[status(thm)],[c_528768]) ).
tff(c_483132,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_482672,plain,
! [X_6068: job] :
( ( synthetic_food_nutitionist = X_6068 )
| ( lunar_energy_engineer = X_6068 )
| ( space_planner = X_6068 )
| ( communications_consultant = X_6068 )
| ( airfoil_technician = X_6068 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_539,plain,
! [X_112: knowheyan,Y_113: knowheyan] :
( greater(age_of(X_112),age_of(Y_113))
| ( job_of(Y_113) != synthetic_food_nutitionist )
| ( job_of(X_112) != space_planner ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_84,plain,
! [Y_25: age,X_26: age] :
( ~ greater(Y_25,X_26)
| ~ greater(X_26,Y_25) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_96,plain,
~ greater(age_of(c),age_of(b)),
inference(resolution,[status(thm)],[c_68,c_84]) ).
tff(c_590,plain,
( ( job_of(b) != synthetic_food_nutitionist )
| ( job_of(c) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_96]) ).
tff(c_433700,plain,
job_of(c) != space_planner,
inference(splitLeft,[status(thm)],[c_590]) ).
tff(c_102,plain,
! [Y_29: knowheyan,X_30: knowheyan] :
( ~ greater(age_of(Y_29),age_of(X_30))
| ( job_of(X_30) != communications_consultant ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_118,plain,
job_of(c) != communications_consultant,
inference(resolution,[status(thm)],[c_68,c_102]) ).
tff(c_182,plain,
! [X_33: knowheyan] :
( greater(age_of(X_33),age_of(b))
| ( job_of(X_33) != lunar_energy_engineer ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_196,plain,
job_of(c) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_182,c_96]) ).
tff(c_93,plain,
~ greater(age_of('#skF_1'),age_of(c)),
inference(resolution,[status(thm)],[c_74,c_84]) ).
tff(c_286,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_263,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_287,plain,
! [X_38: knowheyan] :
( ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_286,c_263]) ).
tff(c_430561,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_287]) ).
tff(c_62,plain,
greater(age_of(a),age_of(d)),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_217,plain,
! [X_35: age,Z_36: age,Y_37: age] :
( greater(X_35,Z_36)
| ~ greater(Y_37,Z_36)
| ~ greater(X_35,Y_37) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_520,plain,
! [X_110: age] :
( greater(X_110,age_of(b))
| ~ greater(X_110,age_of(d)) ),
inference(resolution,[status(thm)],[c_64,c_217]) ).
tff(c_538,plain,
greater(age_of(a),age_of(b)),
inference(resolution,[status(thm)],[c_62,c_520]) ).
tff(c_54,plain,
! [Y_13: age,X_12: age] :
( greater(Y_13,X_12)
| greater(X_12,Y_13)
| ( Y_13 = X_12 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_236,plain,
! [X_35: age] :
( greater(X_35,age_of(d))
| ~ greater(X_35,age_of(a)) ),
inference(resolution,[status(thm)],[c_62,c_217]) ).
tff(c_456,plain,
! [X_105: age] :
( greater(X_105,age_of(c))
| ~ greater(X_105,age_of(b)) ),
inference(resolution,[status(thm)],[c_68,c_217]) ).
tff(c_425029,plain,
! [X_5171: age] :
( ~ greater(age_of(c),X_5171)
| ~ greater(X_5171,age_of(b)) ),
inference(resolution,[status(thm)],[c_456,c_52]) ).
tff(c_425038,plain,
( ~ greater(age_of(d),age_of(b))
| ~ greater(age_of(c),age_of(a)) ),
inference(resolution,[status(thm)],[c_236,c_425029]) ).
tff(c_425060,plain,
~ greater(age_of(c),age_of(a)),
inference(demodulation,[status(thm),theory(equality)],[c_64,c_425038]) ).
tff(c_425085,plain,
( greater(age_of(a),age_of(c))
| ( age_of(c) = age_of(a) ) ),
inference(resolution,[status(thm)],[c_54,c_425060]) ).
tff(c_425587,plain,
age_of(c) = age_of(a),
inference(splitLeft,[status(thm)],[c_425085]) ).
tff(c_425592,plain,
~ greater(age_of(a),age_of(b)),
inference(demodulation,[status(thm),theory(equality)],[c_425587,c_96]) ).
tff(c_425598,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_538,c_425592]) ).
tff(c_425600,plain,
age_of(c) != age_of(a),
inference(splitRight,[status(thm)],[c_425085]) ).
tff(c_425084,plain,
( greater(age_of(a),age_of(c))
| ( age_of(c) = age_of(a) ) ),
inference(resolution,[status(thm)],[c_54,c_425060]) ).
tff(c_425601,plain,
greater(age_of(a),age_of(c)),
inference(negUnitSimplification,[status(thm)],[c_425600,c_425084]) ).
tff(c_430578,plain,
greater(age_of('#skF_1'),age_of(c)),
inference(demodulation,[status(thm),theory(equality)],[c_430561,c_425601]) ).
tff(c_430599,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_93,c_430578]) ).
tff(c_430600,plain,
! [X_38: knowheyan] :
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' )
| ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(splitRight,[status(thm)],[c_287]) ).
tff(c_431236,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_430600]) ).
tff(c_235,plain,
! [X_35: age] :
( greater(X_35,age_of('#skF_1'))
| ~ greater(X_35,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_217]) ).
tff(c_425090,plain,
! [X_5175: age] :
( greater(X_5175,age_of('#skF_1'))
| ~ greater(X_5175,age_of(b)) ),
inference(resolution,[status(thm)],[c_456,c_235]) ).
tff(c_425122,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_425090]) ).
tff(c_431260,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_431236,c_425122]) ).
tff(c_431275,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_431260]) ).
tff(c_431276,plain,
! [X_38: knowheyan] :
( ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(splitRight,[status(thm)],[c_430600]) ).
tff(c_431907,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_431276]) ).
tff(c_314,plain,
! [X_52: age] :
( greater(X_52,age_of('#skF_1'))
| ~ greater(X_52,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_217]) ).
tff(c_328,plain,
greater(age_of(b),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_68,c_314]) ).
tff(c_431948,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_431907,c_328]) ).
tff(c_431962,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_431948]) ).
tff(c_431963,plain,
! [X_38: knowheyan] :
( ( c = '#skF_1' )
| ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(splitRight,[status(thm)],[c_431276]) ).
tff(c_432135,plain,
c = '#skF_1',
inference(splitLeft,[status(thm)],[c_431963]) ).
tff(c_432165,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_432135,c_74]) ).
tff(c_432173,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_432165]) ).
tff(c_432175,plain,
c != '#skF_1',
inference(splitRight,[status(thm)],[c_431963]) ).
tff(c_115,plain,
job_of('#skF_1') != communications_consultant,
inference(resolution,[status(thm)],[c_74,c_102]) ).
tff(c_431964,plain,
b != '#skF_1',
inference(splitRight,[status(thm)],[c_431276]) ).
tff(c_610,plain,
! [X_118: knowheyan,Y_119: knowheyan] :
( greater(age_of(X_118),age_of(Y_119))
| ( job_of(Y_119) != space_planner )
| ( job_of(X_118) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_486,plain,
! [X_107: age] :
( greater(X_107,age_of(d))
| ~ greater(X_107,age_of(a)) ),
inference(resolution,[status(thm)],[c_62,c_217]) ).
tff(c_95,plain,
~ greater(age_of(b),age_of(d)),
inference(resolution,[status(thm)],[c_64,c_84]) ).
tff(c_509,plain,
~ greater(age_of(b),age_of(a)),
inference(resolution,[status(thm)],[c_486,c_95]) ).
tff(c_653,plain,
( ( job_of(a) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_509]) ).
tff(c_424984,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_653]) ).
tff(c_117,plain,
job_of(b) != communications_consultant,
inference(resolution,[status(thm)],[c_64,c_102]) ).
tff(c_384227,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_653]) ).
tff(c_661,plain,
( ( job_of(b) != space_planner )
| ( job_of(c) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_96]) ).
tff(c_678,plain,
job_of(c) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_661]) ).
tff(c_12,plain,
d != b,
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_582,plain,
( ( job_of(a) != synthetic_food_nutitionist )
| ( job_of(b) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_509]) ).
tff(c_346991,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_582]) ).
tff(c_198,plain,
job_of(b) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_182,c_58]) ).
tff(c_662,plain,
( ( job_of(c) != space_planner )
| ( job_of('#skF_1') != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_93]) ).
tff(c_27080,plain,
job_of('#skF_1') != airfoil_technician,
inference(splitLeft,[status(thm)],[c_662]) ).
tff(c_197,plain,
! [X_33: knowheyan] :
( ~ greater(age_of(b),age_of(X_33))
| ( job_of(X_33) != lunar_energy_engineer ) ),
inference(resolution,[status(thm)],[c_182,c_52]) ).
tff(c_340,plain,
job_of('#skF_1') != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_328,c_197]) ).
tff(c_591,plain,
( ( job_of(c) != synthetic_food_nutitionist )
| ( job_of('#skF_1') != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_93]) ).
tff(c_673,plain,
job_of('#skF_1') != space_planner,
inference(splitLeft,[status(thm)],[c_591]) ).
tff(c_312928,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_287]) ).
tff(c_305375,plain,
! [X_3793: age] :
( greater(X_3793,age_of(b))
| ~ greater(X_3793,age_of(a)) ),
inference(resolution,[status(thm)],[c_236,c_520]) ).
tff(c_305413,plain,
~ greater(age_of(c),age_of(a)),
inference(resolution,[status(thm)],[c_305375,c_96]) ).
tff(c_305432,plain,
( greater(age_of(a),age_of(c))
| ( age_of(c) = age_of(a) ) ),
inference(resolution,[status(thm)],[c_54,c_305413]) ).
tff(c_306157,plain,
age_of(c) = age_of(a),
inference(splitLeft,[status(thm)],[c_305432]) ).
tff(c_306162,plain,
~ greater(age_of(a),age_of(b)),
inference(demodulation,[status(thm),theory(equality)],[c_306157,c_96]) ).
tff(c_306168,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_538,c_306162]) ).
tff(c_306169,plain,
greater(age_of(a),age_of(c)),
inference(splitRight,[status(thm)],[c_305432]) ).
tff(c_312947,plain,
greater(age_of('#skF_1'),age_of(c)),
inference(demodulation,[status(thm),theory(equality)],[c_312928,c_306169]) ).
tff(c_312971,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_93,c_312947]) ).
tff(c_312972,plain,
! [X_38: knowheyan] :
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' )
| ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(splitRight,[status(thm)],[c_287]) ).
tff(c_313927,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_312972]) ).
tff(c_305484,plain,
! [X_3799: age] :
( greater(X_3799,age_of('#skF_1'))
| ~ greater(X_3799,age_of(b)) ),
inference(resolution,[status(thm)],[c_456,c_235]) ).
tff(c_305523,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_305484]) ).
tff(c_313951,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_313927,c_305523]) ).
tff(c_313966,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_313951]) ).
tff(c_313967,plain,
! [X_38: knowheyan] :
( ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(splitRight,[status(thm)],[c_312972]) ).
tff(c_314634,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_313967]) ).
tff(c_223808,plain,
! [Y_2914: knowheyan,X_2915: knowheyan] :
( ~ greater(age_of(Y_2914),age_of(X_2915))
| ( job_of(Y_2914) != space_planner )
| ( job_of(X_2915) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_52]) ).
tff(c_223858,plain,
! [X_17: knowheyan] :
( ( job_of(X_17) != space_planner )
| ( job_of(b) != airfoil_technician )
| ( job_of(X_17) != lunar_energy_engineer ) ),
inference(resolution,[status(thm)],[c_66,c_223808]) ).
tff(c_224507,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_223858]) ).
tff(c_223798,plain,
job_of(c) != space_planner,
inference(splitLeft,[status(thm)],[c_590]) ).
tff(c_584,plain,
! [X_112: knowheyan] :
( greater(age_of(X_112),age_of('#skF_1'))
| ( job_of(c) != synthetic_food_nutitionist )
| ( job_of(X_112) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_235]) ).
tff(c_264671,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_264810,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_264671]) ).
tff(c_264814,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_678,c_118,c_223798,c_196,c_264810]) ).
tff(c_264816,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_367,plain,
! [X_53: job] :
( ( synthetic_food_nutitionist = X_53 )
| ( lunar_energy_engineer = X_53 )
| ( space_planner = X_53 )
| ( communications_consultant = X_53 )
| ( airfoil_technician = X_53 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_48,plain,
! [Y_6: knowheyan,X_5: knowheyan] :
( ( job_of(Y_6) != job_of(X_5) )
| ( Y_6 = X_5 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_268951,plain,
! [X_3428: knowheyan,Y_3429: knowheyan] :
( ( job_of(X_3428) != synthetic_food_nutitionist )
| ( Y_3429 = X_3428 )
| ( job_of(Y_3429) = lunar_energy_engineer )
| ( job_of(Y_3429) = space_planner )
| ( job_of(Y_3429) = communications_consultant )
| ( job_of(Y_3429) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_304952,plain,
! [Y_3774: knowheyan] :
( ( c = Y_3774 )
| ( job_of(Y_3774) = lunar_energy_engineer )
| ( job_of(Y_3774) = space_planner )
| ( job_of(Y_3774) = communications_consultant )
| ( job_of(Y_3774) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_264816,c_268951]) ).
tff(c_223803,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_582]) ).
tff(c_304988,plain,
( ( c = b )
| ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_304952,c_223803]) ).
tff(c_305057,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_224507,c_117,c_198,c_10,c_304988]) ).
tff(c_305059,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_223858]) ).
tff(c_270,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_42,plain,
! [X_1: knowheyan] :
( ( e = X_1 )
| ( d = X_1 )
| ( c = X_1 )
| ( b = X_1 )
| ( a = X_1 ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_271,plain,
! [X_1: knowheyan] :
( ( X_1 = '#skF_1' )
| ( d = X_1 )
| ( c = X_1 )
| ( b = X_1 )
| ( a = X_1 )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_270,c_42]) ).
tff(c_152820,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_271]) ).
tff(c_146154,plain,
! [X_2077: age] :
( greater(X_2077,age_of(b))
| ~ greater(X_2077,age_of(a)) ),
inference(resolution,[status(thm)],[c_236,c_520]) ).
tff(c_146186,plain,
~ greater(age_of(c),age_of(a)),
inference(resolution,[status(thm)],[c_146154,c_96]) ).
tff(c_146206,plain,
( greater(age_of(a),age_of(c))
| ( age_of(c) = age_of(a) ) ),
inference(resolution,[status(thm)],[c_54,c_146186]) ).
tff(c_147112,plain,
age_of(c) = age_of(a),
inference(splitLeft,[status(thm)],[c_146206]) ).
tff(c_147118,plain,
~ greater(age_of(a),age_of(b)),
inference(demodulation,[status(thm),theory(equality)],[c_147112,c_96]) ).
tff(c_147124,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_538,c_147118]) ).
tff(c_147125,plain,
greater(age_of(a),age_of(c)),
inference(splitRight,[status(thm)],[c_146206]) ).
tff(c_152834,plain,
greater(age_of('#skF_1'),age_of(c)),
inference(demodulation,[status(thm),theory(equality)],[c_152820,c_147125]) ).
tff(c_152857,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_93,c_152834]) ).
tff(c_152858,plain,
! [X_1: knowheyan] :
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' )
| ( X_1 = '#skF_1' )
| ( d = X_1 )
| ( c = X_1 )
| ( b = X_1 )
| ( a = X_1 ) ),
inference(splitRight,[status(thm)],[c_271]) ).
tff(c_153754,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_152858]) ).
tff(c_146357,plain,
! [X_2088: age] :
( greater(X_2088,age_of('#skF_1'))
| ~ greater(X_2088,age_of(b)) ),
inference(resolution,[status(thm)],[c_456,c_235]) ).
tff(c_146396,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_146357]) ).
tff(c_153775,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_153754,c_146396]) ).
tff(c_153791,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_153775]) ).
tff(c_153792,plain,
! [X_1: knowheyan] :
( ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( X_1 = '#skF_1' )
| ( d = X_1 )
| ( c = X_1 )
| ( b = X_1 )
| ( a = X_1 ) ),
inference(splitRight,[status(thm)],[c_152858]) ).
tff(c_154787,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_153792]) ).
tff(c_6,plain,
d != a,
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_94,plain,
~ greater(age_of(d),age_of(a)),
inference(resolution,[status(thm)],[c_62,c_84]) ).
tff(c_659,plain,
( ( job_of(a) != space_planner )
| ( job_of(d) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_94]) ).
tff(c_27085,plain,
job_of(d) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_659]) ).
tff(c_116,plain,
job_of(d) != communications_consultant,
inference(resolution,[status(thm)],[c_62,c_102]) ).
tff(c_588,plain,
( ( job_of(a) != synthetic_food_nutitionist )
| ( job_of(d) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_94]) ).
tff(c_609,plain,
job_of(d) != space_planner,
inference(splitLeft,[status(thm)],[c_588]) ).
tff(c_142580,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_271]) ).
tff(c_134935,plain,
! [X_1770: age] :
( greater(X_1770,age_of(b))
| ~ greater(X_1770,age_of(a)) ),
inference(resolution,[status(thm)],[c_236,c_520]) ).
tff(c_134971,plain,
~ greater(age_of(c),age_of(a)),
inference(resolution,[status(thm)],[c_134935,c_96]) ).
tff(c_135032,plain,
( greater(age_of(a),age_of(c))
| ( age_of(c) = age_of(a) ) ),
inference(resolution,[status(thm)],[c_54,c_134971]) ).
tff(c_137372,plain,
age_of(c) = age_of(a),
inference(splitLeft,[status(thm)],[c_135032]) ).
tff(c_137377,plain,
~ greater(age_of(a),age_of(b)),
inference(demodulation,[status(thm),theory(equality)],[c_137372,c_96]) ).
tff(c_137383,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_538,c_137377]) ).
tff(c_137384,plain,
greater(age_of(a),age_of(c)),
inference(splitRight,[status(thm)],[c_135032]) ).
tff(c_142597,plain,
greater(age_of('#skF_1'),age_of(c)),
inference(demodulation,[status(thm),theory(equality)],[c_142580,c_137384]) ).
tff(c_142619,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_93,c_142597]) ).
tff(c_142621,plain,
a != '#skF_1',
inference(splitRight,[status(thm)],[c_271]) ).
tff(c_16,plain,
d != c,
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_60711,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_653]) ).
tff(c_60702,plain,
job_of(c) != space_planner,
inference(splitLeft,[status(thm)],[c_590]) ).
tff(c_102769,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_102772,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_102769]) ).
tff(c_102776,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_678,c_118,c_60702,c_196,c_102772]) ).
tff(c_102778,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_105074,plain,
! [Y_1456: knowheyan,X_1457: knowheyan] :
( ( job_of(Y_1456) != synthetic_food_nutitionist )
| ( Y_1456 = X_1457 )
| ( job_of(X_1457) = lunar_energy_engineer )
| ( job_of(X_1457) = space_planner )
| ( job_of(X_1457) = communications_consultant )
| ( job_of(X_1457) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_134720,plain,
! [X_1761: knowheyan] :
( ( c = X_1761 )
| ( job_of(X_1761) = lunar_energy_engineer )
| ( job_of(X_1761) = space_planner )
| ( job_of(X_1761) = communications_consultant )
| ( job_of(X_1761) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_102778,c_105074]) ).
tff(c_589,plain,
( ( job_of(d) != synthetic_food_nutitionist )
| ( job_of(b) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_95]) ).
tff(c_60701,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_589]) ).
tff(c_134759,plain,
( ( c = b )
| ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_134720,c_60701]) ).
tff(c_134825,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60711,c_117,c_198,c_10,c_134759]) ).
tff(c_134827,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_653]) ).
tff(c_50,plain,
! [X_7: age,Z_9: age,Y_8: age] :
( greater(X_7,Z_9)
| ~ greater(Y_8,Z_9)
| ~ greater(X_7,Y_8) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_136786,plain,
! [X_1842: age,Y_1843: knowheyan,X_1844: knowheyan] :
( greater(X_1842,age_of(Y_1843))
| ~ greater(X_1842,age_of(X_1844))
| ( job_of(Y_1843) != space_planner )
| ( job_of(X_1844) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_50]) ).
tff(c_136851,plain,
! [Y_1843: knowheyan] :
( greater(age_of(d),age_of(Y_1843))
| ( job_of(Y_1843) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_64,c_136786]) ).
tff(c_137057,plain,
! [Y_1852: knowheyan] :
( greater(age_of(d),age_of(Y_1852))
| ( job_of(Y_1852) != space_planner ) ),
inference(demodulation,[status(thm),theory(equality)],[c_134827,c_136851]) ).
tff(c_592,plain,
! [Y_113: knowheyan,X_112: knowheyan] :
( ~ greater(age_of(Y_113),age_of(X_112))
| ( job_of(Y_113) != synthetic_food_nutitionist )
| ( job_of(X_112) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_52]) ).
tff(c_137122,plain,
! [Y_1852: knowheyan] :
( ( job_of(d) != synthetic_food_nutitionist )
| ( job_of(Y_1852) != space_planner ) ),
inference(resolution,[status(thm)],[c_137057,c_592]) ).
tff(c_137138,plain,
job_of(d) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_137122]) ).
tff(c_137141,plain,
( ( job_of(d) = lunar_energy_engineer )
| ( job_of(d) = space_planner )
| ( job_of(d) = communications_consultant )
| ( job_of(d) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_137138]) ).
tff(c_137144,plain,
job_of(d) = lunar_energy_engineer,
inference(negUnitSimplification,[status(thm)],[c_27085,c_116,c_609,c_137141]) ).
tff(c_2,plain,
b != a,
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_76,plain,
( ( job_of(e) != synthetic_food_nutitionist )
| ( job_of(c) != space_planner )
| ( job_of(b) != airfoil_technician )
| ( job_of(d) != lunar_energy_engineer )
| ( job_of(a) != communications_consultant ) ),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_77,plain,
job_of(a) != communications_consultant,
inference(splitLeft,[status(thm)],[c_76]) ).
tff(c_134826,plain,
job_of(a) != space_planner,
inference(splitRight,[status(thm)],[c_653]) ).
tff(c_72,plain,
! [X_20: knowheyan,Y_21: knowheyan] :
( greater(age_of(X_20),age_of(Y_21))
| ( job_of(Y_21) != synthetic_food_nutitionist )
| ( job_of(X_20) != space_planner ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_663,plain,
! [Y_119: knowheyan,X_118: knowheyan] :
( ~ greater(age_of(Y_119),age_of(X_118))
| ( job_of(Y_119) != space_planner )
| ( job_of(X_118) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_52]) ).
tff(c_134939,plain,
! [Y_119: knowheyan] :
( ( job_of(Y_119) != space_planner )
| ( job_of(b) != airfoil_technician )
| ~ greater(age_of(Y_119),age_of(a)) ),
inference(resolution,[status(thm)],[c_134935,c_663]) ).
tff(c_135393,plain,
! [Y_1796: knowheyan] :
( ( job_of(Y_1796) != space_planner )
| ~ greater(age_of(Y_1796),age_of(a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_134827,c_134939]) ).
tff(c_135409,plain,
! [X_20: knowheyan] :
( ( job_of(a) != synthetic_food_nutitionist )
| ( job_of(X_20) != space_planner ) ),
inference(resolution,[status(thm)],[c_72,c_135393]) ).
tff(c_135412,plain,
job_of(a) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_135409]) ).
tff(c_135415,plain,
( ( job_of(a) = lunar_energy_engineer )
| ( job_of(a) = space_planner )
| ( job_of(a) = communications_consultant )
| ( job_of(a) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_135412]) ).
tff(c_135418,plain,
( ( job_of(a) = lunar_energy_engineer )
| ( job_of(a) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_77,c_134826,c_135415]) ).
tff(c_135419,plain,
job_of(a) = airfoil_technician,
inference(splitLeft,[status(thm)],[c_135418]) ).
tff(c_134905,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( b = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_134827,c_48]) ).
tff(c_135426,plain,
b = a,
inference(superposition,[status(thm),theory(equality)],[c_135419,c_134905]) ).
tff(c_135453,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_135426]) ).
tff(c_135454,plain,
job_of(a) = lunar_energy_engineer,
inference(splitRight,[status(thm)],[c_135418]) ).
tff(c_135546,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != lunar_energy_engineer )
| ( a = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_135454,c_48]) ).
tff(c_137163,plain,
d = a,
inference(superposition,[status(thm),theory(equality)],[c_137144,c_135546]) ).
tff(c_137197,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6,c_137163]) ).
tff(c_137199,plain,
job_of(d) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_137122]) ).
tff(c_136715,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_136718,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_136715]) ).
tff(c_136722,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_678,c_118,c_60702,c_196,c_136718]) ).
tff(c_136724,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_136758,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != synthetic_food_nutitionist )
| ( c = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_136724,c_48]) ).
tff(c_137218,plain,
d = c,
inference(superposition,[status(thm),theory(equality)],[c_137199,c_136758]) ).
tff(c_137251,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_137218]) ).
tff(c_137253,plain,
job_of(a) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_135409]) ).
tff(c_137252,plain,
! [X_20: knowheyan] : ( job_of(X_20) != space_planner ),
inference(splitRight,[status(thm)],[c_135409]) ).
tff(c_403,plain,
! [X_5: knowheyan,Y_6: knowheyan] :
( ( job_of(X_5) != synthetic_food_nutitionist )
| ( Y_6 = X_5 )
| ( job_of(Y_6) = lunar_energy_engineer )
| ( job_of(Y_6) = space_planner )
| ( job_of(Y_6) = communications_consultant )
| ( job_of(Y_6) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_141038,plain,
! [X_1950: knowheyan,Y_1951: knowheyan] :
( ( job_of(X_1950) != synthetic_food_nutitionist )
| ( Y_1951 = X_1950 )
| ( job_of(Y_1951) = lunar_energy_engineer )
| ( job_of(Y_1951) = communications_consultant )
| ( job_of(Y_1951) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_137252,c_403]) ).
tff(c_144992,plain,
! [Y_2011: knowheyan] :
( ( a = Y_2011 )
| ( job_of(Y_2011) = lunar_energy_engineer )
| ( job_of(Y_2011) = communications_consultant )
| ( job_of(Y_2011) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_137253,c_141038]) ).
tff(c_145031,plain,
( ( a = '#skF_1' )
| ( job_of('#skF_1') = communications_consultant )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_144992,c_340]) ).
tff(c_145074,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27080,c_115,c_142621,c_145031]) ).
tff(c_145076,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_590]) ).
tff(c_145325,plain,
! [X_2030: age] :
( ~ greater(age_of(c),X_2030)
| ~ greater(X_2030,age_of(b)) ),
inference(resolution,[status(thm)],[c_456,c_52]) ).
tff(c_145331,plain,
! [Y_21: knowheyan] :
( ~ greater(age_of(Y_21),age_of(b))
| ( job_of(Y_21) != synthetic_food_nutitionist )
| ( job_of(c) != space_planner ) ),
inference(resolution,[status(thm)],[c_72,c_145325]) ).
tff(c_145848,plain,
! [Y_2058: knowheyan] :
( ~ greater(age_of(Y_2058),age_of(b))
| ( job_of(Y_2058) != synthetic_food_nutitionist ) ),
inference(demodulation,[status(thm),theory(equality)],[c_145076,c_145331]) ).
tff(c_145885,plain,
job_of(d) != synthetic_food_nutitionist,
inference(resolution,[status(thm)],[c_64,c_145848]) ).
tff(c_145888,plain,
( ( job_of(d) = lunar_energy_engineer )
| ( job_of(d) = space_planner )
| ( job_of(d) = communications_consultant )
| ( job_of(d) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_145885]) ).
tff(c_145891,plain,
job_of(d) = lunar_energy_engineer,
inference(negUnitSimplification,[status(thm)],[c_27085,c_116,c_609,c_145888]) ).
tff(c_145075,plain,
job_of(b) != synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_590]) ).
tff(c_145083,plain,
( ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = space_planner )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_145075]) ).
tff(c_145086,plain,
job_of(b) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_117,c_60701,c_198,c_145083]) ).
tff(c_145160,plain,
! [Y_2017: knowheyan,X_2018: knowheyan] :
( ~ greater(age_of(Y_2017),age_of(X_2018))
| ( job_of(Y_2017) != space_planner )
| ( job_of(X_2018) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_610,c_52]) ).
tff(c_145166,plain,
( ( job_of(a) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_538,c_145160]) ).
tff(c_145205,plain,
job_of(a) != space_planner,
inference(demodulation,[status(thm),theory(equality)],[c_145086,c_145166]) ).
tff(c_145334,plain,
( ~ greater(age_of(d),age_of(b))
| ~ greater(age_of(c),age_of(a)) ),
inference(resolution,[status(thm)],[c_236,c_145325]) ).
tff(c_145356,plain,
~ greater(age_of(c),age_of(a)),
inference(demodulation,[status(thm),theory(equality)],[c_64,c_145334]) ).
tff(c_145368,plain,
( ( job_of(a) != synthetic_food_nutitionist )
| ( job_of(c) != space_planner ) ),
inference(resolution,[status(thm)],[c_72,c_145356]) ).
tff(c_145379,plain,
job_of(a) != synthetic_food_nutitionist,
inference(demodulation,[status(thm),theory(equality)],[c_145076,c_145368]) ).
tff(c_145418,plain,
( ( job_of(a) = lunar_energy_engineer )
| ( job_of(a) = space_planner )
| ( job_of(a) = communications_consultant )
| ( job_of(a) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_145379]) ).
tff(c_145421,plain,
( ( job_of(a) = lunar_energy_engineer )
| ( job_of(a) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_77,c_145205,c_145418]) ).
tff(c_145422,plain,
job_of(a) = airfoil_technician,
inference(splitLeft,[status(thm)],[c_145421]) ).
tff(c_145146,plain,
! [Y_6: knowheyan] :
( ( job_of(Y_6) != airfoil_technician )
| ( b = Y_6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_145086,c_48]) ).
tff(c_145432,plain,
b = a,
inference(superposition,[status(thm),theory(equality)],[c_145422,c_145146]) ).
tff(c_145463,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_145432]) ).
tff(c_145464,plain,
job_of(a) = lunar_energy_engineer,
inference(splitRight,[status(thm)],[c_145421]) ).
tff(c_145493,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != lunar_energy_engineer )
| ( a = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_145464,c_48]) ).
tff(c_145899,plain,
d = a,
inference(superposition,[status(thm),theory(equality)],[c_145891,c_145493]) ).
tff(c_145935,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6,c_145899]) ).
tff(c_145937,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_589]) ).
tff(c_154815,plain,
job_of('#skF_1') = space_planner,
inference(demodulation,[status(thm),theory(equality)],[c_154787,c_145937]) ).
tff(c_154834,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_673,c_154815]) ).
tff(c_154835,plain,
! [X_1: knowheyan] :
( ( c = '#skF_1' )
| ( X_1 = '#skF_1' )
| ( d = X_1 )
| ( c = X_1 )
| ( b = X_1 )
| ( a = X_1 ) ),
inference(splitRight,[status(thm)],[c_153792]) ).
tff(c_155980,plain,
c = '#skF_1',
inference(splitLeft,[status(thm)],[c_154835]) ).
tff(c_156008,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_155980,c_74]) ).
tff(c_156016,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_156008]) ).
tff(c_156018,plain,
c != '#skF_1',
inference(splitRight,[status(thm)],[c_154835]) ).
tff(c_147890,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_147893,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_147890]) ).
tff(c_147896,plain,
job_of(c) = space_planner,
inference(negUnitSimplification,[status(thm)],[c_678,c_118,c_196,c_147893]) ).
tff(c_145995,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( b = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_145937,c_48]) ).
tff(c_148019,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_147896,c_145995]) ).
tff(c_148050,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_148019]) ).
tff(c_148052,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_150474,plain,
! [X_2194: knowheyan,Y_2195: knowheyan] :
( ( job_of(X_2194) != synthetic_food_nutitionist )
| ( Y_2195 = X_2194 )
| ( job_of(Y_2195) = lunar_energy_engineer )
| ( job_of(Y_2195) = space_planner )
| ( job_of(Y_2195) = communications_consultant )
| ( job_of(Y_2195) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_184568,plain,
! [Y_2503: knowheyan] :
( ( c = Y_2503 )
| ( job_of(Y_2503) = lunar_energy_engineer )
| ( job_of(Y_2503) = space_planner )
| ( job_of(Y_2503) = communications_consultant )
| ( job_of(Y_2503) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_148052,c_150474]) ).
tff(c_184622,plain,
( ( c = '#skF_1' )
| ( job_of('#skF_1') = lunar_energy_engineer )
| ( job_of('#skF_1') = communications_consultant )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_184568,c_673]) ).
tff(c_184677,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27080,c_115,c_340,c_156018,c_184622]) ).
tff(c_184679,plain,
job_of(d) = airfoil_technician,
inference(splitRight,[status(thm)],[c_659]) ).
tff(c_184698,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( d = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_184679,c_48]) ).
tff(c_305072,plain,
d = b,
inference(superposition,[status(thm),theory(equality)],[c_305059,c_184698]) ).
tff(c_305098,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_305072]) ).
tff(c_305100,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_582]) ).
tff(c_314665,plain,
job_of('#skF_1') = space_planner,
inference(demodulation,[status(thm),theory(equality)],[c_314634,c_305100]) ).
tff(c_314684,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_673,c_314665]) ).
tff(c_314685,plain,
! [X_38: knowheyan] :
( ( c = '#skF_1' )
| ( X_38 = '#skF_1' )
| ( d = X_38 )
| ( c = X_38 )
| ( b = X_38 )
| ( a = X_38 ) ),
inference(splitRight,[status(thm)],[c_313967]) ).
tff(c_315325,plain,
c = '#skF_1',
inference(splitLeft,[status(thm)],[c_314685]) ).
tff(c_315354,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_315325,c_74]) ).
tff(c_315362,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_315354]) ).
tff(c_315364,plain,
c != '#skF_1',
inference(splitRight,[status(thm)],[c_314685]) ).
tff(c_307416,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_307419,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_307416]) ).
tff(c_307423,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_678,c_118,c_223798,c_196,c_307419]) ).
tff(c_307425,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_310655,plain,
! [X_3920: knowheyan,Y_3921: knowheyan] :
( ( job_of(X_3920) != synthetic_food_nutitionist )
| ( Y_3921 = X_3920 )
| ( job_of(Y_3921) = lunar_energy_engineer )
| ( job_of(Y_3921) = space_planner )
| ( job_of(Y_3921) = communications_consultant )
| ( job_of(Y_3921) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_346759,plain,
! [Y_4228: knowheyan] :
( ( c = Y_4228 )
| ( job_of(Y_4228) = lunar_energy_engineer )
| ( job_of(Y_4228) = space_planner )
| ( job_of(Y_4228) = communications_consultant )
| ( job_of(Y_4228) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_307425,c_310655]) ).
tff(c_346813,plain,
( ( c = '#skF_1' )
| ( job_of('#skF_1') = lunar_energy_engineer )
| ( job_of('#skF_1') = communications_consultant )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_346759,c_673]) ).
tff(c_346868,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27080,c_115,c_340,c_315364,c_346813]) ).
tff(c_346869,plain,
job_of(b) != synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_590]) ).
tff(c_346873,plain,
( ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = space_planner )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_346869]) ).
tff(c_346876,plain,
( ( job_of(b) = space_planner )
| ( job_of(b) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_117,c_198,c_346873]) ).
tff(c_346996,plain,
job_of(b) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_346991,c_346876]) ).
tff(c_347010,plain,
d = b,
inference(superposition,[status(thm),theory(equality)],[c_346996,c_184698]) ).
tff(c_347036,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_347010]) ).
tff(c_347038,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_582]) ).
tff(c_346870,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_590]) ).
tff(c_346958,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( c = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_346870,c_48]) ).
tff(c_347051,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_347038,c_346958]) ).
tff(c_347081,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_347051]) ).
tff(c_347082,plain,
job_of(c) != space_planner,
inference(splitRight,[status(thm)],[c_662]) ).
tff(c_385167,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_385170,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_385167]) ).
tff(c_385174,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_678,c_118,c_347082,c_196,c_385170]) ).
tff(c_385176,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_347083,plain,
job_of('#skF_1') = airfoil_technician,
inference(splitRight,[status(thm)],[c_662]) ).
tff(c_385372,plain,
! [X_4701: knowheyan] :
( greater(age_of(X_4701),age_of('#skF_1'))
| ( job_of(X_4701) != space_planner ) ),
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_385378,plain,
! [X_4701: knowheyan] :
( ( job_of('#skF_1') != airfoil_technician )
| ( job_of(X_4701) != space_planner ) ),
inference(resolution,[status(thm)],[c_385372,c_663]) ).
tff(c_385418,plain,
! [X_4701: knowheyan] : ( job_of(X_4701) != space_planner ),
inference(demodulation,[status(thm),theory(equality)],[c_347083,c_385378]) ).
tff(c_387889,plain,
! [X_4757: knowheyan,Y_4758: knowheyan] :
( ( job_of(X_4757) != synthetic_food_nutitionist )
| ( Y_4758 = X_4757 )
| ( job_of(Y_4758) = lunar_energy_engineer )
| ( job_of(Y_4758) = communications_consultant )
| ( job_of(Y_4758) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_385418,c_403]) ).
tff(c_387909,plain,
! [Y_4760: knowheyan] :
( ( c = Y_4760 )
| ( job_of(Y_4760) = lunar_energy_engineer )
| ( job_of(Y_4760) = communications_consultant )
| ( job_of(Y_4760) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_385176,c_387889]) ).
tff(c_387945,plain,
( ( c = b )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_387909,c_198]) ).
tff(c_387984,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_384227,c_117,c_10,c_387945]) ).
tff(c_387986,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_653]) ).
tff(c_384139,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( X_5 = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_347083,c_48]) ).
tff(c_388022,plain,
b = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_387986,c_384139]) ).
tff(c_388036,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_388022,c_328]) ).
tff(c_388050,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_388036]) ).
tff(c_388051,plain,
job_of(b) != space_planner,
inference(splitRight,[status(thm)],[c_661]) ).
tff(c_388052,plain,
job_of(c) = airfoil_technician,
inference(splitRight,[status(thm)],[c_661]) ).
tff(c_425032,plain,
! [Y_19: knowheyan] :
( ~ greater(age_of(Y_19),age_of(b))
| ( job_of(Y_19) != space_planner )
| ( job_of(c) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_70,c_425029]) ).
tff(c_425416,plain,
! [Y_5194: knowheyan] :
( ~ greater(age_of(Y_5194),age_of(b))
| ( job_of(Y_5194) != space_planner ) ),
inference(demodulation,[status(thm),theory(equality)],[c_388052,c_425032]) ).
tff(c_425446,plain,
! [X_20: knowheyan] :
( ( job_of(b) != synthetic_food_nutitionist )
| ( job_of(X_20) != space_planner ) ),
inference(resolution,[status(thm)],[c_72,c_425416]) ).
tff(c_425451,plain,
job_of(b) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_425446]) ).
tff(c_425462,plain,
( ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = space_planner )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_425451]) ).
tff(c_425466,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_424984,c_117,c_388051,c_198,c_425462]) ).
tff(c_425468,plain,
job_of(b) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_425446]) ).
tff(c_425467,plain,
! [X_20: knowheyan] : ( job_of(X_20) != space_planner ),
inference(splitRight,[status(thm)],[c_425446]) ).
tff(c_406,plain,
! [Y_6: knowheyan,X_5: knowheyan] :
( ( job_of(Y_6) != synthetic_food_nutitionist )
| ( Y_6 = X_5 )
| ( job_of(X_5) = lunar_energy_engineer )
| ( job_of(X_5) = space_planner )
| ( job_of(X_5) = communications_consultant )
| ( job_of(X_5) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_428878,plain,
! [Y_5279: knowheyan,X_5280: knowheyan] :
( ( job_of(Y_5279) != synthetic_food_nutitionist )
| ( Y_5279 = X_5280 )
| ( job_of(X_5280) = lunar_energy_engineer )
| ( job_of(X_5280) = communications_consultant )
| ( job_of(X_5280) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_425467,c_406]) ).
tff(c_433181,plain,
! [X_5348: knowheyan] :
( ( b = X_5348 )
| ( job_of(X_5348) = lunar_energy_engineer )
| ( job_of(X_5348) = communications_consultant )
| ( job_of(X_5348) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_425468,c_428878]) ).
tff(c_433214,plain,
( ( b = '#skF_1' )
| ( job_of('#skF_1') = communications_consultant )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_433181,c_340]) ).
tff(c_433251,plain,
job_of('#skF_1') = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_115,c_431964,c_433214]) ).
tff(c_388068,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( c = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_388052,c_48]) ).
tff(c_433441,plain,
c = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_433251,c_388068]) ).
tff(c_433464,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_432175,c_433441]) ).
tff(c_433466,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_653]) ).
tff(c_433483,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_433466,c_388068]) ).
tff(c_433506,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_433483]) ).
tff(c_433507,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_591]) ).
tff(c_433511,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_433507]) ).
tff(c_433514,plain,
( ( job_of(c) = space_planner )
| ( job_of(c) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_118,c_196,c_433511]) ).
tff(c_433943,plain,
job_of(c) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_433700,c_433514]) ).
tff(c_433705,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_653]) ).
tff(c_433676,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_589]) ).
tff(c_433508,plain,
job_of('#skF_1') = space_planner,
inference(splitRight,[status(thm)],[c_591]) ).
tff(c_342,plain,
~ greater(age_of('#skF_1'),age_of(b)),
inference(resolution,[status(thm)],[c_328,c_52]) ).
tff(c_583,plain,
( ( job_of(b) != synthetic_food_nutitionist )
| ( job_of('#skF_1') != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_342]) ).
tff(c_433821,plain,
job_of(b) != synthetic_food_nutitionist,
inference(demodulation,[status(thm),theory(equality)],[c_433508,c_583]) ).
tff(c_433824,plain,
( ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = space_planner )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_433821]) ).
tff(c_433828,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_433705,c_117,c_433676,c_198,c_433824]) ).
tff(c_433830,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_653]) ).
tff(c_433913,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( b = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_433830,c_48]) ).
tff(c_433951,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_433943,c_433913]) ).
tff(c_433981,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_433951]) ).
tff(c_433983,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_590]) ).
tff(c_433526,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( X_5 = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_433508,c_48]) ).
tff(c_434023,plain,
c = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_433983,c_433526]) ).
tff(c_434037,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_434023,c_74]) ).
tff(c_434045,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_434037]) ).
tff(c_434047,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_589]) ).
tff(c_434086,plain,
b = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_434047,c_433526]) ).
tff(c_434100,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_434086,c_328]) ).
tff(c_434114,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_434100]) ).
tff(c_434116,plain,
job_of(d) = space_planner,
inference(splitRight,[status(thm)],[c_588]) ).
tff(c_434117,plain,
! [X_5397: knowheyan,Y_5398: knowheyan] :
( greater(age_of(X_5397),age_of(Y_5398))
| ( job_of(Y_5398) != space_planner )
| ( job_of(X_5397) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_434167,plain,
( ( job_of(d) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_434117,c_95]) ).
tff(c_439218,plain,
job_of(b) != airfoil_technician,
inference(demodulation,[status(thm),theory(equality)],[c_434116,c_434167]) ).
tff(c_434168,plain,
( ( job_of(b) != space_planner )
| ( job_of(c) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_434117,c_96]) ).
tff(c_439074,plain,
job_of(c) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_434168]) ).
tff(c_439149,plain,
job_of(c) != space_planner,
inference(splitLeft,[status(thm)],[c_590]) ).
tff(c_441421,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_584]) ).
tff(c_441506,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_441421]) ).
tff(c_441510,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_439074,c_118,c_439149,c_196,c_441506]) ).
tff(c_441512,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_584]) ).
tff(c_443859,plain,
! [Y_5682: knowheyan,X_5683: knowheyan] :
( ( job_of(Y_5682) != synthetic_food_nutitionist )
| ( Y_5682 = X_5683 )
| ( job_of(X_5683) = lunar_energy_engineer )
| ( job_of(X_5683) = space_planner )
| ( job_of(X_5683) = communications_consultant )
| ( job_of(X_5683) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_367,c_48]) ).
tff(c_481508,plain,
! [X_6005: knowheyan] :
( ( c = X_6005 )
| ( job_of(X_6005) = lunar_energy_engineer )
| ( job_of(X_6005) = space_planner )
| ( job_of(X_6005) = communications_consultant )
| ( job_of(X_6005) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_441512,c_443859]) ).
tff(c_586,plain,
! [Y_113: knowheyan] :
( ( job_of(Y_113) != lunar_energy_engineer )
| ( job_of(Y_113) != synthetic_food_nutitionist )
| ( job_of(b) != space_planner ) ),
inference(resolution,[status(thm)],[c_539,c_197]) ).
tff(c_439975,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_586]) ).
tff(c_481529,plain,
( ( c = b )
| ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_481508,c_439975]) ).
tff(c_481606,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_439218,c_117,c_198,c_10,c_481529]) ).
tff(c_481608,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_586]) ).
tff(c_434185,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( d = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_434116,c_48]) ).
tff(c_481756,plain,
d = b,
inference(superposition,[status(thm),theory(equality)],[c_481608,c_434185]) ).
tff(c_481781,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_481756]) ).
tff(c_481783,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_590]) ).
tff(c_481808,plain,
d = c,
inference(superposition,[status(thm),theory(equality)],[c_481783,c_434185]) ).
tff(c_481832,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16,c_481808]) ).
tff(c_481834,plain,
job_of(c) = airfoil_technician,
inference(splitRight,[status(thm)],[c_434168]) ).
tff(c_238,plain,
! [X_35: age] :
( greater(X_35,age_of(c))
| ~ greater(X_35,age_of(b)) ),
inference(resolution,[status(thm)],[c_68,c_217]) ).
tff(c_482313,plain,
! [Y_6043: knowheyan,X_6044: knowheyan] :
( ~ greater(age_of(Y_6043),age_of(X_6044))
| ( job_of(Y_6043) != space_planner )
| ( job_of(X_6044) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_434117,c_52]) ).
tff(c_482334,plain,
! [Y_6043: knowheyan] :
( ( job_of(Y_6043) != space_planner )
| ( job_of(c) != airfoil_technician )
| ~ greater(age_of(Y_6043),age_of(b)) ),
inference(resolution,[status(thm)],[c_238,c_482313]) ).
tff(c_482447,plain,
! [Y_6050: knowheyan] :
( ( job_of(Y_6050) != space_planner )
| ~ greater(age_of(Y_6050),age_of(b)) ),
inference(demodulation,[status(thm),theory(equality)],[c_481834,c_482334]) ).
tff(c_482473,plain,
job_of(d) != space_planner,
inference(resolution,[status(thm)],[c_64,c_482447]) ).
tff(c_482485,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_434116,c_482473]) ).
tff(c_482486,plain,
( ( job_of(d) != lunar_energy_engineer )
| ( job_of(b) != airfoil_technician )
| ( job_of(c) != space_planner )
| ( job_of(e) != synthetic_food_nutitionist ) ),
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_482493,plain,
job_of(e) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_482486]) ).
tff(c_482744,plain,
( ( job_of(e) = lunar_energy_engineer )
| ( job_of(e) = space_planner )
| ( job_of(e) = communications_consultant )
| ( job_of(e) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_482672,c_482493]) ).
tff(c_483110,plain,
job_of(e) = airfoil_technician,
inference(splitLeft,[status(thm)],[c_482744]) ).
tff(c_483133,plain,
( ( job_of('#skF_1') = airfoil_technician )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_483132,c_483110]) ).
tff(c_483424,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_483133]) ).
tff(c_482645,plain,
! [X_6065: age] :
( greater(X_6065,age_of(d))
| ~ greater(X_6065,age_of(a)) ),
inference(resolution,[status(thm)],[c_62,c_482626]) ).
tff(c_482788,plain,
! [X_6119: age] :
( greater(X_6119,age_of(b))
| ~ greater(X_6119,age_of(d)) ),
inference(resolution,[status(thm)],[c_64,c_482626]) ).
tff(c_482994,plain,
! [X_6135: age] :
( greater(X_6135,age_of(b))
| ~ greater(X_6135,age_of(a)) ),
inference(resolution,[status(thm)],[c_482645,c_482788]) ).
tff(c_483021,plain,
~ greater(age_of(c),age_of(a)),
inference(resolution,[status(thm)],[c_482994,c_482520]) ).
tff(c_483426,plain,
~ greater(age_of(c),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_483424,c_483021]) ).
tff(c_483444,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_74,c_483426]) ).
tff(c_483446,plain,
a != '#skF_1',
inference(splitRight,[status(thm)],[c_483133]) ).
tff(c_483445,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(splitRight,[status(thm)],[c_483133]) ).
tff(c_530759,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(negUnitSimplification,[status(thm)],[c_528788,c_483445]) ).
tff(c_530760,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_530759]) ).
tff(c_530764,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_530760,c_483521]) ).
tff(c_530782,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_530764]) ).
tff(c_530783,plain,
( ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_530759]) ).
tff(c_530839,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_530783]) ).
tff(c_530850,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_530839,c_482979]) ).
tff(c_530871,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_530850]) ).
tff(c_530873,plain,
b != '#skF_1',
inference(splitRight,[status(thm)],[c_530783]) ).
tff(c_530784,plain,
d != '#skF_1',
inference(splitRight,[status(thm)],[c_530759]) ).
tff(c_482625,plain,
job_of('#skF_1') != communications_consultant,
inference(resolution,[status(thm)],[c_74,c_482597]) ).
tff(c_482831,plain,
! [X_6121: knowheyan] :
( ( e = X_6121 )
| ( d = X_6121 )
| ( c = X_6121 )
| ( b = X_6121 )
| ( a = X_6121 ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_482920,plain,
! [X_6127: knowheyan] :
( ( job_of(X_6127) != synthetic_food_nutitionist )
| ( d = X_6127 )
| ( c = X_6127 )
| ( b = X_6127 )
| ( a = X_6127 ) ),
inference(superposition,[status(thm),theory(equality)],[c_482831,c_482493]) ).
tff(c_483283,plain,
! [X_6154: knowheyan] :
( ( d = X_6154 )
| ( c = X_6154 )
| ( b = X_6154 )
| ( a = X_6154 )
| ( job_of(X_6154) = lunar_energy_engineer )
| ( job_of(X_6154) = space_planner )
| ( job_of(X_6154) = communications_consultant )
| ( job_of(X_6154) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_482920]) ).
tff(c_483266,plain,
job_of('#skF_1') != space_planner,
inference(splitLeft,[status(thm)],[c_483077]) ).
tff(c_483289,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' )
| ( job_of('#skF_1') = lunar_energy_engineer )
| ( job_of('#skF_1') = communications_consultant )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_483283,c_483266]) ).
tff(c_483356,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' )
| ( job_of('#skF_1') = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_482625,c_482919,c_483289]) ).
tff(c_530876,plain,
c = '#skF_1',
inference(negUnitSimplification,[status(thm)],[c_528788,c_483446,c_530873,c_530784,c_483356]) ).
tff(c_530892,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_530876,c_74]) ).
tff(c_530899,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_530892]) ).
tff(c_530901,plain,
job_of('#skF_1') = airfoil_technician,
inference(splitRight,[status(thm)],[c_528768]) ).
tff(c_483124,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( e = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_483110,c_48]) ).
tff(c_530963,plain,
e = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_530901,c_483124]) ).
tff(c_530977,plain,
c != '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_530963,c_18]) ).
tff(c_482647,plain,
! [X_6065: age] :
( greater(X_6065,age_of('#skF_1'))
| ~ greater(X_6065,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_482626]) ).
tff(c_483066,plain,
! [X_6137: knowheyan] :
( greater(age_of(X_6137),age_of('#skF_1'))
| ( job_of(c) != synthetic_food_nutitionist )
| ( job_of(X_6137) != space_planner ) ),
inference(resolution,[status(thm)],[c_483024,c_482647]) ).
tff(c_533283,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_483066]) ).
tff(c_533297,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_533283]) ).
tff(c_533303,plain,
job_of(c) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_482622,c_483181,c_482594,c_533297]) ).
tff(c_530948,plain,
! [Y_6: knowheyan] :
( ( job_of(Y_6) != airfoil_technician )
| ( Y_6 = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_530901,c_48]) ).
tff(c_533447,plain,
c = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_533303,c_530948]) ).
tff(c_533521,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_530977,c_533447]) ).
tff(c_533523,plain,
job_of(c) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_483066]) ).
tff(c_533806,plain,
! [X_6571: knowheyan] :
( greater(age_of(X_6571),age_of('#skF_1'))
| ( job_of(X_6571) != space_planner ) ),
inference(splitRight,[status(thm)],[c_483066]) ).
tff(c_483251,plain,
! [Y_6149: knowheyan,X_6148: knowheyan] :
( ~ greater(age_of(Y_6149),age_of(X_6148))
| ( job_of(Y_6149) != space_planner )
| ( job_of(X_6148) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_483186,c_52]) ).
tff(c_533829,plain,
! [X_6571: knowheyan] :
( ( job_of('#skF_1') != airfoil_technician )
| ( job_of(X_6571) != space_planner ) ),
inference(resolution,[status(thm)],[c_533806,c_483251]) ).
tff(c_533874,plain,
! [X_6571: knowheyan] : ( job_of(X_6571) != space_planner ),
inference(demodulation,[status(thm),theory(equality)],[c_530901,c_533829]) ).
tff(c_482705,plain,
! [X_5: knowheyan,Y_6: knowheyan] :
( ( job_of(X_5) != synthetic_food_nutitionist )
| ( Y_6 = X_5 )
| ( job_of(Y_6) = lunar_energy_engineer )
| ( job_of(Y_6) = space_planner )
| ( job_of(Y_6) = communications_consultant )
| ( job_of(Y_6) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_482672,c_48]) ).
tff(c_538752,plain,
! [X_6635: knowheyan,Y_6636: knowheyan] :
( ( job_of(X_6635) != synthetic_food_nutitionist )
| ( Y_6636 = X_6635 )
| ( job_of(Y_6636) = lunar_energy_engineer )
| ( job_of(Y_6636) = communications_consultant )
| ( job_of(Y_6636) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_533874,c_482705]) ).
tff(c_541285,plain,
! [Y_6646: knowheyan] :
( ( c = Y_6646 )
| ( job_of(Y_6646) = lunar_energy_engineer )
| ( job_of(Y_6646) = communications_consultant )
| ( job_of(Y_6646) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_533523,c_538752]) ).
tff(c_482596,plain,
job_of(b) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_482584,c_58]) ).
tff(c_541335,plain,
( ( c = b )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_541285,c_482596]) ).
tff(c_541396,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_483393,c_482624,c_10,c_541335]) ).
tff(c_541398,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_483248]) ).
tff(c_541422,plain,
e = b,
inference(superposition,[status(thm),theory(equality)],[c_541398,c_483124]) ).
tff(c_541454,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_541422]) ).
tff(c_541455,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_483077]) ).
tff(c_541459,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_541455]) ).
tff(c_541462,plain,
job_of(c) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_482622,c_483181,c_482594,c_541459]) ).
tff(c_541513,plain,
e = c,
inference(superposition,[status(thm),theory(equality)],[c_541462,c_483124]) ).
tff(c_541539,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_541513]) ).
tff(c_541541,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_483078]) ).
tff(c_541724,plain,
! [X_6660: knowheyan,Y_6661: knowheyan] :
( greater(age_of(X_6660),age_of(Y_6661))
| ( job_of(Y_6661) != space_planner )
| ( job_of(X_6660) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_541762,plain,
( ( job_of(c) != space_planner )
| ( job_of('#skF_1') != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_541724,c_482523]) ).
tff(c_541791,plain,
job_of('#skF_1') != airfoil_technician,
inference(demodulation,[status(thm),theory(equality)],[c_541541,c_541762]) ).
tff(c_541827,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(negUnitSimplification,[status(thm)],[c_541791,c_483133]) ).
tff(c_541828,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_541827]) ).
tff(c_541830,plain,
~ greater(age_of(c),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_541828,c_483021]) ).
tff(c_541848,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_74,c_541830]) ).
tff(c_541849,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_541827]) ).
tff(c_541860,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_541849]) ).
tff(c_541869,plain,
~ greater(age_of(b),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_541860,c_482522]) ).
tff(c_541878,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_482979,c_541869]) ).
tff(c_541879,plain,
( ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_541849]) ).
tff(c_541881,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_541879]) ).
tff(c_542007,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_541881,c_482979]) ).
tff(c_542028,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_542007]) ).
tff(c_542029,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_541879]) ).
tff(c_542042,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_542029,c_74]) ).
tff(c_542049,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_542042]) ).
tff(c_542050,plain,
( ( job_of(e) = communications_consultant )
| ( job_of(e) = space_planner )
| ( job_of(e) = lunar_energy_engineer ) ),
inference(splitRight,[status(thm)],[c_482744]) ).
tff(c_544451,plain,
job_of(e) = lunar_energy_engineer,
inference(splitLeft,[status(thm)],[c_542050]) ).
tff(c_544475,plain,
( ( job_of('#skF_1') = lunar_energy_engineer )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_544474,c_544451]) ).
tff(c_544496,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(negUnitSimplification,[status(thm)],[c_482919,c_544475]) ).
tff(c_545092,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_544496]) ).
tff(c_482806,plain,
greater(age_of(a),age_of(b)),
inference(resolution,[status(thm)],[c_62,c_482788]) ).
tff(c_544890,plain,
! [X_6808: age] :
( greater(X_6808,age_of('#skF_1'))
| ~ greater(X_6808,age_of(b)) ),
inference(resolution,[status(thm)],[c_482644,c_482961]) ).
tff(c_544918,plain,
greater(age_of(a),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_482806,c_544890]) ).
tff(c_545094,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_545092,c_544918]) ).
tff(c_545113,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_545094]) ).
tff(c_545114,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_544496]) ).
tff(c_545116,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_545114]) ).
tff(c_544922,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_544890]) ).
tff(c_545119,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_545116,c_544922]) ).
tff(c_545136,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_545119]) ).
tff(c_545137,plain,
( ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_545114]) ).
tff(c_545139,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_545137]) ).
tff(c_542137,plain,
job_of('#skF_1') != space_planner,
inference(splitLeft,[status(thm)],[c_483077]) ).
tff(c_542991,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_542164,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_542138,plain,
job_of(e) = lunar_energy_engineer,
inference(splitLeft,[status(thm)],[c_542050]) ).
tff(c_542165,plain,
( ( job_of('#skF_1') = lunar_energy_engineer )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_542164,c_542138]) ).
tff(c_542187,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(negUnitSimplification,[status(thm)],[c_482919,c_542165]) ).
tff(c_542474,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_542187]) ).
tff(c_542358,plain,
! [X_6690: age] :
( greater(X_6690,age_of('#skF_1'))
| ~ greater(X_6690,age_of(b)) ),
inference(resolution,[status(thm)],[c_482644,c_482961]) ).
tff(c_542380,plain,
greater(age_of(a),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_482806,c_542358]) ).
tff(c_542529,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_542474,c_542380]) ).
tff(c_542547,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_542529]) ).
tff(c_542548,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_542187]) ).
tff(c_542550,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_542548]) ).
tff(c_542384,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_542358]) ).
tff(c_542651,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_542550,c_542384]) ).
tff(c_542666,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_542651]) ).
tff(c_542667,plain,
( ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_542548]) ).
tff(c_542669,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_542667]) ).
tff(c_542673,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_542669,c_482979]) ).
tff(c_542694,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_542673]) ).
tff(c_542695,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_542667]) ).
tff(c_542761,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_542695,c_74]) ).
tff(c_542768,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_542761]) ).
tff(c_542769,plain,
( ( job_of(e) = space_planner )
| ( job_of(e) = communications_consultant ) ),
inference(splitRight,[status(thm)],[c_542050]) ).
tff(c_542889,plain,
job_of(e) = communications_consultant,
inference(splitLeft,[status(thm)],[c_542769]) ).
tff(c_482487,plain,
job_of(a) = communications_consultant,
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_482498,plain,
! [Y_6053: knowheyan,X_6054: knowheyan] :
( ( job_of(Y_6053) != job_of(X_6054) )
| ( Y_6053 = X_6054 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_482501,plain,
! [X_6054: knowheyan] :
( ( job_of(X_6054) != communications_consultant )
| ( a = X_6054 ) ),
inference(superposition,[status(thm),theory(equality)],[c_482487,c_482498]) ).
tff(c_542908,plain,
e = a,
inference(superposition,[status(thm),theory(equality)],[c_542889,c_482501]) ).
tff(c_542946,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8,c_542908]) ).
tff(c_542947,plain,
job_of(e) = space_planner,
inference(splitRight,[status(thm)],[c_542769]) ).
tff(c_542992,plain,
( ( job_of('#skF_1') = space_planner )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_542991,c_542947]) ).
tff(c_543022,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(negUnitSimplification,[status(thm)],[c_542137,c_542992]) ).
tff(c_543435,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_543022]) ).
tff(c_543242,plain,
! [X_6730: age] :
( greater(X_6730,age_of('#skF_1'))
| ~ greater(X_6730,age_of(b)) ),
inference(resolution,[status(thm)],[c_482644,c_482961]) ).
tff(c_543269,plain,
greater(age_of(a),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_482806,c_543242]) ).
tff(c_543438,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_543435,c_543269]) ).
tff(c_543457,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_543438]) ).
tff(c_543458,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_543022]) ).
tff(c_543460,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_543458]) ).
tff(c_543273,plain,
greater(age_of(d),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_64,c_543242]) ).
tff(c_543464,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_543460,c_543273]) ).
tff(c_543480,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_543464]) ).
tff(c_543481,plain,
( ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_543458]) ).
tff(c_543483,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_543481]) ).
tff(c_543490,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_543483,c_482979]) ).
tff(c_543511,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_543490]) ).
tff(c_543512,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_543481]) ).
tff(c_543529,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_543512,c_74]) ).
tff(c_543536,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_543529]) ).
tff(c_543537,plain,
job_of(c) != synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_483077]) ).
tff(c_543541,plain,
( ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = space_planner )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_543537]) ).
tff(c_543544,plain,
( ( job_of(c) = space_planner )
| ( job_of(c) = airfoil_technician ) ),
inference(negUnitSimplification,[status(thm)],[c_482622,c_482594,c_543541]) ).
tff(c_544259,plain,
job_of(c) = airfoil_technician,
inference(splitLeft,[status(thm)],[c_543544]) ).
tff(c_542058,plain,
! [X_6673: knowheyan,Y_6674: knowheyan] :
( greater(age_of(X_6673),age_of(Y_6674))
| ( job_of(Y_6674) != space_planner )
| ( job_of(X_6673) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_542120,plain,
( ( job_of(d) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_542058,c_482522]) ).
tff(c_543697,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_542120]) ).
tff(c_483076,plain,
( ( job_of(d) != synthetic_food_nutitionist )
| ( job_of(b) != space_planner ) ),
inference(resolution,[status(thm)],[c_483024,c_482522]) ).
tff(c_542057,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_483076]) ).
tff(c_543538,plain,
job_of('#skF_1') = space_planner,
inference(splitRight,[status(thm)],[c_483077]) ).
tff(c_483068,plain,
( ( job_of(b) != synthetic_food_nutitionist )
| ( job_of('#skF_1') != space_planner ) ),
inference(resolution,[status(thm)],[c_483024,c_482911]) ).
tff(c_544014,plain,
job_of(b) != synthetic_food_nutitionist,
inference(demodulation,[status(thm),theory(equality)],[c_543538,c_483068]) ).
tff(c_544020,plain,
( ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = space_planner )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_544014]) ).
tff(c_544025,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_543697,c_482624,c_542057,c_482596,c_544020]) ).
tff(c_544027,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_542120]) ).
tff(c_544059,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( b = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_544027,c_48]) ).
tff(c_544315,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_544259,c_544059]) ).
tff(c_544358,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_544315]) ).
tff(c_544359,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_543544]) ).
tff(c_543562,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( X_5 = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_543538,c_48]) ).
tff(c_544417,plain,
c = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_544359,c_543562]) ).
tff(c_544440,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_544417,c_74]) ).
tff(c_544448,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_544440]) ).
tff(c_544450,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_483076]) ).
tff(c_545144,plain,
job_of('#skF_1') = space_planner,
inference(demodulation,[status(thm),theory(equality)],[c_545139,c_544450]) ).
tff(c_545165,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_544796,c_545144]) ).
tff(c_545166,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_545137]) ).
tff(c_545294,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_545166,c_74]) ).
tff(c_545301,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_545294]) ).
tff(c_545303,plain,
job_of('#skF_1') = space_planner,
inference(splitRight,[status(thm)],[c_483077]) ).
tff(c_544526,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( b = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_544450,c_48]) ).
tff(c_545358,plain,
b = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_545303,c_544526]) ).
tff(c_545371,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_545358,c_482979]) ).
tff(c_545391,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_545371]) ).
tff(c_545392,plain,
( ( job_of(e) = space_planner )
| ( job_of(e) = communications_consultant ) ),
inference(splitRight,[status(thm)],[c_542050]) ).
tff(c_545636,plain,
job_of(e) = communications_consultant,
inference(splitLeft,[status(thm)],[c_545392]) ).
tff(c_545658,plain,
e = a,
inference(superposition,[status(thm),theory(equality)],[c_545636,c_482501]) ).
tff(c_545697,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8,c_545658]) ).
tff(c_545698,plain,
job_of(e) = space_planner,
inference(splitRight,[status(thm)],[c_545392]) ).
tff(c_545480,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( b = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_544450,c_48]) ).
tff(c_545719,plain,
e = b,
inference(superposition,[status(thm),theory(equality)],[c_545698,c_545480]) ).
tff(c_545766,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14,c_545719]) ).
tff(c_545768,plain,
job_of(e) = synthetic_food_nutitionist,
inference(splitRight,[status(thm)],[c_482486]) ).
tff(c_547928,plain,
( ( job_of('#skF_1') = synthetic_food_nutitionist )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_547927,c_545768]) ).
tff(c_548021,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_547928]) ).
tff(c_548028,plain,
job_of('#skF_1') = communications_consultant,
inference(demodulation,[status(thm),theory(equality)],[c_548021,c_482487]) ).
tff(c_548034,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_547838,c_548028]) ).
tff(c_548035,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' )
| ( job_of('#skF_1') = synthetic_food_nutitionist ) ),
inference(splitRight,[status(thm)],[c_547928]) ).
tff(c_548234,plain,
job_of('#skF_1') = synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_548035]) ).
tff(c_545777,plain,
! [Y_6839: knowheyan,X_6840: knowheyan] :
( ( job_of(Y_6839) != job_of(X_6840) )
| ( Y_6839 = X_6840 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_545783,plain,
! [Y_6839: knowheyan] :
( ( job_of(Y_6839) != synthetic_food_nutitionist )
| ( e = Y_6839 ) ),
inference(superposition,[status(thm),theory(equality)],[c_545768,c_545777]) ).
tff(c_548262,plain,
e = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_548234,c_545783]) ).
tff(c_548271,plain,
b != '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_548262,c_14]) ).
tff(c_548090,plain,
! [X_7003: job] :
( ( synthetic_food_nutitionist = X_7003 )
| ( lunar_energy_engineer = X_7003 )
| ( space_planner = X_7003 )
| ( communications_consultant = X_7003 )
| ( airfoil_technician = X_7003 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_548185,plain,
! [Y_6839: knowheyan] :
( ( e = Y_6839 )
| ( job_of(Y_6839) = lunar_energy_engineer )
| ( job_of(Y_6839) = space_planner )
| ( job_of(Y_6839) = communications_consultant )
| ( job_of(Y_6839) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_548090,c_545783]) ).
tff(c_548359,plain,
! [Y_6839: knowheyan] :
( ( Y_6839 = '#skF_1' )
| ( job_of(Y_6839) = lunar_energy_engineer )
| ( job_of(Y_6839) = space_planner )
| ( job_of(Y_6839) = communications_consultant )
| ( job_of(Y_6839) = airfoil_technician ) ),
inference(demodulation,[status(thm),theory(equality)],[c_548262,c_548185]) ).
tff(c_547834,plain,
job_of(c) != communications_consultant,
inference(resolution,[status(thm)],[c_68,c_547809]) ).
tff(c_545810,plain,
! [Y_6843: age,X_6844: age] :
( ~ greater(Y_6843,X_6844)
| ~ greater(X_6844,Y_6843) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_545819,plain,
~ greater(age_of(c),age_of(b)),
inference(resolution,[status(thm)],[c_68,c_545810]) ).
tff(c_547806,plain,
job_of(c) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_547796,c_545819]) ).
tff(c_548273,plain,
c != '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_548262,c_18]) ).
tff(c_548372,plain,
! [Y_7076: knowheyan] :
( ( Y_7076 = '#skF_1' )
| ( job_of(Y_7076) = lunar_energy_engineer )
| ( job_of(Y_7076) = space_planner )
| ( job_of(Y_7076) = communications_consultant )
| ( job_of(Y_7076) = airfoil_technician ) ),
inference(demodulation,[status(thm),theory(equality)],[c_548262,c_548185]) ).
tff(c_545926,plain,
! [X_6852: age,Z_6853: age,Y_6854: age] :
( greater(X_6852,Z_6853)
| ~ greater(Y_6854,Z_6853)
| ~ greater(X_6852,Y_6854) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_546184,plain,
! [X_6860: age] :
( greater(X_6860,age_of('#skF_1'))
| ~ greater(X_6860,age_of(c)) ),
inference(resolution,[status(thm)],[c_74,c_545926]) ).
tff(c_546202,plain,
greater(age_of(b),age_of('#skF_1')),
inference(resolution,[status(thm)],[c_68,c_546184]) ).
tff(c_545884,plain,
! [Y_6849: knowheyan,X_6850: knowheyan] :
( ~ greater(age_of(Y_6849),age_of(X_6850))
| ( job_of(X_6850) != communications_consultant ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_545907,plain,
job_of(b) != communications_consultant,
inference(resolution,[status(thm)],[c_64,c_545884]) ).
tff(c_545909,plain,
! [X_6851: knowheyan] :
( greater(age_of(X_6851),age_of(b))
| ( job_of(X_6851) != lunar_energy_engineer ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_545925,plain,
job_of(b) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_545909,c_58]) ).
tff(c_545908,plain,
job_of('#skF_1') != communications_consultant,
inference(resolution,[status(thm)],[c_74,c_545884]) ).
tff(c_546028,plain,
( ( e = '#skF_1' )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_546029,plain,
( ( job_of('#skF_1') = synthetic_food_nutitionist )
| ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' )
| ( a = '#skF_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_546028,c_545768]) ).
tff(c_546161,plain,
a = '#skF_1',
inference(splitLeft,[status(thm)],[c_546029]) ).
tff(c_546169,plain,
job_of('#skF_1') = communications_consultant,
inference(demodulation,[status(thm),theory(equality)],[c_546161,c_482487]) ).
tff(c_546175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_545908,c_546169]) ).
tff(c_546176,plain,
( ( b = '#skF_1' )
| ( c = '#skF_1' )
| ( d = '#skF_1' )
| ( job_of('#skF_1') = synthetic_food_nutitionist ) ),
inference(splitRight,[status(thm)],[c_546029]) ).
tff(c_546380,plain,
job_of('#skF_1') = synthetic_food_nutitionist,
inference(splitLeft,[status(thm)],[c_546176]) ).
tff(c_546405,plain,
e = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_546380,c_545783]) ).
tff(c_546414,plain,
b != '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_546405,c_14]) ).
tff(c_546227,plain,
! [X_6861: job] :
( ( synthetic_food_nutitionist = X_6861 )
| ( lunar_energy_engineer = X_6861 )
| ( space_planner = X_6861 )
| ( communications_consultant = X_6861 )
| ( airfoil_technician = X_6861 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_546318,plain,
! [Y_6839: knowheyan] :
( ( e = Y_6839 )
| ( job_of(Y_6839) = lunar_energy_engineer )
| ( job_of(Y_6839) = space_planner )
| ( job_of(Y_6839) = communications_consultant )
| ( job_of(Y_6839) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_546227,c_545783]) ).
tff(c_546505,plain,
! [Y_6839: knowheyan] :
( ( Y_6839 = '#skF_1' )
| ( job_of(Y_6839) = lunar_energy_engineer )
| ( job_of(Y_6839) = space_planner )
| ( job_of(Y_6839) = communications_consultant )
| ( job_of(Y_6839) = airfoil_technician ) ),
inference(demodulation,[status(thm),theory(equality)],[c_546405,c_546318]) ).
tff(c_545906,plain,
job_of(d) != communications_consultant,
inference(resolution,[status(thm)],[c_62,c_545884]) ).
tff(c_545767,plain,
( ( job_of(c) != space_planner )
| ( job_of(b) != airfoil_technician )
| ( job_of(d) != lunar_energy_engineer ) ),
inference(splitRight,[status(thm)],[c_482486]) ).
tff(c_545828,plain,
job_of(d) != lunar_energy_engineer,
inference(splitLeft,[status(thm)],[c_545767]) ).
tff(c_20,plain,
e != d,
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_546415,plain,
d != '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_546405,c_20]) ).
tff(c_546423,plain,
! [X_6931: knowheyan,Y_6932: knowheyan] :
( greater(age_of(X_6931),age_of(Y_6932))
| ( job_of(Y_6932) != space_planner )
| ( job_of(X_6931) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_546488,plain,
( ( job_of(b) != space_planner )
| ( job_of(c) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_546423,c_545819]) ).
tff(c_546605,plain,
job_of(c) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_546488]) ).
tff(c_545905,plain,
job_of(c) != communications_consultant,
inference(resolution,[status(thm)],[c_68,c_545884]) ).
tff(c_546416,plain,
c != '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_546405,c_18]) ).
tff(c_545821,plain,
~ greater(age_of(b),age_of(d)),
inference(resolution,[status(thm)],[c_64,c_545810]) ).
tff(c_546483,plain,
( ( job_of(d) != space_planner )
| ( job_of(b) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_546423,c_545821]) ).
tff(c_546614,plain,
job_of(b) != airfoil_technician,
inference(splitLeft,[status(thm)],[c_546483]) ).
tff(c_546623,plain,
! [X_6942: knowheyan,Y_6943: knowheyan] :
( greater(age_of(X_6942),age_of(Y_6943))
| ( job_of(Y_6943) != synthetic_food_nutitionist )
| ( job_of(X_6942) != space_planner ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_546683,plain,
( ( job_of(d) != synthetic_food_nutitionist )
| ( job_of(b) != space_planner ) ),
inference(resolution,[status(thm)],[c_546623,c_545821]) ).
tff(c_546708,plain,
job_of(b) != space_planner,
inference(splitLeft,[status(thm)],[c_546683]) ).
tff(c_546711,plain,
( ( b = '#skF_1' )
| ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_546505,c_546708]) ).
tff(c_546718,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_546614,c_545907,c_545925,c_546414,c_546711]) ).
tff(c_546720,plain,
job_of(b) = space_planner,
inference(splitRight,[status(thm)],[c_546683]) ).
tff(c_546779,plain,
! [X_6950: knowheyan] :
( ( job_of(X_6950) != space_planner )
| ( b = X_6950 ) ),
inference(superposition,[status(thm),theory(equality)],[c_546720,c_48]) ).
tff(c_547076,plain,
! [Y_6967: knowheyan] :
( ( b = Y_6967 )
| ( Y_6967 = '#skF_1' )
| ( job_of(Y_6967) = lunar_energy_engineer )
| ( job_of(Y_6967) = communications_consultant )
| ( job_of(Y_6967) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_546505,c_546779]) ).
tff(c_545923,plain,
job_of(c) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_545909,c_545819]) ).
tff(c_547118,plain,
( ( c = b )
| ( c = '#skF_1' )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_547076,c_545923]) ).
tff(c_547169,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_546605,c_545905,c_546416,c_10,c_547118]) ).
tff(c_547170,plain,
job_of(d) != space_planner,
inference(splitRight,[status(thm)],[c_546483]) ).
tff(c_547174,plain,
( ( d = '#skF_1' )
| ( job_of(d) = lunar_energy_engineer )
| ( job_of(d) = communications_consultant )
| ( job_of(d) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_546505,c_547170]) ).
tff(c_547180,plain,
job_of(d) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_545906,c_545828,c_546415,c_547174]) ).
tff(c_547171,plain,
job_of(b) = airfoil_technician,
inference(splitRight,[status(thm)],[c_546483]) ).
tff(c_547263,plain,
! [X_6972: knowheyan] :
( ( job_of(X_6972) != airfoil_technician )
| ( b = X_6972 ) ),
inference(superposition,[status(thm),theory(equality)],[c_547171,c_48]) ).
tff(c_547266,plain,
d = b,
inference(superposition,[status(thm),theory(equality)],[c_547180,c_547263]) ).
tff(c_547285,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12,c_547266]) ).
tff(c_547286,plain,
job_of(b) != space_planner,
inference(splitRight,[status(thm)],[c_546488]) ).
tff(c_547290,plain,
( ( b = '#skF_1' )
| ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_546505,c_547286]) ).
tff(c_547296,plain,
job_of(b) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_545907,c_545925,c_546414,c_547290]) ).
tff(c_547287,plain,
job_of(c) = airfoil_technician,
inference(splitRight,[status(thm)],[c_546488]) ).
tff(c_547447,plain,
! [X_6980: knowheyan] :
( ( job_of(X_6980) != airfoil_technician )
| ( c = X_6980 ) ),
inference(superposition,[status(thm),theory(equality)],[c_547287,c_48]) ).
tff(c_547450,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_547296,c_547447]) ).
tff(c_547469,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_547450]) ).
tff(c_547470,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_546176]) ).
tff(c_547578,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_547470]) ).
tff(c_547580,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_547578,c_546202]) ).
tff(c_547600,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_547580]) ).
tff(c_547601,plain,
( ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_547470]) ).
tff(c_547603,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_547601]) ).
tff(c_547675,plain,
~ greater(age_of(b),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_547603,c_545821]) ).
tff(c_547685,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_546202,c_547675]) ).
tff(c_547686,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_547601]) ).
tff(c_547698,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_547686,c_74]) ).
tff(c_547705,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_547698]) ).
tff(c_547706,plain,
( ( job_of(b) != airfoil_technician )
| ( job_of(c) != space_planner ) ),
inference(splitRight,[status(thm)],[c_545767]) ).
tff(c_547740,plain,
job_of(c) != space_planner,
inference(splitLeft,[status(thm)],[c_547706]) ).
tff(c_548396,plain,
( ( c = '#skF_1' )
| ( job_of(c) = lunar_energy_engineer )
| ( job_of(c) = communications_consultant )
| ( job_of(c) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_548372,c_547740]) ).
tff(c_548440,plain,
job_of(c) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_547834,c_547806,c_548273,c_548396]) ).
tff(c_548280,plain,
! [X_7071: knowheyan,Y_7072: knowheyan] :
( greater(age_of(X_7071),age_of(Y_7072))
| ( job_of(Y_7072) != space_planner )
| ( job_of(X_7071) != airfoil_technician ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_548338,plain,
( ( job_of(b) != space_planner )
| ( job_of(c) != airfoil_technician ) ),
inference(resolution,[status(thm)],[c_548280,c_545819]) ).
tff(c_548544,plain,
job_of(b) != space_planner,
inference(demodulation,[status(thm),theory(equality)],[c_548440,c_548338]) ).
tff(c_548547,plain,
( ( b = '#skF_1' )
| ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_548359,c_548544]) ).
tff(c_548553,plain,
job_of(b) = airfoil_technician,
inference(negUnitSimplification,[status(thm)],[c_547837,c_547808,c_548271,c_548547]) ).
tff(c_548472,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != airfoil_technician )
| ( c = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_548440,c_48]) ).
tff(c_548627,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_548553,c_548472]) ).
tff(c_548659,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_548627]) ).
tff(c_548660,plain,
( ( d = '#skF_1' )
| ( c = '#skF_1' )
| ( b = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_548035]) ).
tff(c_548668,plain,
b = '#skF_1',
inference(splitLeft,[status(thm)],[c_548660]) ).
tff(c_548783,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_548668,c_548051]) ).
tff(c_548799,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_548783]) ).
tff(c_548800,plain,
( ( c = '#skF_1' )
| ( d = '#skF_1' ) ),
inference(splitRight,[status(thm)],[c_548660]) ).
tff(c_548802,plain,
d = '#skF_1',
inference(splitLeft,[status(thm)],[c_548800]) ).
tff(c_547707,plain,
job_of(d) = lunar_energy_engineer,
inference(splitRight,[status(thm)],[c_545767]) ).
tff(c_548807,plain,
job_of('#skF_1') = lunar_energy_engineer,
inference(demodulation,[status(thm),theory(equality)],[c_548802,c_547707]) ).
tff(c_548817,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_548062,c_548807]) ).
tff(c_548818,plain,
c = '#skF_1',
inference(splitRight,[status(thm)],[c_548800]) ).
tff(c_548887,plain,
greater(age_of('#skF_1'),age_of('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_548818,c_74]) ).
tff(c_548894,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58,c_548887]) ).
tff(c_548895,plain,
job_of(b) != airfoil_technician,
inference(splitRight,[status(thm)],[c_547706]) ).
tff(c_548992,plain,
! [Y_7099: knowheyan,X_7100: knowheyan] :
( ~ greater(age_of(Y_7099),age_of(X_7100))
| ( job_of(X_7100) != communications_consultant ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_549017,plain,
job_of(b) != communications_consultant,
inference(resolution,[status(thm)],[c_64,c_548992]) ).
tff(c_549019,plain,
! [X_7101: knowheyan] :
( greater(age_of(X_7101),age_of(b))
| ( job_of(X_7101) != lunar_energy_engineer ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_549036,plain,
job_of(b) != lunar_energy_engineer,
inference(resolution,[status(thm)],[c_549019,c_58]) ).
tff(c_548896,plain,
job_of(c) = space_planner,
inference(splitRight,[status(thm)],[c_547706]) ).
tff(c_549633,plain,
! [X_7187: knowheyan,Y_7188: knowheyan] :
( greater(age_of(X_7187),age_of(Y_7188))
| ( job_of(Y_7188) != synthetic_food_nutitionist )
| ( job_of(X_7187) != space_planner ) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_549672,plain,
( ( job_of(b) != synthetic_food_nutitionist )
| ( job_of(c) != space_planner ) ),
inference(resolution,[status(thm)],[c_549633,c_545819]) ).
tff(c_549699,plain,
job_of(b) != synthetic_food_nutitionist,
inference(demodulation,[status(thm),theory(equality)],[c_548896,c_549672]) ).
tff(c_549704,plain,
( ( job_of(b) = lunar_energy_engineer )
| ( job_of(b) = space_planner )
| ( job_of(b) = communications_consultant )
| ( job_of(b) = airfoil_technician ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_549699]) ).
tff(c_549707,plain,
job_of(b) = space_planner,
inference(negUnitSimplification,[status(thm)],[c_548895,c_549017,c_549036,c_549704]) ).
tff(c_548909,plain,
! [X_5: knowheyan] :
( ( job_of(X_5) != space_planner )
| ( c = X_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_548896,c_48]) ).
tff(c_549715,plain,
c = b,
inference(superposition,[status(thm),theory(equality)],[c_549707,c_548909]) ).
tff(c_549736,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_549715]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : PUZ134_1 : TPTP v9.0.0. Released v5.1.0.
% 0.06/0.13 % 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.13/0.34 % Computer : n002.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 17:31:02 EDT 2025
% 0.13/0.34 % CPUTime :
% 40.59/25.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 40.72/25.98
% 40.72/25.98 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------