%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ134_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:31:41 PM UTC 2026
% Result : Theorem 3.43s 1.71s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 67
% Syntax : Number of formulae : 476 ( 84 unt; 0 typ; 38 def)
% Number of atoms : 1602 ( 671 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1716 ( 590 ~;1065 |; 16 &)
% ( 39 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 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 : 41 ( 39 usr; 39 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-1 aty)
% Number of variables : 151 ( 0 sgn 149 !; 2 ?; 151 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
knowheyan: $tType ).
tff(type_def_6,type,
job: $tType ).
tff(type_def_7,type,
age: $tType ).
tff(func_def_0,type,
age_of: knowheyan > age ).
tff(func_def_1,type,
job_of: knowheyan > job ).
tff(func_def_2,type,
a: knowheyan ).
tff(func_def_3,type,
b: knowheyan ).
tff(func_def_4,type,
c: knowheyan ).
tff(func_def_5,type,
d: knowheyan ).
tff(func_def_6,type,
e: knowheyan ).
tff(func_def_7,type,
airfoil_technician: job ).
tff(func_def_8,type,
communications_consultant: job ).
tff(func_def_9,type,
space_planner: job ).
tff(func_def_10,type,
lunar_energy_engineer: job ).
tff(func_def_11,type,
synthetic_food_nutitionist: job ).
tff(func_def_12,type,
sK0: knowheyan ).
tff(pred_def_1,type,
greater: ( age * age ) > $o ).
tff(f1,axiom,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_b) ).
tff(f2,axiom,
a != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_c) ).
tff(f3,axiom,
a != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_d) ).
tff(f4,axiom,
a != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_e) ).
tff(f5,axiom,
b != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_c) ).
tff(f6,axiom,
b != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_d) ).
tff(f7,axiom,
b != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_e) ).
tff(f8,axiom,
c != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_d) ).
tff(f9,axiom,
c != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_e) ).
tff(f10,axiom,
d != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_not_e) ).
tff(f14,axiom,
airfoil_technician != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',airfoil_technician_not_synthetic_food_nutitionist) ).
tff(f17,axiom,
communications_consultant != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_synthetic_food_nutitionist) ).
tff(f19,axiom,
space_planner != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',space_planner_not_synthetic_food_nutitionist) ).
tff(f20,axiom,
lunar_energy_engineer != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lunar_energy_engineer_not_synthetic_food_nutitionist) ).
tff(f21,axiom,
! [X0: knowheyan] :
( ( X0 = a )
| ( X0 = b )
| ( X0 = c )
| ( X0 = d )
| ( X0 = e ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_knowheyans) ).
tff(f22,axiom,
! [X0: job] :
( ( X0 = airfoil_technician )
| ( X0 = communications_consultant )
| ( X0 = space_planner )
| ( X0 = lunar_energy_engineer )
| ( X0 = synthetic_food_nutitionist ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_jobs) ).
tff(f24,axiom,
! [X0: knowheyan,X1: knowheyan] :
( ( X0 != X1 )
=> ( job_of(X0) != job_of(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_jobs) ).
tff(f25,axiom,
! [X0: age,X1: age,X2: age] :
( ( greater(X0,X1)
& greater(X1,X2) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_transitive) ).
tff(f26,axiom,
! [X0: age,X1: age] :
~ ( greater(X0,X1)
& greater(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_irreflexive) ).
tff(f27,axiom,
! [X0: age,X1: age] :
( ( X0 != X1 )
<=> ( greater(X0,X1)
| greater(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_greater) ).
tff(f28,axiom,
! [X0: knowheyan] :
( ( job_of(X0) = communications_consultant )
=> ~ ? [X1: knowheyan] : greater(age_of(X1),age_of(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_younger) ).
tff(f29,axiom,
greater(age_of(a),age_of(d)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info1) ).
tff(f30,axiom,
greater(age_of(d),age_of(b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info2) ).
tff(f31,axiom,
! [X0: knowheyan] :
( ( job_of(X0) = lunar_energy_engineer )
=> greater(age_of(X0),age_of(b)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info3) ).
tff(f32,axiom,
greater(age_of(b),age_of(c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info4) ).
tff(f33,axiom,
! [X0: knowheyan,X1: knowheyan] :
( ( ( job_of(X0) = airfoil_technician )
& ( job_of(X1) = space_planner ) )
=> greater(age_of(X0),age_of(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_job1) ).
tff(f34,axiom,
! [X0: knowheyan,X1: knowheyan] :
( ( ( job_of(X0) = space_planner )
& ( job_of(X1) = synthetic_food_nutitionist ) )
=> greater(age_of(X0),age_of(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_job2) ).
tff(f35,axiom,
? [X0: knowheyan] : greater(age_of(c),age_of(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_youngest) ).
tff(f36,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(f37,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 ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
tff(f39,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( job_of(X0) != job_of(X1) )
| ( X0 = X1 ) ),
inference(ennf_transformation,[],[f24]) ).
tff(f40,plain,
! [X0: age,X1: age,X2: age] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(ennf_transformation,[],[f25]) ).
tff(f41,plain,
! [X0: age,X1: age,X2: age] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(flattening,[],[f40]) ).
tff(f42,plain,
! [X0: age,X1: age] :
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(ennf_transformation,[],[f26]) ).
tff(f43,plain,
! [X0: knowheyan] :
( ! [X1: knowheyan] : ~ greater(age_of(X1),age_of(X0))
| ( communications_consultant != job_of(X0) ) ),
inference(ennf_transformation,[],[f28]) ).
tff(f44,plain,
! [X0: knowheyan] :
( greater(age_of(X0),age_of(b))
| ( lunar_energy_engineer != job_of(X0) ) ),
inference(ennf_transformation,[],[f31]) ).
tff(f45,plain,
! [X0: knowheyan,X1: knowheyan] :
( greater(age_of(X0),age_of(X1))
| ( airfoil_technician != job_of(X0) )
| ( space_planner != job_of(X1) ) ),
inference(ennf_transformation,[],[f33]) ).
tff(f46,plain,
! [X0: knowheyan,X1: knowheyan] :
( greater(age_of(X0),age_of(X1))
| ( airfoil_technician != job_of(X0) )
| ( space_planner != job_of(X1) ) ),
inference(flattening,[],[f45]) ).
tff(f47,plain,
! [X0: knowheyan,X1: knowheyan] :
( greater(age_of(X0),age_of(X1))
| ( space_planner != job_of(X0) )
| ( synthetic_food_nutitionist != job_of(X1) ) ),
inference(ennf_transformation,[],[f34]) ).
tff(f48,plain,
! [X0: knowheyan,X1: knowheyan] :
( greater(age_of(X0),age_of(X1))
| ( space_planner != job_of(X0) )
| ( synthetic_food_nutitionist != job_of(X1) ) ),
inference(flattening,[],[f47]) ).
tff(f49,plain,
( ( communications_consultant != job_of(a) )
| ( lunar_energy_engineer != job_of(d) )
| ( airfoil_technician != job_of(b) )
| ( space_planner != job_of(c) )
| ( synthetic_food_nutitionist != job_of(e) ) ),
inference(ennf_transformation,[],[f37]) ).
tff(f50,plain,
! [X0: age,X1: age] :
( ( ( X0 != X1 )
| ( ~ greater(X0,X1)
& ~ greater(X1,X0) ) )
& ( greater(X0,X1)
| greater(X1,X0)
| ( X0 = X1 ) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f51,plain,
! [X0: age,X1: age] :
( ( ( X0 != X1 )
| ( ~ greater(X0,X1)
& ~ greater(X1,X0) ) )
& ( greater(X0,X1)
| greater(X1,X0)
| ( X0 = X1 ) ) ),
inference(flattening,[],[f50]) ).
tff(f52,plain,
greater(age_of(c),age_of(sK0)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f35]) ).
tff(f53,plain,
a != b,
inference(cnf_transformation,[],[f1]) ).
tff(f54,plain,
a != c,
inference(cnf_transformation,[],[f2]) ).
tff(f55,plain,
a != d,
inference(cnf_transformation,[],[f3]) ).
tff(f56,plain,
a != e,
inference(cnf_transformation,[],[f4]) ).
tff(f57,plain,
b != c,
inference(cnf_transformation,[],[f5]) ).
tff(f58,plain,
b != d,
inference(cnf_transformation,[],[f6]) ).
tff(f59,plain,
b != e,
inference(cnf_transformation,[],[f7]) ).
tff(f60,plain,
c != d,
inference(cnf_transformation,[],[f8]) ).
tff(f61,plain,
c != e,
inference(cnf_transformation,[],[f9]) ).
tff(f62,plain,
d != e,
inference(cnf_transformation,[],[f10]) ).
tff(f66,plain,
airfoil_technician != synthetic_food_nutitionist,
inference(cnf_transformation,[],[f14]) ).
tff(f69,plain,
communications_consultant != synthetic_food_nutitionist,
inference(cnf_transformation,[],[f17]) ).
tff(f71,plain,
space_planner != synthetic_food_nutitionist,
inference(cnf_transformation,[],[f19]) ).
tff(f72,plain,
lunar_energy_engineer != synthetic_food_nutitionist,
inference(cnf_transformation,[],[f20]) ).
tff(f73,plain,
! [X0: knowheyan] :
( ( e = X0 )
| ( b = X0 )
| ( c = X0 )
| ( d = X0 )
| ( a = X0 ) ),
inference(cnf_transformation,[],[f21]) ).
tff(f74,plain,
! [X0: job] :
( ( synthetic_food_nutitionist = X0 )
| ( communications_consultant = X0 )
| ( space_planner = X0 )
| ( lunar_energy_engineer = X0 )
| ( airfoil_technician = X0 ) ),
inference(cnf_transformation,[],[f22]) ).
tff(f76,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( job_of(X0) != job_of(X1) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f77,plain,
! [X2: age,X0: age,X1: age] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
inference(cnf_transformation,[],[f41]) ).
tff(f78,plain,
! [X0: age,X1: age] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tff(f79,plain,
! [X0: age,X1: age] :
( greater(X0,X1)
| greater(X1,X0)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f51]) ).
tff(f80,plain,
! [X0: age,X1: age] :
( ( X0 != X1 )
| ~ greater(X1,X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f82,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( communications_consultant != job_of(X0) )
| ~ greater(age_of(X1),age_of(X0)) ),
inference(cnf_transformation,[],[f43]) ).
tff(f83,plain,
greater(age_of(a),age_of(d)),
inference(cnf_transformation,[],[f29]) ).
tff(f84,plain,
greater(age_of(d),age_of(b)),
inference(cnf_transformation,[],[f30]) ).
tff(f85,plain,
! [X0: knowheyan] :
( ( lunar_energy_engineer != job_of(X0) )
| greater(age_of(X0),age_of(b)) ),
inference(cnf_transformation,[],[f44]) ).
tff(f86,plain,
greater(age_of(b),age_of(c)),
inference(cnf_transformation,[],[f32]) ).
tff(f87,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( space_planner != job_of(X1) )
| ( airfoil_technician != job_of(X0) )
| greater(age_of(X0),age_of(X1)) ),
inference(cnf_transformation,[],[f46]) ).
tff(f88,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( synthetic_food_nutitionist != job_of(X1) )
| ( space_planner != job_of(X0) )
| greater(age_of(X0),age_of(X1)) ),
inference(cnf_transformation,[],[f48]) ).
tff(f89,plain,
greater(age_of(c),age_of(sK0)),
inference(cnf_transformation,[],[f52]) ).
tff(f90,plain,
( ( communications_consultant != job_of(a) )
| ( lunar_energy_engineer != job_of(d) )
| ( airfoil_technician != job_of(b) )
| ( space_planner != job_of(c) )
| ( synthetic_food_nutitionist != job_of(e) ) ),
inference(cnf_transformation,[],[f49]) ).
tff(f92,plain,
! [X1: age] : ~ greater(X1,X1),
inference(equality_resolution,[],[f80]) ).
tff(f94,definition,
( spl1_1
<=> ( synthetic_food_nutitionist = job_of(e) ) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
tff(f95,plain,
( ( synthetic_food_nutitionist != job_of(e) )
| spl1_1 ),
inference(avatar_component_clause,[],[f94]) ).
tff(f97,definition,
( spl1_2
<=> ( space_planner = job_of(c) ) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
tff(f98,plain,
( ( space_planner != job_of(c) )
| spl1_2 ),
inference(avatar_component_clause,[],[f97]) ).
tff(f100,definition,
( spl1_3
<=> ( airfoil_technician = job_of(b) ) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
tff(f101,plain,
( ( airfoil_technician != job_of(b) )
| spl1_3 ),
inference(avatar_component_clause,[],[f100]) ).
tff(f103,definition,
( spl1_4
<=> ( lunar_energy_engineer = job_of(d) ) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
tff(f106,definition,
( spl1_5
<=> ( communications_consultant = job_of(a) ) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
tff(f108,plain,
( ~ spl1_1
| ~ spl1_2
| ~ spl1_3
| ~ spl1_4
| ~ spl1_5 ),
inference(avatar_split_clause,[],[f90,f106,f103,f100,f97,f94]) ).
tff(f109,plain,
! [X0: job,X1: job] :
( ( X0 = X1 )
| ( lunar_energy_engineer = X1 )
| ( lunar_energy_engineer = X0 )
| ( communications_consultant = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = X0 )
| ( space_planner = X0 )
| ( space_planner = X1 )
| ( airfoil_technician = X0 ) ),
inference(superposition,[],[f74,f74]) ).
tff(f114,plain,
( ( synthetic_food_nutitionist != synthetic_food_nutitionist )
| ( communications_consultant = job_of(e) )
| ( space_planner = job_of(e) )
| ( lunar_energy_engineer = job_of(e) )
| ( airfoil_technician = job_of(e) )
| spl1_1 ),
inference(superposition,[],[f95,f74]) ).
tff(f115,plain,
( ( communications_consultant = job_of(e) )
| ( space_planner = job_of(e) )
| ( lunar_energy_engineer = job_of(e) )
| ( airfoil_technician = job_of(e) )
| spl1_1 ),
inference(trivial_inequality_removal,[],[f114]) ).
tff(f117,definition,
( spl1_6
<=> ( airfoil_technician = job_of(e) ) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
tff(f118,plain,
( ( airfoil_technician = job_of(e) )
| ~ spl1_6 ),
inference(avatar_component_clause,[],[f117]) ).
tff(f120,definition,
( spl1_7
<=> ( lunar_energy_engineer = job_of(e) ) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
tff(f121,plain,
( ( lunar_energy_engineer = job_of(e) )
| ~ spl1_7 ),
inference(avatar_component_clause,[],[f120]) ).
tff(f123,definition,
( spl1_8
<=> ( space_planner = job_of(e) ) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
tff(f124,plain,
( ( space_planner = job_of(e) )
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f123]) ).
tff(f126,definition,
( spl1_9
<=> ( communications_consultant = job_of(e) ) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
tff(f127,plain,
( ( communications_consultant = job_of(e) )
| ~ spl1_9 ),
inference(avatar_component_clause,[],[f126]) ).
tff(f128,plain,
( spl1_6
| spl1_7
| spl1_8
| spl1_9
| spl1_1 ),
inference(avatar_split_clause,[],[f115,f94,f126,f123,f120,f117]) ).
tff(f138,definition,
( spl1_10
<=> ( a = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition]) ).
tff(f139,plain,
( ( a = sK0 )
| ~ spl1_10 ),
inference(avatar_component_clause,[],[f138]) ).
tff(f141,definition,
( spl1_11
<=> ( d = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
tff(f142,plain,
( ( d = sK0 )
| ~ spl1_11 ),
inference(avatar_component_clause,[],[f141]) ).
tff(f144,definition,
( spl1_12
<=> ( c = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
tff(f145,plain,
( ( c = sK0 )
| ~ spl1_12 ),
inference(avatar_component_clause,[],[f144]) ).
tff(f147,definition,
( spl1_13
<=> ( b = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
tff(f148,plain,
( ( b = sK0 )
| ~ spl1_13 ),
inference(avatar_component_clause,[],[f147]) ).
tff(f158,plain,
! [X2: age,X0: age,X1: age] :
( ~ greater(X0,X1)
| greater(X0,X2)
| greater(X2,X1)
| ( X1 = X2 ) ),
inference(resolution,[],[f77,f79]) ).
tff(f160,plain,
~ greater(age_of(sK0),age_of(c)),
inference(resolution,[],[f78,f89]) ).
tff(f163,plain,
( ~ greater(age_of(a),age_of(c))
| ~ spl1_10 ),
inference(forward_demodulation,[],[f160,f139]) ).
tff(f165,plain,
~ greater(age_of(c),age_of(b)),
inference(resolution,[],[f86,f78]) ).
tff(f166,plain,
! [X0: age] :
( greater(X0,age_of(c))
| ~ greater(X0,age_of(b)) ),
inference(resolution,[],[f86,f77]) ).
tff(f168,plain,
! [X0: age] :
( ~ greater(X0,age_of(a))
| greater(X0,age_of(d)) ),
inference(resolution,[],[f83,f77]) ).
tff(f169,plain,
~ greater(age_of(b),age_of(d)),
inference(resolution,[],[f84,f78]) ).
tff(f170,plain,
! [X0: age] :
( ~ greater(X0,age_of(d))
| greater(X0,age_of(b)) ),
inference(resolution,[],[f84,f77]) ).
tff(f174,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( synthetic_food_nutitionist != synthetic_food_nutitionist )
| ( space_planner != job_of(X1) )
| greater(age_of(X1),age_of(X0))
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( lunar_energy_engineer = job_of(X0) )
| ( airfoil_technician = job_of(X0) ) ),
inference(superposition,[],[f88,f74]) ).
tff(f175,plain,
! [X0: knowheyan,X1: knowheyan] :
( ( space_planner != job_of(X1) )
| greater(age_of(X1),age_of(X0))
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( lunar_energy_engineer = job_of(X0) )
| ( airfoil_technician = job_of(X0) ) ),
inference(trivial_inequality_removal,[],[f174]) ).
tff(f180,plain,
! [X0: age] :
( greater(age_of(b),X0)
| greater(X0,age_of(c))
| ( age_of(c) = X0 ) ),
inference(resolution,[],[f158,f86]) ).
tff(f212,plain,
greater(age_of(a),age_of(b)),
inference(resolution,[],[f170,f83]) ).
tff(f214,plain,
( greater(age_of(b),age_of(b))
| greater(age_of(d),age_of(c))
| ( age_of(d) = age_of(c) ) ),
inference(resolution,[],[f170,f180]) ).
tff(f220,plain,
( greater(age_of(d),age_of(c))
| ( age_of(d) = age_of(c) ) ),
inference(forward_subsumption_resolution,[],[f214,f92]) ).
tff(f222,definition,
( spl1_15
<=> ( age_of(d) = age_of(c) ) ),
introduced(definition,[new_symbols(definition,[spl1_15])],[avatar_definition]) ).
tff(f223,plain,
( ( age_of(d) = age_of(c) )
| ~ spl1_15 ),
inference(avatar_component_clause,[],[f222]) ).
tff(f225,definition,
( spl1_16
<=> greater(age_of(d),age_of(c)) ),
introduced(definition,[new_symbols(definition,[spl1_16])],[avatar_definition]) ).
tff(f226,plain,
( greater(age_of(d),age_of(c))
| ~ spl1_16 ),
inference(avatar_component_clause,[],[f225]) ).
tff(f227,plain,
( spl1_15
| spl1_16 ),
inference(avatar_split_clause,[],[f220,f225,f222]) ).
tff(f231,plain,
( greater(age_of(c),age_of(b))
| ~ spl1_15 ),
inference(superposition,[],[f84,f223]) ).
tff(f235,plain,
( $false
| ~ spl1_15 ),
inference(forward_subsumption_resolution,[],[f231,f165]) ).
tff(f236,plain,
~ spl1_15,
inference(avatar_contradiction_clause,[],[f235]) ).
tff(f246,plain,
( greater(age_of(b),age_of(d))
| greater(age_of(a),age_of(c))
| ( age_of(a) = age_of(c) ) ),
inference(resolution,[],[f168,f180]) ).
tff(f251,plain,
( greater(age_of(a),age_of(c))
| ( age_of(a) = age_of(c) ) ),
inference(forward_subsumption_resolution,[],[f246,f169]) ).
tff(f252,plain,
( ( age_of(a) = age_of(c) )
| ~ spl1_10 ),
inference(forward_subsumption_resolution,[],[f251,f163]) ).
tff(f254,plain,
( greater(age_of(c),age_of(b))
| ~ spl1_10 ),
inference(superposition,[],[f212,f252]) ).
tff(f259,plain,
( $false
| ~ spl1_10 ),
inference(forward_subsumption_resolution,[],[f254,f165]) ).
tff(f260,plain,
~ spl1_10,
inference(avatar_contradiction_clause,[],[f259]) ).
tff(f262,plain,
( ~ greater(age_of(d),age_of(c))
| ~ spl1_11 ),
inference(forward_demodulation,[],[f160,f142]) ).
tff(f271,plain,
( $false
| ~ spl1_11
| ~ spl1_16 ),
inference(forward_subsumption_resolution,[],[f262,f226]) ).
tff(f272,plain,
( ~ spl1_11
| ~ spl1_16 ),
inference(avatar_contradiction_clause,[],[f271]) ).
tff(f279,plain,
( greater(age_of(c),age_of(c))
| ~ spl1_12 ),
inference(superposition,[],[f89,f145]) ).
tff(f280,plain,
( $false
| ~ spl1_12 ),
inference(forward_subsumption_resolution,[],[f279,f92]) ).
tff(f281,plain,
~ spl1_12,
inference(avatar_contradiction_clause,[],[f280]) ).
tff(f283,plain,
( ~ greater(age_of(b),age_of(c))
| ~ spl1_13 ),
inference(forward_demodulation,[],[f160,f148]) ).
tff(f285,plain,
( $false
| ~ spl1_13 ),
inference(forward_subsumption_resolution,[],[f283,f86]) ).
tff(f286,plain,
~ spl1_13,
inference(avatar_contradiction_clause,[],[f285]) ).
tff(f354,plain,
~ greater(age_of(sK0),age_of(b)),
inference(resolution,[],[f160,f166]) ).
tff(f355,plain,
( greater(age_of(b),age_of(sK0))
| ( age_of(c) = age_of(sK0) ) ),
inference(resolution,[],[f160,f180]) ).
tff(f360,definition,
( spl1_26
<=> ( age_of(c) = age_of(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl1_26])],[avatar_definition]) ).
tff(f361,plain,
( ( age_of(c) = age_of(sK0) )
| ~ spl1_26 ),
inference(avatar_component_clause,[],[f360]) ).
tff(f363,definition,
( spl1_27
<=> greater(age_of(b),age_of(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_27])],[avatar_definition]) ).
tff(f364,plain,
( greater(age_of(b),age_of(sK0))
| ~ spl1_27 ),
inference(avatar_component_clause,[],[f363]) ).
tff(f365,plain,
( spl1_26
| spl1_27 ),
inference(avatar_split_clause,[],[f355,f363,f360]) ).
tff(f370,plain,
( greater(age_of(c),age_of(c))
| ~ spl1_26 ),
inference(superposition,[],[f89,f361]) ).
tff(f373,plain,
( $false
| ~ spl1_26 ),
inference(forward_subsumption_resolution,[],[f370,f92]) ).
tff(f374,plain,
~ spl1_26,
inference(avatar_contradiction_clause,[],[f373]) ).
tff(f891,definition,
( spl1_51
<=> ! [X0: knowheyan] :
( ( c = X0 )
| ( a = X0 )
| ( d = X0 )
| ( b = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl1_51])],[avatar_definition]) ).
tff(f892,plain,
( ! [X0: knowheyan] :
( ( a = X0 )
| ( c = X0 )
| ( d = X0 )
| ( b = X0 ) )
| ~ spl1_51 ),
inference(avatar_component_clause,[],[f891]) ).
tff(f893,plain,
( ( a != sK0 )
| spl1_10 ),
inference(avatar_component_clause,[],[f138]) ).
tff(f895,plain,
( ( d != sK0 )
| spl1_11 ),
inference(avatar_component_clause,[],[f141]) ).
tff(f897,plain,
( ( b != sK0 )
| spl1_13 ),
inference(avatar_component_clause,[],[f147]) ).
tff(f899,plain,
( ( c != sK0 )
| spl1_12 ),
inference(avatar_component_clause,[],[f144]) ).
tff(f928,plain,
( ~ greater(age_of(c),age_of(d))
| ~ spl1_16 ),
inference(resolution,[],[f226,f78]) ).
tff(f1007,plain,
! [X0: knowheyan,X1: job] :
( ( lunar_energy_engineer != lunar_energy_engineer )
| greater(age_of(X0),age_of(b))
| ( job_of(X0) = X1 )
| ( lunar_energy_engineer = X1 )
| ( communications_consultant = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( space_planner = X1 )
| ( airfoil_technician = job_of(X0) ) ),
inference(superposition,[],[f85,f109]) ).
tff(f1068,plain,
! [X0: knowheyan,X1: job] :
( greater(age_of(X0),age_of(b))
| ( job_of(X0) = X1 )
| ( lunar_energy_engineer = X1 )
| ( communications_consultant = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( space_planner = X1 )
| ( airfoil_technician = job_of(X0) ) ),
inference(trivial_inequality_removal,[],[f1007]) ).
tff(f1072,plain,
! [X0: job] :
( ( job_of(sK0) = X0 )
| ( lunar_energy_engineer = X0 )
| ( communications_consultant = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = job_of(sK0) )
| ( space_planner = job_of(sK0) )
| ( space_planner = X0 )
| ( airfoil_technician = job_of(sK0) ) ),
inference(resolution,[],[f1068,f354]) ).
tff(f1074,plain,
! [X0: knowheyan,X1: job] :
( ( job_of(X0) = X1 )
| ( lunar_energy_engineer = X1 )
| ( communications_consultant = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( space_planner = X1 )
| ( airfoil_technician = job_of(X0) )
| ~ greater(age_of(b),age_of(X0)) ),
inference(resolution,[],[f1068,f78]) ).
tff(f1076,plain,
! [X0: job] :
( ( job_of(b) = X0 )
| ( lunar_energy_engineer = X0 )
| ( communications_consultant = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = job_of(b) )
| ( space_planner = job_of(b) )
| ( space_planner = X0 )
| ( airfoil_technician = job_of(b) ) ),
inference(resolution,[],[f1068,f92]) ).
tff(f1077,plain,
( ( airfoil_technician = job_of(b) )
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f100]) ).
tff(f1079,definition,
( spl1_52
<=> ( space_planner = job_of(b) ) ),
introduced(definition,[new_symbols(definition,[spl1_52])],[avatar_definition]) ).
tff(f1080,plain,
( ( space_planner = job_of(b) )
| ~ spl1_52 ),
inference(avatar_component_clause,[],[f1079]) ).
tff(f1082,definition,
( spl1_53
<=> ( communications_consultant = job_of(b) ) ),
introduced(definition,[new_symbols(definition,[spl1_53])],[avatar_definition]) ).
tff(f1083,plain,
( ( communications_consultant = job_of(b) )
| ~ spl1_53 ),
inference(avatar_component_clause,[],[f1082]) ).
tff(f1085,definition,
( spl1_54
<=> ! [X0: job] :
( ( job_of(b) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl1_54])],[avatar_definition]) ).
tff(f1086,plain,
( ! [X0: job] :
( ( job_of(b) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_54 ),
inference(avatar_component_clause,[],[f1085]) ).
tff(f1087,plain,
( spl1_3
| spl1_52
| spl1_53
| spl1_54 ),
inference(avatar_split_clause,[],[f1076,f1085,f1082,f1079,f100]) ).
tff(f1088,plain,
! [X0: knowheyan,X1: job] :
( ~ greater(age_of(b),age_of(X0))
| ( lunar_energy_engineer = X1 )
| ( communications_consultant = X1 )
| ( airfoil_technician = X1 )
| ( space_planner = job_of(X0) )
| ( space_planner = X1 )
| ( airfoil_technician = job_of(X0) )
| ( job_of(X0) = X1 ) ),
inference(forward_subsumption_resolution,[],[f1074,f82]) ).
tff(f1090,definition,
( spl1_55
<=> ( airfoil_technician = job_of(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl1_55])],[avatar_definition]) ).
tff(f1091,plain,
( ( airfoil_technician = job_of(sK0) )
| ~ spl1_55 ),
inference(avatar_component_clause,[],[f1090]) ).
tff(f1093,definition,
( spl1_56
<=> ( space_planner = job_of(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl1_56])],[avatar_definition]) ).
tff(f1094,plain,
( ( space_planner = job_of(sK0) )
| ~ spl1_56 ),
inference(avatar_component_clause,[],[f1093]) ).
tff(f1096,definition,
( spl1_57
<=> ( communications_consultant = job_of(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl1_57])],[avatar_definition]) ).
tff(f1097,plain,
( ( communications_consultant = job_of(sK0) )
| ~ spl1_57 ),
inference(avatar_component_clause,[],[f1096]) ).
tff(f1099,definition,
( spl1_58
<=> ! [X0: job] :
( ( job_of(sK0) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl1_58])],[avatar_definition]) ).
tff(f1100,plain,
( ! [X0: job] :
( ( job_of(sK0) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_58 ),
inference(avatar_component_clause,[],[f1099]) ).
tff(f1101,plain,
( spl1_55
| spl1_56
| spl1_57
| spl1_58 ),
inference(avatar_split_clause,[],[f1072,f1099,f1096,f1093,f1090]) ).
tff(f1107,plain,
( ( airfoil_technician = job_of(e) )
| ( b = sK0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| ~ spl1_55 ),
inference(superposition,[],[f1091,f73]) ).
tff(f1122,plain,
( ( airfoil_technician = job_of(e) )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_13
| ~ spl1_55 ),
inference(forward_subsumption_resolution,[],[f1107,f897]) ).
tff(f1125,plain,
( ( airfoil_technician = job_of(e) )
| ( d = sK0 )
| ( a = sK0 )
| spl1_12
| spl1_13
| ~ spl1_55 ),
inference(forward_subsumption_resolution,[],[f1122,f899]) ).
tff(f1126,plain,
( ( airfoil_technician = job_of(e) )
| ( a = sK0 )
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_55 ),
inference(forward_subsumption_resolution,[],[f1125,f895]) ).
tff(f1127,plain,
( ( airfoil_technician = job_of(e) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_55 ),
inference(forward_subsumption_resolution,[],[f1126,f893]) ).
tff(f1128,plain,
( spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_55 ),
inference(avatar_split_clause,[],[f1127,f1090,f147,f144,f141,f138,f117]) ).
tff(f1140,plain,
( ! [X0: knowheyan] :
( ( airfoil_technician != job_of(X0) )
| ( e = X0 ) )
| ~ spl1_6 ),
inference(superposition,[],[f76,f118]) ).
tff(f1164,plain,
( ( airfoil_technician != airfoil_technician )
| ( b = e )
| ~ spl1_3
| ~ spl1_6 ),
inference(superposition,[],[f1140,f1077]) ).
tff(f1170,plain,
( ( b = e )
| ~ spl1_3
| ~ spl1_6 ),
inference(trivial_inequality_removal,[],[f1164]) ).
tff(f1173,plain,
( $false
| ~ spl1_3
| ~ spl1_6 ),
inference(forward_subsumption_resolution,[],[f1170,f59]) ).
tff(f1174,plain,
( ~ spl1_3
| ~ spl1_6 ),
inference(avatar_contradiction_clause,[],[f1173]) ).
tff(f1202,plain,
( $false
| ~ spl1_52
| ~ spl1_55 ),
inference(unit_resulting_resolution,[],[f87,f1091,f354,f1080]) ).
tff(f1221,plain,
( ~ spl1_52
| ~ spl1_55 ),
inference(avatar_contradiction_clause,[],[f1202]) ).
tff(f1222,plain,
( $false
| ~ spl1_53 ),
inference(unit_resulting_resolution,[],[f82,f212,f1083]) ).
tff(f1240,plain,
~ spl1_53,
inference(avatar_contradiction_clause,[],[f1222]) ).
tff(f1270,plain,
( ! [X0: job] :
( ( lunar_energy_engineer != job_of(b) )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_54 ),
inference(equality_factoring,[],[f1086]) ).
tff(f1274,definition,
( spl1_59
<=> ! [X0: job] :
( ( space_planner = X0 )
| ( lunar_energy_engineer = X0 )
| ( communications_consultant = X0 )
| ( airfoil_technician = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl1_59])],[avatar_definition]) ).
tff(f1275,plain,
( ! [X0: job] :
( ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( communications_consultant = X0 )
| ( airfoil_technician = X0 ) )
| ~ spl1_59 ),
inference(avatar_component_clause,[],[f1274]) ).
tff(f1277,definition,
( spl1_60
<=> ( lunar_energy_engineer = job_of(b) ) ),
introduced(definition,[new_symbols(definition,[spl1_60])],[avatar_definition]) ).
tff(f1278,plain,
( ( lunar_energy_engineer != job_of(b) )
| spl1_60 ),
inference(avatar_component_clause,[],[f1277]) ).
tff(f1280,plain,
( ( communications_consultant != job_of(b) )
| spl1_53 ),
inference(avatar_component_clause,[],[f1082]) ).
tff(f1282,plain,
( ( space_planner != job_of(b) )
| spl1_52 ),
inference(avatar_component_clause,[],[f1079]) ).
tff(f1292,definition,
( spl1_61
<=> ( lunar_energy_engineer = job_of(a) ) ),
introduced(definition,[new_symbols(definition,[spl1_61])],[avatar_definition]) ).
tff(f1293,plain,
( ( lunar_energy_engineer = job_of(a) )
| ~ spl1_61 ),
inference(avatar_component_clause,[],[f1292]) ).
tff(f1295,definition,
( spl1_62
<=> ( airfoil_technician = job_of(a) ) ),
introduced(definition,[new_symbols(definition,[spl1_62])],[avatar_definition]) ).
tff(f1296,plain,
( ( airfoil_technician = job_of(a) )
| ~ spl1_62 ),
inference(avatar_component_clause,[],[f1295]) ).
tff(f1298,definition,
( spl1_63
<=> ( space_planner = job_of(a) ) ),
introduced(definition,[new_symbols(definition,[spl1_63])],[avatar_definition]) ).
tff(f1299,plain,
( ( space_planner = job_of(a) )
| ~ spl1_63 ),
inference(avatar_component_clause,[],[f1298]) ).
tff(f1329,plain,
( ( space_planner = job_of(e) )
| ( b = sK0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| ~ spl1_56 ),
inference(superposition,[],[f1094,f73]) ).
tff(f1347,plain,
( ( space_planner = job_of(e) )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_13
| ~ spl1_56 ),
inference(forward_subsumption_resolution,[],[f1329,f897]) ).
tff(f1350,plain,
( ( space_planner = job_of(e) )
| ( d = sK0 )
| ( a = sK0 )
| spl1_12
| spl1_13
| ~ spl1_56 ),
inference(forward_subsumption_resolution,[],[f1347,f899]) ).
tff(f1351,plain,
( ( space_planner = job_of(e) )
| ( a = sK0 )
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_56 ),
inference(forward_subsumption_resolution,[],[f1350,f895]) ).
tff(f1352,plain,
( ( space_planner = job_of(e) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_56 ),
inference(forward_subsumption_resolution,[],[f1351,f893]) ).
tff(f1353,plain,
( spl1_8
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_56 ),
inference(avatar_split_clause,[],[f1352,f1093,f147,f144,f141,f138,f123]) ).
tff(f1388,plain,
( ! [X0: job] :
( ( job_of(e) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 )
| ( b = sK0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 ) )
| ~ spl1_58 ),
inference(superposition,[],[f1100,f73]) ).
tff(f1414,plain,
( ! [X0: job] :
( ( lunar_energy_engineer != job_of(sK0) )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_58 ),
inference(equality_factoring,[],[f1100]) ).
tff(f1418,definition,
( spl1_69
<=> ( lunar_energy_engineer = job_of(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl1_69])],[avatar_definition]) ).
tff(f1419,plain,
( ( lunar_energy_engineer != job_of(sK0) )
| spl1_69 ),
inference(avatar_component_clause,[],[f1418]) ).
tff(f1421,plain,
( ( communications_consultant != job_of(sK0) )
| spl1_57 ),
inference(avatar_component_clause,[],[f1096]) ).
tff(f1425,plain,
( ( space_planner != job_of(sK0) )
| spl1_56 ),
inference(avatar_component_clause,[],[f1093]) ).
tff(f1433,plain,
( ! [X0: job] :
( ( job_of(e) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 ) )
| spl1_13
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f1388,f897]) ).
tff(f1448,plain,
( ! [X0: job] :
( ( job_of(e) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 )
| ( d = sK0 )
| ( a = sK0 ) )
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f1433,f899]) ).
tff(f1449,plain,
( ! [X0: job] :
( ( job_of(e) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 )
| ( a = sK0 ) )
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f1448,f895]) ).
tff(f1450,plain,
( ! [X0: job] :
( ( job_of(e) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f1449,f893]) ).
tff(f1451,plain,
( ! [X0: job] :
( ( airfoil_technician = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(forward_demodulation,[],[f1450,f118]) ).
tff(f1452,plain,
( ! [X0: job] :
( ( airfoil_technician = X0 )
| ( space_planner = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(duplicate_literal_removal,[],[f1451]) ).
tff(f1453,plain,
( spl1_59
| ~ spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(avatar_split_clause,[],[f1452,f1099,f147,f144,f141,f138,f117,f1274]) ).
tff(f1454,plain,
( $false
| ~ spl1_27
| ~ spl1_57 ),
inference(unit_resulting_resolution,[],[f82,f364,f1097]) ).
tff(f1477,plain,
( ~ spl1_27
| ~ spl1_57 ),
inference(avatar_contradiction_clause,[],[f1454]) ).
tff(f1488,plain,
( spl1_59
| ~ spl1_69
| ~ spl1_58 ),
inference(avatar_split_clause,[],[f1414,f1099,f1418,f1274]) ).
tff(f1504,plain,
( ! [X0: job,X1: knowheyan] :
( ( job_of(X1) != X0 )
| ( sK0 = X1 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_58 ),
inference(superposition,[],[f76,f1100]) ).
tff(f1533,plain,
( ! [X0: knowheyan] :
( ( space_planner != job_of(X0) )
| ( b = X0 ) )
| ~ spl1_52 ),
inference(superposition,[],[f76,f1080]) ).
tff(f1536,plain,
( ! [X0: knowheyan] :
( ( space_planner != space_planner )
| ( airfoil_technician != job_of(X0) )
| greater(age_of(X0),age_of(b)) )
| ~ spl1_52 ),
inference(superposition,[],[f87,f1080]) ).
tff(f1541,plain,
( ! [X0: knowheyan] :
( ( airfoil_technician != job_of(X0) )
| greater(age_of(X0),age_of(b)) )
| ~ spl1_52 ),
inference(trivial_inequality_removal,[],[f1536]) ).
tff(f1567,plain,
( ( lunar_energy_engineer != lunar_energy_engineer )
| ( space_planner = synthetic_food_nutitionist )
| ( communications_consultant = synthetic_food_nutitionist )
| ( airfoil_technician = synthetic_food_nutitionist )
| ~ spl1_59 ),
inference(superposition,[],[f72,f1275]) ).
tff(f1575,plain,
( ( space_planner = synthetic_food_nutitionist )
| ( communications_consultant = synthetic_food_nutitionist )
| ( airfoil_technician = synthetic_food_nutitionist )
| ~ spl1_59 ),
inference(trivial_inequality_removal,[],[f1567]) ).
tff(f1579,plain,
( ( communications_consultant = synthetic_food_nutitionist )
| ( airfoil_technician = synthetic_food_nutitionist )
| ~ spl1_59 ),
inference(forward_subsumption_resolution,[],[f1575,f71]) ).
tff(f1581,plain,
( ( airfoil_technician = synthetic_food_nutitionist )
| ~ spl1_59 ),
inference(forward_subsumption_resolution,[],[f1579,f69]) ).
tff(f1582,plain,
( $false
| ~ spl1_59 ),
inference(forward_subsumption_resolution,[],[f1581,f66]) ).
tff(f1583,plain,
~ spl1_59,
inference(avatar_contradiction_clause,[],[f1582]) ).
tff(f1587,plain,
! [X0: job] :
( ( lunar_energy_engineer = X0 )
| ( communications_consultant = X0 )
| ( airfoil_technician = X0 )
| ( space_planner = job_of(c) )
| ( space_planner = X0 )
| ( airfoil_technician = job_of(c) )
| ( job_of(c) = X0 ) ),
inference(resolution,[],[f1088,f86]) ).
tff(f1622,definition,
( spl1_72
<=> ( airfoil_technician = job_of(c) ) ),
introduced(definition,[new_symbols(definition,[spl1_72])],[avatar_definition]) ).
tff(f1623,plain,
( ( airfoil_technician = job_of(c) )
| ~ spl1_72 ),
inference(avatar_component_clause,[],[f1622]) ).
tff(f1624,plain,
( ( space_planner = job_of(c) )
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f97]) ).
tff(f1626,definition,
( spl1_73
<=> ! [X0: job] :
( ( lunar_energy_engineer = X0 )
| ( job_of(c) = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl1_73])],[avatar_definition]) ).
tff(f1627,plain,
( ! [X0: job] :
( ( job_of(c) = X0 )
| ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 ) )
| ~ spl1_73 ),
inference(avatar_component_clause,[],[f1626]) ).
tff(f1628,plain,
( spl1_72
| spl1_2
| spl1_73 ),
inference(avatar_split_clause,[],[f1587,f1626,f97,f1622]) ).
tff(f1652,plain,
( ( space_planner != job_of(e) )
| ( b = sK0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_56 ),
inference(superposition,[],[f1425,f73]) ).
tff(f1659,plain,
( ( space_planner != job_of(e) )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_13
| spl1_56 ),
inference(forward_subsumption_resolution,[],[f1652,f897]) ).
tff(f1660,plain,
( ( space_planner != job_of(e) )
| ( d = sK0 )
| ( a = sK0 )
| spl1_12
| spl1_13
| spl1_56 ),
inference(forward_subsumption_resolution,[],[f1659,f899]) ).
tff(f1661,plain,
( ( space_planner != job_of(e) )
| ( a = sK0 )
| spl1_11
| spl1_12
| spl1_13
| spl1_56 ),
inference(forward_subsumption_resolution,[],[f1660,f895]) ).
tff(f1662,plain,
( ( space_planner != job_of(e) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_56 ),
inference(forward_subsumption_resolution,[],[f1661,f893]) ).
tff(f1668,plain,
( ( lunar_energy_engineer != job_of(e) )
| ( b = sK0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_69 ),
inference(superposition,[],[f1419,f73]) ).
tff(f1677,plain,
( ( lunar_energy_engineer != job_of(e) )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_13
| spl1_69 ),
inference(forward_subsumption_resolution,[],[f1668,f897]) ).
tff(f1680,plain,
( ( lunar_energy_engineer != job_of(e) )
| ( d = sK0 )
| ( a = sK0 )
| spl1_12
| spl1_13
| spl1_69 ),
inference(forward_subsumption_resolution,[],[f1677,f899]) ).
tff(f1681,plain,
( ( lunar_energy_engineer != job_of(e) )
| ( a = sK0 )
| spl1_11
| spl1_12
| spl1_13
| spl1_69 ),
inference(forward_subsumption_resolution,[],[f1680,f895]) ).
tff(f1682,plain,
( ( lunar_energy_engineer != job_of(e) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_69 ),
inference(forward_subsumption_resolution,[],[f1681,f893]) ).
tff(f1704,plain,
( ( communications_consultant != job_of(e) )
| ( b = sK0 )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_57 ),
inference(superposition,[],[f1421,f73]) ).
tff(f1711,plain,
( ( communications_consultant != job_of(e) )
| ( c = sK0 )
| ( d = sK0 )
| ( a = sK0 )
| spl1_13
| spl1_57 ),
inference(forward_subsumption_resolution,[],[f1704,f897]) ).
tff(f1714,plain,
( ( communications_consultant != job_of(e) )
| ( d = sK0 )
| ( a = sK0 )
| spl1_12
| spl1_13
| spl1_57 ),
inference(forward_subsumption_resolution,[],[f1711,f899]) ).
tff(f1715,plain,
( ( communications_consultant != job_of(e) )
| ( a = sK0 )
| spl1_11
| spl1_12
| spl1_13
| spl1_57 ),
inference(forward_subsumption_resolution,[],[f1714,f895]) ).
tff(f1716,plain,
( ( communications_consultant != job_of(e) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_57 ),
inference(forward_subsumption_resolution,[],[f1715,f893]) ).
tff(f1803,plain,
( ! [X0: knowheyan] :
( ( lunar_energy_engineer = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( airfoil_technician = job_of(X0) )
| ( communications_consultant = job_of(X0) )
| ( sK0 = X0 ) )
| ~ spl1_58 ),
inference(equality_resolution,[],[f1504]) ).
tff(f1811,definition,
( spl1_76
<=> ( e = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl1_76])],[avatar_definition]) ).
tff(f1812,plain,
( ( e = sK0 )
| ~ spl1_76 ),
inference(avatar_component_clause,[],[f1811]) ).
tff(f1840,plain,
( ! [X0: job] :
( ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( e = sK0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(superposition,[],[f1803,f1450]) ).
tff(f1849,plain,
( ! [X0: knowheyan] :
( ( lunar_energy_engineer != lunar_energy_engineer )
| greater(age_of(X0),age_of(b))
| ( space_planner = job_of(X0) )
| ( airfoil_technician = job_of(X0) )
| ( communications_consultant = job_of(X0) )
| ( sK0 = X0 ) )
| ~ spl1_58 ),
inference(superposition,[],[f85,f1803]) ).
tff(f1867,plain,
( ! [X0: knowheyan] :
( greater(age_of(X0),age_of(b))
| ( space_planner = job_of(X0) )
| ( airfoil_technician = job_of(X0) )
| ( communications_consultant = job_of(X0) )
| ( sK0 = X0 ) )
| ~ spl1_58 ),
inference(trivial_inequality_removal,[],[f1849]) ).
tff(f1870,plain,
( ! [X0: job] :
( ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( e = sK0 ) )
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(duplicate_literal_removal,[],[f1840]) ).
tff(f1871,plain,
( ! [X0: knowheyan] :
( greater(age_of(X0),age_of(b))
| ( space_planner = job_of(X0) )
| ( communications_consultant = job_of(X0) )
| ( sK0 = X0 ) )
| ~ spl1_52
| ~ spl1_58 ),
inference(forward_subsumption_resolution,[],[f1867,f1541]) ).
tff(f1874,plain,
( ! [X0: knowheyan] :
( greater(age_of(X0),age_of(b))
| ( e = X0 )
| ( space_planner = job_of(X0) )
| ( communications_consultant = job_of(X0) ) )
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_demodulation,[],[f1871,f1812]) ).
tff(f1878,plain,
( ! [X0: knowheyan] :
( ( e = X0 )
| ( space_planner = job_of(X0) )
| ( communications_consultant = job_of(X0) )
| ~ greater(age_of(b),age_of(X0)) )
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(resolution,[],[f1874,f78]) ).
tff(f1882,plain,
( ! [X0: knowheyan] :
( ~ greater(age_of(b),age_of(X0))
| ( space_planner = job_of(X0) )
| ( e = X0 ) )
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f1878,f82]) ).
tff(f1883,plain,
( ( space_planner = job_of(c) )
| ( c = e )
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(resolution,[],[f1882,f86]) ).
tff(f1918,plain,
( ( space_planner = job_of(c) )
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f1883,f61]) ).
tff(f1921,plain,
( spl1_2
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(avatar_split_clause,[],[f1918,f1811,f1099,f1079,f97]) ).
tff(f1935,plain,
( ! [X0: knowheyan] :
( ( space_planner != job_of(X0) )
| ( c = X0 ) )
| ~ spl1_2 ),
inference(superposition,[],[f76,f1624]) ).
tff(f1940,plain,
( ! [X0: knowheyan] :
( ( space_planner != space_planner )
| greater(age_of(c),age_of(X0))
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( lunar_energy_engineer = job_of(X0) )
| ( airfoil_technician = job_of(X0) ) )
| ~ spl1_2 ),
inference(superposition,[],[f175,f1624]) ).
tff(f1943,plain,
( ( space_planner != space_planner )
| ( b = c )
| ~ spl1_2
| ~ spl1_52 ),
inference(superposition,[],[f1533,f1624]) ).
tff(f1944,plain,
( ( b = c )
| ~ spl1_2
| ~ spl1_52 ),
inference(trivial_inequality_removal,[],[f1943]) ).
tff(f1946,plain,
( ! [X0: knowheyan] :
( greater(age_of(c),age_of(X0))
| ( communications_consultant = job_of(X0) )
| ( space_planner = job_of(X0) )
| ( lunar_energy_engineer = job_of(X0) )
| ( airfoil_technician = job_of(X0) ) )
| ~ spl1_2 ),
inference(trivial_inequality_removal,[],[f1940]) ).
tff(f1951,plain,
( $false
| ~ spl1_2
| ~ spl1_52 ),
inference(forward_subsumption_resolution,[],[f1944,f57]) ).
tff(f1952,plain,
( ~ spl1_2
| ~ spl1_52 ),
inference(avatar_contradiction_clause,[],[f1951]) ).
tff(f1955,plain,
( ! [X0: knowheyan] :
( greater(age_of(X0),age_of(b))
| ( e = X0 )
| ( space_planner = job_of(X0) )
| ( airfoil_technician = job_of(X0) )
| ( communications_consultant = job_of(X0) ) )
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_demodulation,[],[f1867,f1812]) ).
tff(f1963,plain,
( ! [X0: knowheyan] :
( ( airfoil_technician != job_of(X0) )
| ( b = X0 ) )
| ~ spl1_3 ),
inference(superposition,[],[f76,f1077]) ).
tff(f2012,plain,
( ! [X0: knowheyan] :
( ( e = X0 )
| ( space_planner = job_of(X0) )
| ( airfoil_technician = job_of(X0) )
| ( communications_consultant = job_of(X0) )
| ~ greater(age_of(b),age_of(X0)) )
| ~ spl1_58
| ~ spl1_76 ),
inference(resolution,[],[f1955,f78]) ).
tff(f2014,plain,
( ( b = e )
| ( space_planner = job_of(b) )
| ( airfoil_technician = job_of(b) )
| ( communications_consultant = job_of(b) )
| ~ spl1_58
| ~ spl1_76 ),
inference(resolution,[],[f1955,f92]) ).
tff(f2016,plain,
( ! [X0: knowheyan] :
( ~ greater(age_of(b),age_of(X0))
| ( space_planner = job_of(X0) )
| ( airfoil_technician = job_of(X0) )
| ( e = X0 ) )
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f2012,f82]) ).
tff(f2018,plain,
( ( space_planner = job_of(c) )
| ( airfoil_technician = job_of(c) )
| ( c = e )
| ~ spl1_58
| ~ spl1_76 ),
inference(resolution,[],[f2016,f86]) ).
tff(f2063,plain,
( ( communications_consultant = job_of(d) )
| ( space_planner = job_of(d) )
| ( lunar_energy_engineer = job_of(d) )
| ( airfoil_technician = job_of(d) )
| greater(age_of(c),age_of(b))
| ~ spl1_2 ),
inference(resolution,[],[f1946,f170]) ).
tff(f2064,plain,
( ( communications_consultant = job_of(a) )
| ( space_planner = job_of(a) )
| ( lunar_energy_engineer = job_of(a) )
| ( airfoil_technician = job_of(a) )
| greater(age_of(c),age_of(d))
| ~ spl1_2 ),
inference(resolution,[],[f1946,f168]) ).
tff(f2071,plain,
( ( communications_consultant = job_of(d) )
| ( space_planner = job_of(d) )
| ( lunar_energy_engineer = job_of(d) )
| ( airfoil_technician = job_of(d) )
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f2063,f165]) ).
tff(f2074,definition,
( spl1_77
<=> ( airfoil_technician = job_of(d) ) ),
introduced(definition,[new_symbols(definition,[spl1_77])],[avatar_definition]) ).
tff(f2075,plain,
( ( airfoil_technician = job_of(d) )
| ~ spl1_77 ),
inference(avatar_component_clause,[],[f2074]) ).
tff(f2076,plain,
( ( lunar_energy_engineer = job_of(d) )
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f103]) ).
tff(f2078,definition,
( spl1_78
<=> ( space_planner = job_of(d) ) ),
introduced(definition,[new_symbols(definition,[spl1_78])],[avatar_definition]) ).
tff(f2079,plain,
( ( space_planner = job_of(d) )
| ~ spl1_78 ),
inference(avatar_component_clause,[],[f2078]) ).
tff(f2081,definition,
( spl1_79
<=> ( communications_consultant = job_of(d) ) ),
introduced(definition,[new_symbols(definition,[spl1_79])],[avatar_definition]) ).
tff(f2082,plain,
( ( communications_consultant = job_of(d) )
| ~ spl1_79 ),
inference(avatar_component_clause,[],[f2081]) ).
tff(f2083,plain,
( spl1_77
| spl1_4
| spl1_78
| spl1_79
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f2071,f97,f2081,f2078,f103,f2074]) ).
tff(f2101,plain,
( ( space_planner != space_planner )
| ( c = d )
| ~ spl1_2
| ~ spl1_78 ),
inference(superposition,[],[f1935,f2079]) ).
tff(f2104,plain,
( ( c = d )
| ~ spl1_2
| ~ spl1_78 ),
inference(trivial_inequality_removal,[],[f2101]) ).
tff(f2111,plain,
( $false
| ~ spl1_2
| ~ spl1_78 ),
inference(forward_subsumption_resolution,[],[f2104,f60]) ).
tff(f2112,plain,
( ~ spl1_2
| ~ spl1_78 ),
inference(avatar_contradiction_clause,[],[f2111]) ).
tff(f2113,plain,
( $false
| ~ spl1_79 ),
inference(unit_resulting_resolution,[],[f82,f83,f2082]) ).
tff(f2135,plain,
~ spl1_79,
inference(avatar_contradiction_clause,[],[f2113]) ).
tff(f2175,plain,
( ( airfoil_technician != airfoil_technician )
| ( a = b )
| ~ spl1_3
| ~ spl1_62 ),
inference(superposition,[],[f1963,f1296]) ).
tff(f2176,plain,
( ( a = b )
| ~ spl1_3
| ~ spl1_62 ),
inference(trivial_inequality_removal,[],[f2175]) ).
tff(f2181,plain,
( $false
| ~ spl1_3
| ~ spl1_62 ),
inference(forward_subsumption_resolution,[],[f2176,f53]) ).
tff(f2182,plain,
( ~ spl1_3
| ~ spl1_62 ),
inference(avatar_contradiction_clause,[],[f2181]) ).
tff(f2192,plain,
( ! [X0: knowheyan] :
( ( lunar_energy_engineer != job_of(X0) )
| ( a = X0 ) )
| ~ spl1_61 ),
inference(superposition,[],[f76,f1293]) ).
tff(f2212,plain,
( ( lunar_energy_engineer != lunar_energy_engineer )
| ( a = d )
| ~ spl1_4
| ~ spl1_61 ),
inference(superposition,[],[f2192,f2076]) ).
tff(f2224,plain,
( ( a = d )
| ~ spl1_4
| ~ spl1_61 ),
inference(trivial_inequality_removal,[],[f2212]) ).
tff(f2227,plain,
( $false
| ~ spl1_4
| ~ spl1_61 ),
inference(forward_subsumption_resolution,[],[f2224,f55]) ).
tff(f2228,plain,
( ~ spl1_4
| ~ spl1_61 ),
inference(avatar_contradiction_clause,[],[f2227]) ).
tff(f2249,plain,
( ( space_planner != space_planner )
| ( a = c )
| ~ spl1_2
| ~ spl1_63 ),
inference(superposition,[],[f1935,f1299]) ).
tff(f2252,plain,
( ( a = c )
| ~ spl1_2
| ~ spl1_63 ),
inference(trivial_inequality_removal,[],[f2249]) ).
tff(f2259,plain,
( $false
| ~ spl1_2
| ~ spl1_63 ),
inference(forward_subsumption_resolution,[],[f2252,f54]) ).
tff(f2260,plain,
( ~ spl1_2
| ~ spl1_63 ),
inference(avatar_contradiction_clause,[],[f2259]) ).
tff(f2263,plain,
( $false
| ~ spl1_9
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_57 ),
inference(forward_subsumption_resolution,[],[f127,f1716]) ).
tff(f2264,plain,
( ~ spl1_9
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_57 ),
inference(avatar_contradiction_clause,[],[f2263]) ).
tff(f2265,plain,
( ( communications_consultant = job_of(a) )
| ( space_planner = job_of(a) )
| ( lunar_energy_engineer = job_of(a) )
| ( airfoil_technician = job_of(a) )
| ~ spl1_2
| ~ spl1_16 ),
inference(forward_subsumption_resolution,[],[f2064,f928]) ).
tff(f2267,plain,
( spl1_62
| spl1_61
| spl1_63
| spl1_5
| ~ spl1_2
| ~ spl1_16 ),
inference(avatar_split_clause,[],[f2265,f225,f97,f106,f1298,f1292,f1295]) ).
tff(f2268,plain,
( $false
| ~ spl1_7
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_69 ),
inference(forward_subsumption_resolution,[],[f121,f1682]) ).
tff(f2269,plain,
( ~ spl1_7
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_69 ),
inference(avatar_contradiction_clause,[],[f2268]) ).
tff(f2288,plain,
( ( airfoil_technician != airfoil_technician )
| ( b = d )
| ~ spl1_3
| ~ spl1_77 ),
inference(superposition,[],[f1963,f2075]) ).
tff(f2289,plain,
( ( b = d )
| ~ spl1_3
| ~ spl1_77 ),
inference(trivial_inequality_removal,[],[f2288]) ).
tff(f2294,plain,
( $false
| ~ spl1_3
| ~ spl1_77 ),
inference(forward_subsumption_resolution,[],[f2289,f58]) ).
tff(f2295,plain,
( ~ spl1_3
| ~ spl1_77 ),
inference(avatar_contradiction_clause,[],[f2294]) ).
tff(f2344,plain,
( ! [X0: knowheyan] :
( ( space_planner = job_of(X0) )
| ( b = X0 )
| ( c = X0 )
| ( d = X0 )
| ( a = X0 ) )
| ~ spl1_8 ),
inference(superposition,[],[f124,f73]) ).
tff(f2355,plain,
( ! [X0: knowheyan] :
( ( space_planner != job_of(X0) )
| ( e = X0 ) )
| ~ spl1_8 ),
inference(superposition,[],[f76,f124]) ).
tff(f2377,plain,
( ! [X0: knowheyan] :
( ( b = X0 )
| ( c = X0 )
| ( d = X0 )
| ( a = X0 ) )
| ~ spl1_2
| ~ spl1_8 ),
inference(forward_subsumption_resolution,[],[f2344,f1935]) ).
tff(f2382,plain,
( spl1_51
| ~ spl1_2
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f2377,f123,f97,f891]) ).
tff(f2403,plain,
( ( airfoil_technician != airfoil_technician )
| ( b = c )
| ~ spl1_3
| ~ spl1_72 ),
inference(superposition,[],[f1963,f1623]) ).
tff(f2404,plain,
( ( b = c )
| ~ spl1_3
| ~ spl1_72 ),
inference(trivial_inequality_removal,[],[f2403]) ).
tff(f2408,plain,
( $false
| ~ spl1_3
| ~ spl1_72 ),
inference(forward_subsumption_resolution,[],[f2404,f57]) ).
tff(f2409,plain,
( ~ spl1_3
| ~ spl1_72 ),
inference(avatar_contradiction_clause,[],[f2408]) ).
tff(f2421,plain,
( ! [X0: job,X1: knowheyan] :
( ( synthetic_food_nutitionist != X0 )
| ( space_planner != job_of(X1) )
| greater(age_of(X1),age_of(c))
| ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 ) )
| ~ spl1_73 ),
inference(superposition,[],[f88,f1627]) ).
tff(f2447,plain,
( ( airfoil_technician != job_of(c) )
| spl1_72 ),
inference(avatar_component_clause,[],[f1622]) ).
tff(f2459,plain,
( ! [X0: job,X1: knowheyan] :
( ( space_planner != job_of(X1) )
| greater(age_of(X1),age_of(c))
| ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 ) )
| ~ spl1_73 ),
inference(forward_subsumption_resolution,[],[f2421,f74]) ).
tff(f2470,definition,
( spl1_83
<=> ! [X1: knowheyan] :
( ( space_planner != job_of(X1) )
| greater(age_of(X1),age_of(c)) ) ),
introduced(definition,[new_symbols(definition,[spl1_83])],[avatar_definition]) ).
tff(f2471,plain,
( ! [X1: knowheyan] :
( greater(age_of(X1),age_of(c))
| ( space_planner != job_of(X1) ) )
| ~ spl1_83 ),
inference(avatar_component_clause,[],[f2470]) ).
tff(f2472,plain,
( spl1_59
| spl1_83
| ~ spl1_73 ),
inference(avatar_split_clause,[],[f2459,f1626,f2470,f1274]) ).
tff(f3008,plain,
( ( space_planner != space_planner )
| ( e = sK0 )
| ~ spl1_8
| ~ spl1_56 ),
inference(superposition,[],[f2355,f1094]) ).
tff(f3012,plain,
( ( e = sK0 )
| ~ spl1_8
| ~ spl1_56 ),
inference(trivial_inequality_removal,[],[f3008]) ).
tff(f3017,plain,
( spl1_76
| ~ spl1_8
| ~ spl1_56 ),
inference(avatar_split_clause,[],[f3012,f1093,f123,f1811]) ).
tff(f3111,plain,
( spl1_59
| ~ spl1_60
| ~ spl1_54 ),
inference(avatar_split_clause,[],[f1270,f1085,f1277,f1274]) ).
tff(f3182,plain,
( ( space_planner != space_planner )
| ( b = e )
| ~ spl1_8
| ~ spl1_52 ),
inference(superposition,[],[f2355,f1080]) ).
tff(f3185,plain,
( ( b = e )
| ~ spl1_8
| ~ spl1_52 ),
inference(trivial_inequality_removal,[],[f3182]) ).
tff(f3191,plain,
( $false
| ~ spl1_8
| ~ spl1_52 ),
inference(forward_subsumption_resolution,[],[f3185,f59]) ).
tff(f3192,plain,
( ~ spl1_8
| ~ spl1_52 ),
inference(avatar_contradiction_clause,[],[f3191]) ).
tff(f3371,plain,
( ! [X0: job,X1: knowheyan] :
( ( job_of(X1) != X0 )
| ( c = X1 )
| ( lunar_energy_engineer = X0 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 ) )
| ~ spl1_73 ),
inference(superposition,[],[f76,f1627]) ).
tff(f3445,plain,
( $false
| spl1_3
| spl1_52
| spl1_53
| ~ spl1_56
| spl1_60 ),
inference(unit_resulting_resolution,[],[f175,f101,f1094,f1282,f1280,f354,f1278]) ).
tff(f3454,plain,
( spl1_3
| spl1_52
| spl1_53
| ~ spl1_56
| spl1_60 ),
inference(avatar_contradiction_clause,[],[f3445]) ).
tff(f3523,plain,
( ! [X0: knowheyan] :
( ( airfoil_technician != job_of(X0) )
| ( e = X0 ) )
| ~ spl1_6 ),
inference(superposition,[],[f76,f118]) ).
tff(f4181,plain,
( ( space_planner != job_of(sK0) )
| ~ spl1_83 ),
inference(resolution,[],[f2471,f160]) ).
tff(f4189,plain,
( ( space_planner != job_of(e) )
| ~ spl1_76
| ~ spl1_83 ),
inference(forward_demodulation,[],[f4181,f1812]) ).
tff(f4684,plain,
( ! [X0: job,X1: job] :
( ( X0 != X1 )
| ( b = c )
| ( lunar_energy_engineer = X1 )
| ( space_planner = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = X1 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_54
| ~ spl1_73 ),
inference(superposition,[],[f3371,f1086]) ).
tff(f4708,plain,
( ! [X0: job,X1: job] :
( ( b = c )
| ( lunar_energy_engineer = X1 )
| ( space_planner = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = X1 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_54
| ~ spl1_73 ),
inference(forward_subsumption_resolution,[],[f4684,f109]) ).
tff(f4712,plain,
( ! [X0: job,X1: job] :
( ( lunar_energy_engineer = X1 )
| ( space_planner = X1 )
| ( airfoil_technician = X1 )
| ( communications_consultant = X1 )
| ( space_planner = X0 )
| ( airfoil_technician = X0 )
| ( communications_consultant = X0 )
| ( lunar_energy_engineer = X0 ) )
| ~ spl1_54
| ~ spl1_73 ),
inference(forward_subsumption_resolution,[],[f4708,f57]) ).
tff(f4725,plain,
( spl1_59
| spl1_59
| ~ spl1_54
| ~ spl1_73 ),
inference(avatar_split_clause,[],[f4712,f1626,f1085,f1274,f1274]) ).
tff(f4794,plain,
( ( airfoil_technician != airfoil_technician )
| ( c = e )
| ~ spl1_6
| ~ spl1_72 ),
inference(superposition,[],[f3523,f1623]) ).
tff(f4796,plain,
( ( c = e )
| ~ spl1_6
| ~ spl1_72 ),
inference(trivial_inequality_removal,[],[f4794]) ).
tff(f4802,plain,
( $false
| ~ spl1_6
| ~ spl1_72 ),
inference(forward_subsumption_resolution,[],[f4796,f61]) ).
tff(f4803,plain,
( ~ spl1_6
| ~ spl1_72 ),
inference(avatar_contradiction_clause,[],[f4802]) ).
tff(f4809,plain,
( ( space_planner = job_of(b) )
| ( airfoil_technician = job_of(b) )
| ( communications_consultant = job_of(b) )
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f2014,f59]) ).
tff(f4817,plain,
( ~ spl1_8
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_56 ),
inference(avatar_split_clause,[],[f1662,f1093,f147,f144,f141,f138,f123]) ).
tff(f4824,plain,
( ~ spl1_8
| ~ spl1_76
| ~ spl1_83 ),
inference(avatar_split_clause,[],[f4189,f2470,f1811,f123]) ).
tff(f4831,plain,
( ( airfoil_technician = job_of(b) )
| ( communications_consultant = job_of(b) )
| spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f4809,f1282]) ).
tff(f4839,plain,
( ( communications_consultant = job_of(b) )
| spl1_3
| spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f4831,f101]) ).
tff(f4846,plain,
( $false
| spl1_3
| spl1_52
| spl1_53
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f4839,f1280]) ).
tff(f4847,plain,
( spl1_3
| spl1_52
| spl1_53
| ~ spl1_58
| ~ spl1_76 ),
inference(avatar_contradiction_clause,[],[f4846]) ).
tff(f4931,plain,
( ! [X0: knowheyan] :
( ( space_planner != space_planner )
| ( airfoil_technician != job_of(X0) )
| greater(age_of(X0),age_of(c)) )
| ~ spl1_2 ),
inference(superposition,[],[f87,f1624]) ).
tff(f4936,plain,
( ! [X0: knowheyan] :
( greater(age_of(X0),age_of(c))
| ( airfoil_technician != job_of(X0) ) )
| ~ spl1_2 ),
inference(trivial_inequality_removal,[],[f4931]) ).
tff(f6152,plain,
( ( a != a )
| ( c = e )
| ( d = e )
| ( b = e )
| ~ spl1_51 ),
inference(superposition,[],[f56,f892]) ).
tff(f6191,plain,
( ( c = e )
| ( d = e )
| ( b = e )
| ~ spl1_51 ),
inference(trivial_inequality_removal,[],[f6152]) ).
tff(f6218,plain,
( ( d = e )
| ( b = e )
| ~ spl1_51 ),
inference(forward_subsumption_resolution,[],[f6191,f61]) ).
tff(f6243,plain,
( ( b = e )
| ~ spl1_51 ),
inference(forward_subsumption_resolution,[],[f6218,f62]) ).
tff(f6269,plain,
( $false
| ~ spl1_51 ),
inference(forward_subsumption_resolution,[],[f6243,f59]) ).
tff(f6270,plain,
~ spl1_51,
inference(avatar_contradiction_clause,[],[f6269]) ).
tff(f6531,plain,
( ( airfoil_technician != job_of(sK0) )
| ~ spl1_2 ),
inference(resolution,[],[f4936,f160]) ).
tff(f6562,plain,
( $false
| ~ spl1_2
| ~ spl1_55 ),
inference(forward_subsumption_resolution,[],[f6531,f1091]) ).
tff(f6563,plain,
( ~ spl1_2
| ~ spl1_55 ),
inference(avatar_contradiction_clause,[],[f6562]) ).
tff(f6571,plain,
( spl1_76
| spl1_59
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(avatar_split_clause,[],[f1870,f1099,f147,f144,f141,f138,f1274,f1811]) ).
tff(f6574,plain,
( ( airfoil_technician = job_of(c) )
| ( c = e )
| spl1_2
| ~ spl1_58
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f2018,f98]) ).
tff(f6589,plain,
( ( c = e )
| spl1_2
| ~ spl1_58
| spl1_72
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f6574,f2447]) ).
tff(f6593,plain,
( $false
| spl1_2
| ~ spl1_58
| spl1_72
| ~ spl1_76 ),
inference(forward_subsumption_resolution,[],[f6589,f61]) ).
tff(f6594,plain,
( spl1_2
| ~ spl1_58
| spl1_72
| ~ spl1_76 ),
inference(avatar_contradiction_clause,[],[f6593]) ).
cnf(s1,plain,
( ~ spl1_1
| ~ spl1_2
| ~ spl1_3
| ~ spl1_4
| ~ spl1_5 ),
inference(sat_conversion,[],[f108]) ).
cnf(s2,plain,
( spl1_1
| spl1_6
| spl1_7
| spl1_8
| spl1_9 ),
inference(sat_conversion,[],[f128]) ).
cnf(s4,plain,
( spl1_15
| spl1_16 ),
inference(sat_conversion,[],[f227]) ).
cnf(s6,plain,
~ spl1_15,
inference(sat_conversion,[],[f236]) ).
cnf(s7,plain,
~ spl1_10,
inference(sat_conversion,[],[f260]) ).
cnf(s9,plain,
( ~ spl1_11
| ~ spl1_16 ),
inference(sat_conversion,[],[f272]) ).
cnf(s10,plain,
~ spl1_12,
inference(sat_conversion,[],[f281]) ).
cnf(s11,plain,
~ spl1_13,
inference(sat_conversion,[],[f286]) ).
cnf(s17,plain,
( spl1_26
| spl1_27 ),
inference(sat_conversion,[],[f365]) ).
cnf(s18,plain,
~ spl1_26,
inference(sat_conversion,[],[f374]) ).
cnf(s74,plain,
( spl1_3
| spl1_52
| spl1_53
| spl1_54 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s75,plain,
( spl1_55
| spl1_56
| spl1_57
| spl1_58 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s76,plain,
( spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_55 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s78,plain,
( ~ spl1_3
| ~ spl1_6 ),
inference(sat_conversion,[],[f1174]) ).
cnf(s79,plain,
( ~ spl1_52
| ~ spl1_55 ),
inference(sat_conversion,[],[f1221]) ).
cnf(s80,plain,
~ spl1_53,
inference(sat_conversion,[],[f1240]) ).
cnf(s90,plain,
( spl1_8
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_56 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s104,plain,
( ~ spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58
| spl1_59 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s105,plain,
( ~ spl1_27
| ~ spl1_57 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s107,plain,
( ~ spl1_58
| spl1_59
| ~ spl1_69 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s111,plain,
~ spl1_59,
inference(sat_conversion,[],[f1583]) ).
cnf(s112,plain,
( spl1_2
| spl1_72
| spl1_73 ),
inference(sat_conversion,[],[f1628]) ).
cnf(s117,plain,
( spl1_2
| ~ spl1_52
| ~ spl1_58
| ~ spl1_76 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s120,plain,
( ~ spl1_2
| ~ spl1_52 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s121,plain,
( ~ spl1_2
| spl1_4
| spl1_77
| spl1_78
| spl1_79 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s124,plain,
( ~ spl1_2
| ~ spl1_78 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s125,plain,
~ spl1_79,
inference(sat_conversion,[],[f2135]) ).
cnf(s127,plain,
( ~ spl1_3
| ~ spl1_62 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s129,plain,
( ~ spl1_4
| ~ spl1_61 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s131,plain,
( ~ spl1_2
| ~ spl1_63 ),
inference(sat_conversion,[],[f2260]) ).
cnf(s132,plain,
( ~ spl1_9
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_57 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s133,plain,
( ~ spl1_2
| spl1_5
| ~ spl1_16
| spl1_61
| spl1_62
| spl1_63 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s134,plain,
( ~ spl1_7
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_69 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s136,plain,
( ~ spl1_3
| ~ spl1_77 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s142,plain,
( ~ spl1_2
| ~ spl1_8
| spl1_51 ),
inference(sat_conversion,[],[f2382]) ).
cnf(s146,plain,
( ~ spl1_3
| ~ spl1_72 ),
inference(sat_conversion,[],[f2409]) ).
cnf(s153,plain,
( spl1_59
| ~ spl1_73
| spl1_83 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s172,plain,
( ~ spl1_8
| ~ spl1_56
| spl1_76 ),
inference(sat_conversion,[],[f3017]) ).
cnf(s177,plain,
( ~ spl1_54
| spl1_59
| ~ spl1_60 ),
inference(sat_conversion,[],[f3111]) ).
cnf(s182,plain,
( ~ spl1_8
| ~ spl1_52 ),
inference(sat_conversion,[],[f3192]) ).
cnf(s188,plain,
( spl1_3
| spl1_52
| spl1_53
| ~ spl1_56
| spl1_60 ),
inference(sat_conversion,[],[f3454]) ).
cnf(s210,plain,
( spl1_59
| ~ spl1_54
| spl1_59
| ~ spl1_73 ),
inference(sat_conversion,[],[f4725]) ).
cnf(s211,plain,
( ~ spl1_54
| spl1_59
| ~ spl1_73 ),
inference(rat,[],[s210]) ).
cnf(s220,plain,
( ~ spl1_6
| ~ spl1_72 ),
inference(sat_conversion,[],[f4803]) ).
cnf(s223,plain,
( ~ spl1_8
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| spl1_56 ),
inference(sat_conversion,[],[f4817]) ).
cnf(s230,plain,
( ~ spl1_8
| ~ spl1_76
| ~ spl1_83 ),
inference(sat_conversion,[],[f4824]) ).
cnf(s238,plain,
( spl1_3
| spl1_52
| spl1_53
| ~ spl1_58
| ~ spl1_76 ),
inference(sat_conversion,[],[f4847]) ).
cnf(s278,plain,
~ spl1_51,
inference(sat_conversion,[],[f6270]) ).
cnf(s306,plain,
( ~ spl1_2
| ~ spl1_55 ),
inference(sat_conversion,[],[f6563]) ).
cnf(s316,plain,
( spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58
| spl1_59
| spl1_76 ),
inference(sat_conversion,[],[f6571]) ).
cnf(s333,plain,
( spl1_2
| ~ spl1_58
| spl1_72
| ~ spl1_76 ),
inference(sat_conversion,[],[f6594]) ).
cnf(s339,plain,
( ~ spl1_2
| ~ spl1_8 ),
inference(rat,[],[s142,s278]) ).
cnf(s340,plain,
( ~ spl1_2
| spl1_4
| spl1_77
| spl1_78 ),
inference(rat,[],[s121,s125]) ).
cnf(s341,plain,
( ~ spl1_58
| ~ spl1_69 ),
inference(rat,[],[s107,s111]) ).
cnf(s342,plain,
( ~ spl1_6
| spl1_10
| spl1_11
| spl1_12
| spl1_13
| ~ spl1_58 ),
inference(rat,[],[s104,s111]) ).
cnf(s352,plain,
( spl1_3
| spl1_52
| spl1_54 ),
inference(rat,[],[s74,s80]) ).
cnf(s360,plain,
spl1_27,
inference(rat,[],[s17,s18]) ).
cnf(s361,plain,
~ spl1_57,
inference(rat,[],[s105,s360]) ).
cnf(s366,plain,
spl1_16,
inference(rat,[],[s4,s6]) ).
cnf(s368,plain,
~ spl1_11,
inference(rat,[],[s9,s366]) ).
cnf(s380,plain,
~ spl1_9,
inference(rat,[],[s132,s361,s11,s10,s7,s368]) ).
cnf(s384,plain,
( spl1_1
| spl1_6
| spl1_7
| spl1_8 ),
inference(rat,[],[s2,s380]) ).
cnf(s385,plain,
( spl1_52
| ~ spl1_56
| spl1_3 ),
inference(rat,[],[s177,s352,s188,s80,s111]) ).
cnf(s386,plain,
( ~ spl1_8
| spl1_3 ),
inference(rat,[],[s385,s182,s223,s7,s10,s11,s368]) ).
cnf(s387,plain,
( spl1_6
| spl1_8
| spl1_1 ),
inference(rat,[],[s341,s134,s75,s384,s76,s90,s7,s10,s11,s368,s361]) ).
cnf(s388,plain,
( spl1_3
| spl1_2
| spl1_1 ),
inference(rat,[],[s352,s79,s211,s75,s112,s342,s220,s387,s90,s386,s111,s361,s7,s10,s11,s368]) ).
cnf(s389,plain,
( spl1_2
| spl1_1 ),
inference(rat,[],[s172,s230,s223,s153,s387,s112,s78,s146,s388,s111,s368,s11,s10,s7]) ).
cnf(s390,plain,
spl1_1,
inference(rat,[],[s342,s75,s387,s90,s339,s306,s389,s7,s10,s11,s368,s361]) ).
cnf(s391,plain,
( ~ spl1_58
| ~ spl1_76
| spl1_3 ),
inference(rat,[],[s117,s120,s238,s80]) ).
cnf(s392,plain,
( ~ spl1_58
| spl1_3 ),
inference(rat,[],[s391,s316,s10,s11,s7,s111,s368]) ).
cnf(s393,plain,
spl1_3,
inference(rat,[],[s112,s211,s220,s352,s76,s79,s306,s75,s392,s90,s386,s111,s7,s10,s11,s368,s361]) ).
cnf(s394,plain,
~ spl1_72,
inference(rat,[],[s146,s393]) ).
cnf(s395,plain,
~ spl1_77,
inference(rat,[],[s136,s393]) ).
cnf(s396,plain,
~ spl1_62,
inference(rat,[],[s127,s393]) ).
cnf(s397,plain,
~ spl1_6,
inference(rat,[],[s78,s393]) ).
cnf(s398,plain,
~ spl1_55,
inference(rat,[],[s76,s368,s11,s10,s7,s397]) ).
cnf(s399,plain,
~ spl1_56,
inference(rat,[],[s153,s230,s112,s172,s339,s90,s111,s394,s7,s10,s11,s368]) ).
cnf(s401,plain,
spl1_58,
inference(rat,[],[s75,s398,s361,s399]) ).
cnf(s404,plain,
spl1_76,
inference(rat,[],[s316,s368,s111,s7,s11,s10,s401]) ).
cnf(s407,plain,
spl1_2,
inference(rat,[],[s333,s401,s394,s404]) ).
cnf(s411,plain,
~ spl1_63,
inference(rat,[],[s131,s407]) ).
cnf(s412,plain,
~ spl1_78,
inference(rat,[],[s124,s407]) ).
cnf(s414,plain,
spl1_4,
inference(rat,[],[s340,s412,s395,s407]) ).
cnf(s418,plain,
~ spl1_61,
inference(rat,[],[s129,s414]) ).
cnf(s419,plain,
~ spl1_5,
inference(rat,[],[s1,s393,s407,s390,s414]) ).
cnf(s420,plain,
$false,
inference(rat,[],[s133,s411,s396,s407,s366,s418,s419]) ).
tff(f6605,plain,
$false,
inference(avatar_sat_refutation,[],[s420]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ134_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n020.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:46:04 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.43/1.70 % (3842271)Detected formulas, will run a generic FOF schedule.
% 3.43/1.70 % (3842372)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1313526676:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.43/1.70 % (3842375)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2675729652:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.43/1.70 % (3842374)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2039871903:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.43/1.70 % (3842371)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1002969356:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.43/1.70 % (3842380)dis-21_1_sil=8000:lcm=predicate:random_seed=1363137166:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.43/1.70 % (3842373)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2166183926:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.43/1.70 % (3842378)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3453072299:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.43/1.70 % (3842374)Instruction limit reached!
% 3.43/1.70 % (3842374)------------------------------
% 3.43/1.70 % (3842374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.70 % (3842374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.70 % (3842374)CaDiCaL version: 2.1.3
% 3.43/1.70 % (3842374)Termination reason: Instruction limit
% 3.43/1.70 % (3842374)Termination phase: Saturation
% 3.43/1.70 % (3842374)Time elapsed: 0.045 s
% 3.43/1.70 % (3842374)Peak memory usage: 88 MB
% 3.43/1.70 % (3842374)Instructions burned: 109 (million)
% 3.43/1.70 % (3842380)Instruction limit reached!
% 3.43/1.70 % (3842380)------------------------------
% 3.43/1.70 % (3842380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.70 % (3842380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.70 % (3842380)CaDiCaL version: 2.1.3
% 3.43/1.70 % (3842380)Termination reason: Instruction limit
% 3.43/1.70 % (3842380)Termination phase: Saturation
% 3.43/1.70 % (3842380)Time elapsed: 0.050 s
% 3.43/1.70 % (3842380)Peak memory usage: 88 MB
% 3.43/1.70 % (3842380)Instructions burned: 132 (million)
% 3.43/1.70 % (3842375)Instruction limit reached!
% 3.43/1.70 % (3842375)------------------------------
% 3.43/1.70 % (3842375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.70 % (3842375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.70 % (3842375)CaDiCaL version: 2.1.3
% 3.43/1.70 % (3842375)Termination reason: Instruction limit
% 3.43/1.70 % (3842375)Termination phase: Saturation
% 3.43/1.70 % (3842375)Time elapsed: 0.055 s
% 3.43/1.70 % (3842375)Peak memory usage: 87 MB
% 3.43/1.70 % (3842375)Instructions burned: 121 (million)
% 3.43/1.70 % (3842378)Instruction limit reached!
% 3.43/1.70 % (3842378)------------------------------
% 3.43/1.70 % (3842378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.70 % (3842378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.70 % (3842378)CaDiCaL version: 2.1.3
% 3.43/1.70 % (3842378)Termination reason: Instruction limit
% 3.43/1.70 % (3842378)Termination phase: Saturation
% 3.43/1.70 % (3842378)Time elapsed: 0.069 s
% 3.43/1.70 % (3842378)Peak memory usage: 89 MB
% 3.43/1.70 % (3842378)Instructions burned: 139 (million)
% 3.43/1.70 % (3842425)lrs+1011_1_sil=32000:sp=occurrence:random_seed=515907558:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 3.43/1.70 % (3842424)lrs+10_1_sil=32000:urr=on:br=off:random_seed=551609319:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 3.43/1.70 % (3842423)lrs+10_1_sil=8000:sp=occurrence:random_seed=1262433345:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.43/1.70 % (3842426)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=816545664:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 3.43/1.70 % (3842424)Instruction limit reached!
% 3.43/1.70 % (3842424)------------------------------
% 3.43/1.70 % (3842424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.70 % (3842424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.70 % (3842424)CaDiCaL version: 2.1.3
% 3.43/1.70 % (3842424)Termination reason: Instruction limit
% 3.43/1.70 % (3842424)Termination phase: Saturation
% 3.43/1.70 % (3842424)Time elapsed: 0.074 s
% 3.43/1.70 % (3842424)Peak memory usage: 89 MB
% 3.43/1.70 % (3842424)Instructions burned: 158 (million)
% 3.43/1.70 % (3842423)Instruction limit reached!
% 3.43/1.70 % (3842423)------------------------------
% 3.43/1.70 % (3842423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.70 % (3842423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.70 % (3842423)CaDiCaL version: 2.1.3
% 3.43/1.70 % (3842423)Termination reason: Instruction limit
% 3.43/1.70 % (3842423)Termination phase: Saturation
% 3.43/1.70 % (3842423)Time elapsed: 0.129 s
% 3.43/1.70 % (3842423)Peak memory usage: 89 MB
% 3.43/1.70 % (3842423)Instructions burned: 286 (million)
% 3.43/1.70 % (3842426)Instruction limit reached!
% 3.43/1.71 % (3842426)------------------------------
% 3.43/1.71 % (3842426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.71 % (3842426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.71 % (3842426)CaDiCaL version: 2.1.3
% 3.43/1.71 % (3842426)Termination reason: Instruction limit
% 3.43/1.71 % (3842426)Termination phase: Saturation
% 3.43/1.71 % (3842426)Time elapsed: 0.118 s
% 3.43/1.71 % (3842426)Peak memory usage: 89 MB
% 3.43/1.71 % (3842426)Instructions burned: 250 (million)
% 3.43/1.71 % (3842425)Instruction limit reached!
% 3.43/1.71 % (3842425)------------------------------
% 3.43/1.71 % (3842425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.71 % (3842425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.71 % (3842425)CaDiCaL version: 2.1.3
% 3.43/1.71 % (3842425)Termination reason: Instruction limit
% 3.43/1.71 % (3842425)Termination phase: Saturation
% 3.43/1.71 % (3842425)Time elapsed: 0.147 s
% 3.43/1.71 % (3842425)Peak memory usage: 89 MB
% 3.43/1.71 % (3842425)Instructions burned: 326 (million)
% 3.43/1.71 % (3842478)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2563908547:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 3.43/1.71 % (3842479)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1203393983:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 3.43/1.71 % (3842480)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3327179169:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 3.43/1.71 % (3842481)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2278652250:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 3.43/1.71 % (3842481)Refutation not found, incomplete strategy
% 3.43/1.71 % (3842481)------------------------------
% 3.43/1.71 % (3842481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.71 % (3842481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.71 % (3842481)CaDiCaL version: 2.1.3
% 3.43/1.71 % (3842481)Termination reason: Refutation not found, incomplete strategy
% 3.43/1.71 % (3842481)Time elapsed: 0.001 s
% 3.43/1.71 % (3842481)Peak memory usage: 88 MB
% 3.43/1.71 % (3842480)Refutation not found, incomplete strategy
% 3.43/1.71 % (3842480)------------------------------
% 3.43/1.71 % (3842480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.71 % (3842480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.71 % (3842480)CaDiCaL version: 2.1.3
% 3.43/1.71 % (3842480)Termination reason: Refutation not found, incomplete strategy
% 3.43/1.71 % (3842480)Time elapsed: 0.002 s
% 3.43/1.71 % (3842480)Peak memory usage: 88 MB
% 3.43/1.71 % (3842480)Instructions burned: 1 (million)
% 3.43/1.71 % (3842372)First to succeed.
% 3.43/1.71 % (3842478)Instruction limit reached!
% 3.43/1.71 % (3842478)------------------------------
% 3.43/1.71 % (3842478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.71 % (3842478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.71 % (3842478)CaDiCaL version: 2.1.3
% 3.43/1.71 % (3842478)Termination reason: Instruction limit
% 3.43/1.71 % (3842478)Termination phase: Saturation
% 3.43/1.71 % (3842478)Time elapsed: 0.118 s
% 3.43/1.71 % (3842478)Peak memory usage: 88 MB
% 3.43/1.71 % (3842478)Instructions burned: 294 (million)
% 3.43/1.71 % (3842372)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3842271"
% 3.43/1.71 % (3842373)Refutation not found, incomplete strategy
% 3.43/1.71 % (3842373)------------------------------
% 3.43/1.71 % (3842373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.43/1.71 % (3842373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.43/1.71 % (3842373)CaDiCaL version: 2.1.3
% 3.43/1.71 % (3842373)Termination reason: Refutation not found, incomplete strategy
% 3.43/1.71 % (3842373)Time elapsed: 0.606 s
% 3.43/1.71 % (3842373)Peak memory usage: 128 MB
% 3.43/1.71 % (3842373)Instructions burned: 904 (million)
% 3.43/1.71 % (3842486)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=284876268:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 3.43/1.71 % (3842372)Refutation found. Thanks to Tanya!
% 3.43/1.71 % SZS status Theorem for theBenchmark
% 3.43/1.71 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/1.90 % (3842372)------------------------------
% 0.18/1.90 % (3842372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/1.90 % (3842372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/1.90 % (3842372)CaDiCaL version: 2.1.3
% 0.18/1.90 % (3842372)Termination reason: Refutation
% 0.18/1.90 % (3842372)Time elapsed: 0.550 s
% 0.18/1.90 % (3842372)Peak memory usage: 132 MB
% 0.18/1.90 % (3842372)Instructions burned: 1635 (million)
% 0.18/1.90 % (3842372)------------------------------
% 0.18/1.90 % (3842372)------------------------------
% 0.18/1.90 % (3842271)Success in time 0.819 s
% 0.18/1.90 % Vampire exiting
%------------------------------------------------------------------------------