%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PUZ134_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n002.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 : Sun Sep 27 08:21:25 AM UTC 2026
% Result : Theorem 110.58s 28.93s
% Output : Refutation 111.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 39
% Syntax : Number of formulae : 696 ( 161 unt; 0 typ; 3 def)
% Number of atoms : 2566 (1498 equ; 0 cnn)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 6888 (1410 ~;1381 |; 25 &;4053 @)
% ( 1 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 4 ( 4 >; 0 *; 0 +; 0 <<)
% Number of symbols : 19 ( 16 usr; 13 con; 0-2 aty)
% Number of variables : 788 ( 0 ^; 777 !; 8 ?; 788 :)
% ( 0 !>; 0 ?*; 0 @-; 3 @+)
% Comments :
%------------------------------------------------------------------------------
thf(knowheyan_type,type,
knowheyan: $tType ).
thf(job_type,type,
job: $tType ).
thf(age_type,type,
age: $tType ).
thf(age_of_decl,type,
age_of: knowheyan > age ).
thf(job_of_decl,type,
job_of: knowheyan > job ).
thf(greater_decl,type,
greater: age > age > $o ).
thf(a_decl,type,
a: knowheyan ).
thf(b_decl,type,
b: knowheyan ).
thf(c_decl,type,
c: knowheyan ).
thf(d_decl,type,
d: knowheyan ).
thf(e_decl,type,
e: knowheyan ).
thf(airfoil_technician_decl,type,
airfoil_technician: job ).
thf(communications_consultant_decl,type,
communications_consultant: job ).
thf(space_planner_decl,type,
space_planner: job ).
thf(lunar_energy_engineer_decl,type,
lunar_energy_engineer: job ).
thf(synthetic_food_nutitionist_decl,type,
synthetic_food_nutitionist: job ).
thf(sk1_decl,type,
sk1: age > knowheyan ).
thf(sk2_decl,type,
sk2: job > knowheyan ).
thf(sk3_decl,type,
sk3: knowheyan ).
thf(sk1_def,definition,
( sk1
= ( @+[A: age > knowheyan] :
! [B: knowheyan] :
( ( B @ age_of @ A )
= B ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: job > knowheyan] :
! [B: knowheyan] :
( ( B @ job_of @ A )
= B ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: knowheyan] : ( A @ age_of @ ( c @ age_of @ greater ) ) ) ) ).
thf(3,axiom,
! [A: knowheyan,B: knowheyan] :
( ( A != B )
=> ( ( A @ age_of )
!= ( B @ age_of ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_ages) ).
thf(41,plain,
! [A: knowheyan,B: knowheyan] :
( ( A != B )
=> ( ( A @ age_of )
!= ( B @ age_of ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(20,axiom,
d != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_not_e) ).
thf(99,plain,
d != e,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(100,plain,
d != e,
inference(polarity_switch,[status(thm)],[99]) ).
thf(101,plain,
e != d,
inference(lifteq,[status(thm)],[100]) ).
thf(19,axiom,
! [A: knowheyan,B: knowheyan] :
( ( A != B )
=> ( ( A @ job_of )
!= ( B @ job_of ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_jobs) ).
thf(94,plain,
! [A: knowheyan,B: knowheyan] :
( ( A != B )
=> ( ( A @ job_of )
!= ( B @ job_of ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(95,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( A @ job_of )
!= ( B @ job_of ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[94]) ).
thf(96,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( A @ job_of )
!= ( B @ job_of ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[95]) ).
thf(97,plain,
? [A: job > knowheyan] :
! [B: knowheyan] :
( ( B @ job_of @ A )
= B ),
inference(detectInverse,[status(thm)],[96]) ).
thf(98,plain,
! [A: knowheyan] :
( ( A @ job_of @ sk2 )
= A ),
inference(cnf,[status(esa)],[97]) ).
thf(231,plain,
! [A: knowheyan] :
( ( A @ job_of @ sk2 )
= A ),
inference(lifteq,[status(thm)],[98]) ).
thf(10,axiom,
! [A: job] :
( ( A = synthetic_food_nutitionist )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_jobs) ).
thf(71,plain,
! [A: job] :
( ( A = synthetic_food_nutitionist )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(72,plain,
! [A: job] :
( ( A = synthetic_food_nutitionist )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(cnf,[status(esa)],[71]) ).
thf(73,plain,
! [A: job] :
( ( A = synthetic_food_nutitionist )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(lifteq,[status(thm)],[72]) ).
thf(484,plain,
! [B: knowheyan,A: job] :
( ( A
!= ( B @ job_of ) )
| ( ( synthetic_food_nutitionist @ sk2 )
= B )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[73,231]) ).
thf(485,plain,
! [A: knowheyan] :
( ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= lunar_energy_engineer )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[484:[bind(A,$thf( C @ job_of )),bind(B,$thf( C ))]]) ).
thf(505,plain,
! [A: knowheyan] :
( ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= lunar_energy_engineer )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[485]) ).
thf(12,axiom,
! [A: knowheyan] :
( ( ( A @ job_of )
= lunar_energy_engineer )
=> ( b @ age_of @ ( A @ age_of @ greater ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info3) ).
thf(75,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
= lunar_energy_engineer )
=> ( b @ age_of @ ( A @ age_of @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(76,plain,
! [A: knowheyan] :
( ( b @ age_of @ ( A @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(cnf,[status(esa)],[75]) ).
thf(77,plain,
! [A: knowheyan] :
( ( b @ age_of @ ( A @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(lifteq,[status(thm)],[76]) ).
thf(5,axiom,
! [A: age,B: age] :
( ( A != B )
<=> ( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_greater) ).
thf(48,plain,
! [A: age,B: age] :
( ( ( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) )
=> ( A != B ) )
& ( ( A != B )
=> ( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(49,plain,
( ! [A: age,B: age] :
( ( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) )
=> ( A != B ) )
& ! [A: age,B: age] :
( ( A != B )
=> ( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ) ) ),
inference(miniscope,[status(thm)],[48]) ).
thf(50,plain,
! [D: age,C: age,B: age,A: age] :
( ( ( C != D )
| ~ ( C @ ( D @ greater ) ) )
& ( ( C != D )
| ~ ( D @ ( C @ greater ) ) )
& ( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(52,plain,
! [B: age,A: age] :
( ( A != B )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(55,plain,
! [B: age,A: age] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(56,plain,
! [A: age] :
~ ( A @ ( A @ greater ) ),
inference(simp,[status(thm)],[55]) ).
thf(648,plain,
! [B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( B @ ( B @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,56]) ).
thf(649,plain,
! [B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( B @ ( B @ greater ) ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[648]) ).
thf(650,plain,
( ( b @ job_of )
!= lunar_energy_engineer ),
inference(pattern_uni,[status(thm)],[649:[bind(A,$thf( b )),bind(B,$thf( b @ age_of ))]]) ).
thf(19948,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( b @ job_of ) )
| ( lunar_energy_engineer != lunar_energy_engineer )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[505,650]) ).
thf(19949,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( b @ job_of ) )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[19948]) ).
thf(19950,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
= b )
| ( ( b @ job_of )
= space_planner )
| ( ( b @ job_of )
= communications_consultant )
| ( ( b @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[19949:[bind(A,$thf( b ))]]) ).
thf(37,axiom,
b @ age_of @ ( d @ age_of @ greater ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info2) ).
thf(149,plain,
b @ age_of @ ( d @ age_of @ greater ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(25,axiom,
! [A: knowheyan] :
( ( ( A @ job_of )
= communications_consultant )
=> ~ ? [B: knowheyan] : ( A @ age_of @ ( B @ age_of @ greater ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_younger) ).
thf(114,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
= communications_consultant )
=> ~ ? [B: knowheyan] : ( A @ age_of @ ( B @ age_of @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(115,plain,
! [B: knowheyan,A: knowheyan] :
( ~ ( A @ age_of @ ( B @ age_of @ greater ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(cnf,[status(esa)],[114]) ).
thf(116,plain,
! [B: knowheyan,A: knowheyan] :
( ~ ( A @ age_of @ ( B @ age_of @ greater ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(lifteq,[status(thm)],[115]) ).
thf(221,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[149,116]) ).
thf(222,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[221]) ).
thf(223,plain,
( ( b @ job_of )
!= communications_consultant ),
inference(pattern_uni,[status(thm)],[222:[bind(A,$thf( b )),bind(B,$thf( d ))]]) ).
thf(41057,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
= b )
| ( ( b @ job_of )
= space_planner )
| ( ( b @ job_of )
= airfoil_technician ) ),
inference(simplifyReflect,[status(thm)],[19950,223]) ).
thf(41266,plain,
! [A: knowheyan] :
( ( ( b @ job_of )
!= ( A @ job_of ) )
| ( ( space_planner @ sk2 )
= A )
| ( ( synthetic_food_nutitionist @ sk2 )
= b )
| ( ( b @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[41057,231]) ).
thf(41267,plain,
( ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b )
| ( ( b @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[41266:[bind(A,$thf( b ))]]) ).
thf(22,axiom,
! [A: knowheyan] :
( ( A = e )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_knowheyans) ).
thf(105,plain,
! [A: knowheyan] :
( ( A = e )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(106,plain,
! [A: knowheyan] :
( ( A = e )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
inference(cnf,[status(esa)],[105]) ).
thf(107,plain,
! [A: knowheyan] :
( ( A = e )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
inference(lifteq,[status(thm)],[106]) ).
thf(1,conjecture,
( ( ( e @ job_of )
= synthetic_food_nutitionist )
& ( ( c @ job_of )
= space_planner )
& ( ( b @ job_of )
= airfoil_technician )
& ( ( d @ job_of )
= lunar_energy_engineer )
& ( ( a @ job_of )
= communications_consultant ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',known_jobs) ).
thf(2,negated_conjecture,
~ ( ( ( e @ job_of )
= synthetic_food_nutitionist )
& ( ( c @ job_of )
= space_planner )
& ( ( b @ job_of )
= airfoil_technician )
& ( ( d @ job_of )
= lunar_energy_engineer )
& ( ( a @ job_of )
= communications_consultant ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(38,plain,
~ ( ( ( e @ job_of )
= synthetic_food_nutitionist )
& ( ( c @ job_of )
= space_planner )
& ( ( b @ job_of )
= airfoil_technician )
& ( ( d @ job_of )
= lunar_energy_engineer )
& ( ( a @ job_of )
= communications_consultant ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(39,plain,
( ( ( e @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(cnf,[status(esa)],[38]) ).
thf(40,plain,
( ( ( e @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(lifteq,[status(thm)],[39]) ).
thf(495,plain,
! [A: job] :
( ( A
!= ( e @ job_of ) )
| ( synthetic_food_nutitionist != synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[73,40]) ).
thf(496,plain,
! [A: job] :
( ( A
!= ( e @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(simp,[status(thm)],[495]) ).
thf(497,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= lunar_energy_engineer )
| ( ( e @ job_of )
= space_planner )
| ( ( e @ job_of )
= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[496:[bind(A,$thf( e @ job_of ))]]) ).
thf(29,axiom,
? [A: knowheyan] : ( A @ age_of @ ( c @ age_of @ greater ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_youngest) ).
thf(126,plain,
? [A: knowheyan] : ( A @ age_of @ ( c @ age_of @ greater ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(127,plain,
sk3 @ age_of @ ( c @ age_of @ greater ),
inference(cnf,[status(esa)],[126]) ).
thf(4,axiom,
! [A: age,B: age,C: age] :
( ( ( C @ ( B @ greater ) )
& ( B @ ( A @ greater ) ) )
=> ( C @ ( A @ greater ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_transitive) ).
thf(46,plain,
! [A: age,B: age,C: age] :
( ( ( C @ ( B @ greater ) )
& ( B @ ( A @ greater ) ) )
=> ( C @ ( A @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(47,plain,
! [C: age,B: age,A: age] :
( ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(11,axiom,
c @ age_of @ ( b @ age_of @ greater ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info4) ).
thf(74,plain,
c @ age_of @ ( b @ age_of @ greater ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(6,axiom,
! [A: age,B: age] :
~ ( ( A @ ( B @ greater ) )
& ( B @ ( A @ greater ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_irreflexive) ).
thf(59,plain,
! [A: age,B: age] :
~ ( ( A @ ( B @ greater ) )
& ( B @ ( A @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(60,plain,
~ ? [A: age,B: age] :
( ( A @ ( B @ greater ) )
& ( B @ ( A @ greater ) ) ),
inference(miniscope,[status(thm)],[59]) ).
thf(61,plain,
! [B: age,A: age] :
( ~ ( A @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[60]) ).
thf(365,plain,
! [B: age,A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[74,61]) ).
thf(366,plain,
! [B: age,A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[365]) ).
thf(367,plain,
~ ( b @ age_of @ ( c @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[366:[bind(A,$thf( b @ age_of )),bind(B,$thf( c @ age_of ))]]) ).
thf(404,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,367]) ).
thf(405,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[404]) ).
thf(406,plain,
! [A: age] :
( ~ ( b @ age_of @ ( A @ greater ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[405:[bind(A,$thf( c @ age_of )),bind(B,$thf( B )),bind(C,$thf( b @ age_of ))]]) ).
thf(434,plain,
! [A: age] :
( ~ ( b @ age_of @ ( A @ greater ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[406]) ).
thf(994,plain,
! [A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ~ ( b @ age_of @ ( A @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[127,434]) ).
thf(995,plain,
! [A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ~ ( b @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[994]) ).
thf(996,plain,
~ ( b @ age_of @ ( sk3 @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[995:[bind(A,$thf( sk3 @ age_of ))]]) ).
thf(1329,plain,
! [A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,996]) ).
thf(1330,plain,
! [A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[1329]) ).
thf(1331,plain,
( ( sk3 @ job_of )
!= lunar_energy_engineer ),
inference(pattern_uni,[status(thm)],[1330:[bind(A,$thf( sk3 ))]]) ).
thf(1367,plain,
( ( ( sk3 @ job_of )
!= ( e @ job_of ) )
| ( lunar_energy_engineer != lunar_energy_engineer )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= space_planner )
| ( ( e @ job_of )
= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[497,1331]) ).
thf(1368,plain,
( ( ( sk3 @ job_of )
!= ( e @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= space_planner )
| ( ( e @ job_of )
= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[1367]) ).
thf(1373,plain,
( ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= space_planner )
| ( ( e @ job_of )
= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[1368]) ).
thf(5055,plain,
! [A: knowheyan] :
( ( ( e @ job_of )
!= ( A @ job_of ) )
| ( ( space_planner @ sk2 )
= A )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[1373,231]) ).
thf(5056,plain,
( ( ( space_planner @ sk2 )
= e )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[5055:[bind(A,$thf( e ))]]) ).
thf(224,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[127,116]) ).
thf(225,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[224]) ).
thf(226,plain,
( ( sk3 @ job_of )
!= communications_consultant ),
inference(pattern_uni,[status(thm)],[225:[bind(A,$thf( sk3 )),bind(B,$thf( c ))]]) ).
thf(8515,plain,
( ( ( sk3 @ job_of )
!= ( e @ job_of ) )
| ( communications_consultant != communications_consultant )
| ( ( space_planner @ sk2 )
= e )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[5056,226]) ).
thf(8516,plain,
( ( ( sk3 @ job_of )
!= ( e @ job_of ) )
| ( ( space_planner @ sk2 )
= e )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[8515]) ).
thf(8712,plain,
( ( sk3 != e )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= e )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[8516]) ).
thf(8720,plain,
( ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= e )
| ( ( e @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[8712]) ).
thf(26,axiom,
! [A: knowheyan,B: knowheyan] :
( ( ( ( B @ job_of )
= space_planner )
& ( ( A @ job_of )
= airfoil_technician ) )
=> ( B @ age_of @ ( A @ age_of @ greater ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_job1) ).
thf(117,plain,
! [A: knowheyan,B: knowheyan] :
( ( ( ( B @ job_of )
= space_planner )
& ( ( A @ job_of )
= airfoil_technician ) )
=> ( B @ age_of @ ( A @ age_of @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(118,plain,
! [B: knowheyan,A: knowheyan] :
( ( B @ age_of @ ( A @ age_of @ greater ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(cnf,[status(esa)],[117]) ).
thf(119,plain,
! [B: knowheyan,A: knowheyan] :
( ( B @ age_of @ ( A @ age_of @ greater ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(lifteq,[status(thm)],[118]) ).
thf(389,plain,
! [B: age,A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[127,61]) ).
thf(390,plain,
! [B: age,A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[389]) ).
thf(391,plain,
~ ( c @ age_of @ ( sk3 @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[390:[bind(A,$thf( c @ age_of )),bind(B,$thf( sk3 @ age_of ))]]) ).
thf(1494,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,391]) ).
thf(1495,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1494]) ).
thf(1496,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( sk3 @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1495:[bind(A,$thf( sk3 )),bind(B,$thf( c ))]]) ).
thf(8930,plain,
( ( ( sk3 @ job_of )
!= ( e @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( airfoil_technician != airfoil_technician )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= e ) ),
inference(paramod_ordered,[status(thm)],[8720,1496]) ).
thf(8931,plain,
( ( ( sk3 @ job_of )
!= ( e @ job_of ) )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= e ) ),
inference(simp,[status(thm)],[8930]) ).
thf(9060,plain,
( ( sk3 != e )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= e ) ),
inference(simp,[status(thm)],[8931]) ).
thf(9153,plain,
( ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= e ) ),
inference(simp,[status(thm)],[9060]) ).
thf(9529,plain,
! [A: knowheyan] :
( ( ( A @ job_of @ sk2 )
!= ( space_planner @ sk2 ) )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = e ) ),
inference(paramod_ordered,[status(thm)],[231,9153]) ).
thf(9550,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= space_planner )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = e ) ),
inference(simp,[status(thm)],[9529]) ).
thf(13252,plain,
! [A: knowheyan] :
( ( space_planner != space_planner )
| ( ( A @ job_of )
!= ( c @ job_of ) )
| ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = e ) ),
inference(eqfactor_ordered,[status(thm)],[9550]) ).
thf(13265,plain,
( ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( e = c ) ),
inference(pattern_uni,[status(thm)],[13252:[bind(A,$thf( c ))]]) ).
thf(13,axiom,
c != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_e) ).
thf(78,plain,
c != e,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(79,plain,
c != e,
inference(polarity_switch,[status(thm)],[78]) ).
thf(80,plain,
e != c,
inference(lifteq,[status(thm)],[79]) ).
thf(13287,plain,
( ( sk3 != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simplifyReflect,[status(thm)],[13265,80]) ).
thf(13329,plain,
! [A: knowheyan] :
( ( A != sk3 )
| ( e != e )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
inference(paramod_ordered,[status(thm)],[107,13287]) ).
thf(13330,plain,
! [A: knowheyan] :
( ( A != sk3 )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
inference(simp,[status(thm)],[13329]) ).
thf(13331,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( sk3 = d )
| ( sk3 = c )
| ( sk3 = b )
| ( sk3 = a ) ),
inference(pattern_uni,[status(thm)],[13330:[bind(A,$thf( sk3 ))]]) ).
thf(425,plain,
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[127,367]) ).
thf(426,plain,
( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[425]) ).
thf(431,plain,
( ( ( sk3 @ age_of )
!= ( b @ age_of ) )
| ( ( c @ age_of )
!= ( c @ age_of ) ) ),
inference(simp,[status(thm)],[426]) ).
thf(438,plain,
( ( sk3 @ age_of )
!= ( b @ age_of ) ),
inference(simp,[status(thm)],[431]) ).
thf(448,plain,
sk3 != b,
inference(simp,[status(thm)],[438]) ).
thf(179,plain,
! [C: age,B: age,A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ $true
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[74,47]) ).
thf(180,plain,
! [C: age,B: age,A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[179]) ).
thf(181,plain,
! [A: age] :
( ( c @ age_of @ ( A @ greater ) )
| ~ ( b @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[180:[bind(A,$thf( A )),bind(B,$thf( b @ age_of )),bind(C,$thf( c @ age_of ))]]) ).
thf(2269,plain,
! [A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( b @ age_of @ ( A @ greater ) ) )
| ( c @ age_of @ ( A @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[149,181]) ).
thf(2270,plain,
! [A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( b @ age_of @ ( A @ greater ) ) )
| ( c @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2269]) ).
thf(2271,plain,
c @ age_of @ ( d @ age_of @ greater ),
inference(pattern_uni,[status(thm)],[2270:[bind(A,$thf( d @ age_of ))]]) ).
thf(185,plain,
! [C: age,B: age,A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ $true
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[127,47]) ).
thf(186,plain,
! [C: age,B: age,A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(187,plain,
! [A: age] :
( ( sk3 @ age_of @ ( A @ greater ) )
| ~ ( c @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[186:[bind(A,$thf( A )),bind(B,$thf( c @ age_of )),bind(C,$thf( sk3 @ age_of ))]]) ).
thf(2594,plain,
! [A: age] :
( ( ( c @ age_of @ ( d @ age_of @ greater ) )
!= ( c @ age_of @ ( A @ greater ) ) )
| ( sk3 @ age_of @ ( A @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2271,187]) ).
thf(2595,plain,
! [A: age] :
( ( ( c @ age_of @ ( d @ age_of @ greater ) )
!= ( c @ age_of @ ( A @ greater ) ) )
| ( sk3 @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2594]) ).
thf(2596,plain,
sk3 @ age_of @ ( d @ age_of @ greater ),
inference(pattern_uni,[status(thm)],[2595:[bind(A,$thf( d @ age_of ))]]) ).
thf(17,axiom,
d @ age_of @ ( a @ age_of @ greater ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_info1) ).
thf(90,plain,
d @ age_of @ ( a @ age_of @ greater ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(395,plain,
! [B: age,A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[90,61]) ).
thf(396,plain,
! [B: age,A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[395]) ).
thf(397,plain,
~ ( a @ age_of @ ( d @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[396:[bind(A,$thf( a @ age_of )),bind(B,$thf( d @ age_of ))]]) ).
thf(2661,plain,
( ( ( sk3 @ age_of @ ( d @ age_of @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2596,397]) ).
thf(2662,plain,
( ( sk3 @ age_of @ ( d @ age_of @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[2661]) ).
thf(2713,plain,
( ( ( sk3 @ age_of )
!= ( a @ age_of ) )
| ( ( d @ age_of )
!= ( d @ age_of ) ) ),
inference(simp,[status(thm)],[2662]) ).
thf(2724,plain,
( ( sk3 @ age_of )
!= ( a @ age_of ) ),
inference(simp,[status(thm)],[2713]) ).
thf(2729,plain,
sk3 != a,
inference(simp,[status(thm)],[2724]) ).
thf(161,plain,
! [A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[127,56]) ).
thf(162,plain,
! [A: age] :
( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[161]) ).
thf(163,plain,
! [A: age] :
( ( ( sk3 @ age_of )
!= A )
| ( ( c @ age_of )
!= A ) ),
inference(simp,[status(thm)],[162]) ).
thf(164,plain,
( ( sk3 @ age_of )
!= ( c @ age_of ) ),
inference(simp,[status(thm)],[163]) ).
thf(202,plain,
sk3 != c,
inference(simp,[status(thm)],[164]) ).
thf(971,plain,
! [A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( b @ age_of @ ( A @ greater ) ) )
| ~ $true
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[149,434]) ).
thf(972,plain,
! [A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( b @ age_of @ ( A @ greater ) ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[971]) ).
thf(973,plain,
~ ( d @ age_of @ ( c @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[972:[bind(A,$thf( d @ age_of ))]]) ).
thf(1050,plain,
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[127,973]) ).
thf(1051,plain,
( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[1050]) ).
thf(1057,plain,
( ( ( sk3 @ age_of )
!= ( d @ age_of ) )
| ( ( c @ age_of )
!= ( c @ age_of ) ) ),
inference(simp,[status(thm)],[1051]) ).
thf(1063,plain,
( ( sk3 @ age_of )
!= ( d @ age_of ) ),
inference(simp,[status(thm)],[1057]) ).
thf(1310,plain,
sk3 != d,
inference(simp,[status(thm)],[1063]) ).
thf(13344,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simplifyReflect,[status(thm)],[13331,448,2729,202,1310]) ).
thf(41494,plain,
( ( ( b @ job_of )
!= ( b @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( airfoil_technician != airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(paramod_ordered,[status(thm)],[41267,13344]) ).
thf(41495,plain,
( ( ( b @ job_of )
!= ( b @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(simp,[status(thm)],[41494]) ).
thf(41496,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(pattern_uni,[status(thm)],[41495:[]]) ).
thf(42004,plain,
( ( b != b )
| ( ( synthetic_food_nutitionist @ sk2 )
!= ( space_planner @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b ) ),
inference(eqfactor_ordered,[status(thm)],[41496]) ).
thf(42006,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
!= ( space_planner @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b ) ),
inference(simp,[status(thm)],[42004]) ).
thf(42703,plain,
! [A: knowheyan] :
( ( ( A @ job_of @ sk2 )
!= ( synthetic_food_nutitionist @ sk2 ) )
| ( A
!= ( space_planner @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b ) ),
inference(paramod_ordered,[status(thm)],[231,42006]) ).
thf(42735,plain,
( ( ( space_planner @ sk2 @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( space_planner @ sk2 )
= b ) ),
inference(simp,[status(thm)],[42703]) ).
thf(20189,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( sk3 @ job_of ) )
| ( lunar_energy_engineer != lunar_energy_engineer )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[505,1331]) ).
thf(20190,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( sk3 @ job_of ) )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[20189]) ).
thf(20191,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
= sk3 )
| ( ( sk3 @ job_of )
= space_planner )
| ( ( sk3 @ job_of )
= communications_consultant )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[20190:[bind(A,$thf( sk3 ))]]) ).
thf(43378,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
= sk3 )
| ( ( sk3 @ job_of )
= space_planner )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(simplifyReflect,[status(thm)],[20191,226]) ).
thf(19957,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( d @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( lunar_energy_engineer != lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[505,13344]) ).
thf(19958,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( d @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[19957]) ).
thf(19959,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( d @ job_of )
= space_planner )
| ( ( d @ job_of )
= communications_consultant )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[19958:[bind(A,$thf( d ))]]) ).
thf(227,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[90,116]) ).
thf(228,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[227]) ).
thf(229,plain,
( ( d @ job_of )
!= communications_consultant ),
inference(pattern_uni,[status(thm)],[228:[bind(A,$thf( d )),bind(B,$thf( a ))]]) ).
thf(20223,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( d @ job_of )
= space_planner )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(simplifyReflect,[status(thm)],[19959,229]) ).
thf(371,plain,
! [B: age,A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[149,61]) ).
thf(372,plain,
! [B: age,A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(373,plain,
~ ( d @ age_of @ ( b @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[372:[bind(A,$thf( d @ age_of )),bind(B,$thf( b @ age_of ))]]) ).
thf(1462,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,373]) ).
thf(1463,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1462]) ).
thf(1464,plain,
( ( ( d @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1463:[bind(A,$thf( b )),bind(B,$thf( d ))]]) ).
thf(20317,plain,
( ( ( d @ job_of )
!= ( d @ job_of ) )
| ( space_planner != space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[20223,1464]) ).
thf(20318,plain,
( ( ( d @ job_of )
!= ( d @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[20317]) ).
thf(20319,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[20318:[]]) ).
thf(20540,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( d @ job_of )
!= ( B @ job_of ) )
| ( ( A @ job_of )
!= airfoil_technician )
| ( A = B )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(paramod_ordered,[status(thm)],[20319,96]) ).
thf(20541,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= airfoil_technician )
| ( A = d )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(pattern_uni,[status(thm)],[20540:[bind(A,$thf( A )),bind(B,$thf( d ))]]) ).
thf(31965,plain,
! [A: knowheyan] :
( ( airfoil_technician != airfoil_technician )
| ( ( A @ job_of )
!= ( b @ job_of ) )
| ( A = d )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(eqfactor_ordered,[status(thm)],[20541]) ).
thf(31969,plain,
( ( d = b )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(pattern_uni,[status(thm)],[31965:[bind(A,$thf( b ))]]) ).
thf(24,axiom,
b != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_d) ).
thf(111,plain,
b != d,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(112,plain,
b != d,
inference(polarity_switch,[status(thm)],[111]) ).
thf(113,plain,
d != b,
inference(lifteq,[status(thm)],[112]) ).
thf(31992,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(simplifyReflect,[status(thm)],[31969,113]) ).
thf(43391,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
!= ( synthetic_food_nutitionist @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( sk3 = d )
| ( ( sk3 @ job_of )
= space_planner )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[43378,31992]) ).
thf(43392,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( sk3 = d )
| ( ( sk3 @ job_of )
= space_planner )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[43391:[]]) ).
thf(51309,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( sk3 @ job_of )
= space_planner )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(simplifyReflect,[status(thm)],[43392,1310]) ).
thf(51638,plain,
! [A: knowheyan] :
( ( ( sk3 @ job_of )
!= ( A @ job_of ) )
| ( ( space_planner @ sk2 )
= A )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[51309,231]) ).
thf(51639,plain,
( ( ( space_planner @ sk2 )
= sk3 )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[51638:[bind(A,$thf( sk3 ))]]) ).
thf(52253,plain,
( ( ( sk3 @ job_of )
!= ( sk3 @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( airfoil_technician != airfoil_technician )
| ( ( space_planner @ sk2 )
= sk3 )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[51639,1496]) ).
thf(52254,plain,
( ( ( sk3 @ job_of )
!= ( sk3 @ job_of ) )
| ( ( space_planner @ sk2 )
= sk3 )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[52253]) ).
thf(52255,plain,
( ( ( space_planner @ sk2 )
= sk3 )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(pattern_uni,[status(thm)],[52254:[]]) ).
thf(637,plain,
! [A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,367]) ).
thf(638,plain,
! [A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[637]) ).
thf(639,plain,
( ( c @ job_of )
!= lunar_energy_engineer ),
inference(pattern_uni,[status(thm)],[638:[bind(A,$thf( c ))]]) ).
thf(20194,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( c @ job_of ) )
| ( lunar_energy_engineer != lunar_energy_engineer )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[505,639]) ).
thf(20195,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= ( c @ job_of ) )
| ( ( synthetic_food_nutitionist @ sk2 )
= A )
| ( ( A @ job_of )
= space_planner )
| ( ( A @ job_of )
= communications_consultant )
| ( ( A @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[20194]) ).
thf(20196,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= space_planner )
| ( ( c @ job_of )
= communications_consultant )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[20195:[bind(A,$thf( c ))]]) ).
thf(218,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[74,116]) ).
thf(219,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[218]) ).
thf(220,plain,
( ( c @ job_of )
!= communications_consultant ),
inference(pattern_uni,[status(thm)],[219:[bind(A,$thf( c )),bind(B,$thf( b ))]]) ).
thf(44492,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= space_planner )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(simplifyReflect,[status(thm)],[20196,220]) ).
thf(44756,plain,
! [A: knowheyan] :
( ( ( c @ job_of )
!= ( A @ job_of ) )
| ( ( space_planner @ sk2 )
= A )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[44492,231]) ).
thf(44757,plain,
( ( ( space_planner @ sk2 )
= c )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[44756:[bind(A,$thf( c ))]]) ).
thf(51,plain,
! [B: age,A: age] :
( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(54,plain,
! [B: age,A: age] :
( ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(42,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( A @ age_of )
!= ( B @ age_of ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[41]) ).
thf(43,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( A @ age_of )
!= ( B @ age_of ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[42]) ).
thf(240,plain,
! [D: knowheyan,C: knowheyan,B: age,A: age] :
( ( A
!= ( C @ age_of ) )
| ( B
!= ( D @ age_of ) )
| ( C = D )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,43]) ).
thf(241,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ( A
!= ( B @ age_of ) )
| ( C = B )
| ( C @ age_of @ ( A @ greater ) )
| ( A @ ( C @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[240:[bind(A,$thf( E @ age_of )),bind(B,$thf( B )),bind(C,$thf( E ))]]) ).
thf(346,plain,
! [B: knowheyan,A: knowheyan] :
( ( B = A )
| ( B @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( B @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[241]) ).
thf(15,axiom,
a != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_e) ).
thf(84,plain,
a != e,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(85,plain,
a != e,
inference(polarity_switch,[status(thm)],[84]) ).
thf(86,plain,
e != a,
inference(lifteq,[status(thm)],[85]) ).
thf(14648,plain,
! [B: knowheyan,A: knowheyan] :
( ( B != e )
| ( A != a )
| ( B @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( B @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[346,86]) ).
thf(14649,plain,
! [A: knowheyan] :
( ( A != a )
| ( e @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( e @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[14648:[bind(A,$thf( A )),bind(B,$thf( e ))]]) ).
thf(15202,plain,
( ( e @ age_of @ ( a @ age_of @ greater ) )
| ( a @ age_of @ ( e @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[14649]) ).
thf(191,plain,
! [C: age,B: age,A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ $true
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[90,47]) ).
thf(192,plain,
! [C: age,B: age,A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[191]) ).
thf(193,plain,
! [A: age] :
( ( d @ age_of @ ( A @ greater ) )
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[192:[bind(A,$thf( A )),bind(B,$thf( a @ age_of )),bind(C,$thf( d @ age_of ))]]) ).
thf(24662,plain,
! [A: age] :
( ( ( a @ age_of @ ( e @ age_of @ greater ) )
!= ( a @ age_of @ ( A @ greater ) ) )
| ( d @ age_of @ ( A @ greater ) )
| ~ $true
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[15202,193]) ).
thf(24663,plain,
! [A: age] :
( ( ( a @ age_of @ ( e @ age_of @ greater ) )
!= ( a @ age_of @ ( A @ greater ) ) )
| ( d @ age_of @ ( A @ greater ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[24662]) ).
thf(24664,plain,
( ( d @ age_of @ ( e @ age_of @ greater ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[24663:[bind(A,$thf( e @ age_of ))]]) ).
thf(206,plain,
! [C: age,B: age,A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ $true
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[149,47]) ).
thf(207,plain,
! [C: age,B: age,A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[206]) ).
thf(208,plain,
! [A: age] :
( ( b @ age_of @ ( A @ greater ) )
| ~ ( d @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[207:[bind(A,$thf( A )),bind(B,$thf( d @ age_of )),bind(C,$thf( b @ age_of ))]]) ).
thf(34492,plain,
! [A: age] :
( ( ( d @ age_of @ ( e @ age_of @ greater ) )
!= ( d @ age_of @ ( A @ greater ) ) )
| ( b @ age_of @ ( A @ greater ) )
| ~ $true
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[24664,208]) ).
thf(34493,plain,
! [A: age] :
( ( ( d @ age_of @ ( e @ age_of @ greater ) )
!= ( d @ age_of @ ( A @ greater ) ) )
| ( b @ age_of @ ( A @ greater ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[34492]) ).
thf(34494,plain,
( ( b @ age_of @ ( e @ age_of @ greater ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[34493:[bind(A,$thf( e @ age_of ))]]) ).
thf(36826,plain,
! [A: age] :
( ( ( b @ age_of @ ( e @ age_of @ greater ) )
!= ( b @ age_of @ ( A @ greater ) ) )
| ( c @ age_of @ ( A @ greater ) )
| ~ $true
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[34494,181]) ).
thf(36827,plain,
! [A: age] :
( ( ( b @ age_of @ ( e @ age_of @ greater ) )
!= ( b @ age_of @ ( A @ greater ) ) )
| ( c @ age_of @ ( A @ greater ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[36826]) ).
thf(36828,plain,
( ( c @ age_of @ ( e @ age_of @ greater ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[36827:[bind(A,$thf( e @ age_of ))]]) ).
thf(913,plain,
! [A: knowheyan] :
( ( A != sk3 )
| ( e @ age_of @ ( c @ age_of @ greater ) )
| ( A = d )
| ( A = c )
| ( A = b )
| ( A = a ) ),
inference(paramod_ordered,[status(thm)],[107,127]) ).
thf(914,plain,
( ( e @ age_of @ ( c @ age_of @ greater ) )
| ( sk3 = d )
| ( sk3 = c )
| ( sk3 = b )
| ( sk3 = a ) ),
inference(pattern_uni,[status(thm)],[913:[bind(A,$thf( sk3 ))]]) ).
thf(47048,plain,
e @ age_of @ ( c @ age_of @ greater ),
inference(simplifyReflect,[status(thm)],[914,448,2729,202,1310]) ).
thf(47083,plain,
! [B: age,A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47048,61]) ).
thf(47084,plain,
! [B: age,A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[47083]) ).
thf(47085,plain,
~ ( c @ age_of @ ( e @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[47084:[bind(A,$thf( c @ age_of )),bind(B,$thf( e @ age_of ))]]) ).
thf(47793,plain,
( $false
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(rewrite,[status(thm)],[36828,47085]) ).
thf(47794,plain,
e @ age_of @ ( a @ age_of @ greater ),
inference(simp,[status(thm)],[47793]) ).
thf(27,axiom,
a != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_d) ).
thf(120,plain,
a != d,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(651,plain,
! [C: age,B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( B @ ( C @ greater ) )
| ~ $true
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,61]) ).
thf(652,plain,
! [C: age,B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( B @ ( C @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[651]) ).
thf(653,plain,
! [A: knowheyan] :
( ~ ( A @ age_of @ ( b @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(pattern_uni,[status(thm)],[652:[bind(A,$thf( D )),bind(B,$thf( D @ age_of )),bind(C,$thf( b @ age_of ))]]) ).
thf(677,plain,
! [A: knowheyan] :
( ~ ( A @ age_of @ ( b @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[653]) ).
thf(34,axiom,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_b) ).
thf(140,plain,
a != b,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(141,plain,
a != b,
inference(polarity_switch,[status(thm)],[140]) ).
thf(142,plain,
b != a,
inference(lifteq,[status(thm)],[141]) ).
thf(1505,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,996]) ).
thf(1506,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1505]) ).
thf(1507,plain,
( ( ( b @ job_of )
!= space_planner )
| ( ( sk3 @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1506:[bind(A,$thf( sk3 )),bind(B,$thf( b ))]]) ).
thf(1321,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,996]) ).
thf(1322,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[1321]) ).
thf(1323,plain,
! [A: age] :
( ~ ( b @ age_of @ ( A @ greater ) )
| ~ ( A @ ( sk3 @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1322:[bind(A,$thf( sk3 @ age_of )),bind(B,$thf( B )),bind(C,$thf( b @ age_of ))]]) ).
thf(1359,plain,
! [A: age] :
( ~ ( b @ age_of @ ( A @ greater ) )
| ~ ( A @ ( sk3 @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[1323]) ).
thf(300,plain,
! [B: age,A: age] :
( ( B
!= ( d @ age_of ) )
| ( b @ age_of @ ( A @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,149]) ).
thf(301,plain,
! [A: age] :
( ( b @ age_of @ ( A @ greater ) )
| ( A @ ( d @ age_of @ greater ) )
| ( d @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[300:[bind(A,$thf( A )),bind(B,$thf( d @ age_of ))]]) ).
thf(966,plain,
! [B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( B @ greater ) ) )
| ~ $true
| ~ ( B @ ( c @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,434]) ).
thf(967,plain,
! [B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( B @ greater ) ) )
| ~ ( B @ ( c @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[966]) ).
thf(968,plain,
! [A: knowheyan] :
( ~ ( A @ age_of @ ( c @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(pattern_uni,[status(thm)],[967:[bind(A,$thf( C )),bind(B,$thf( C @ age_of ))]]) ).
thf(1015,plain,
! [A: knowheyan] :
( ~ ( A @ age_of @ ( c @ age_of @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[968]) ).
thf(47190,plain,
! [A: knowheyan] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[47048,1015]) ).
thf(47191,plain,
! [A: knowheyan] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[47190]) ).
thf(47192,plain,
( ( e @ job_of )
!= lunar_energy_engineer ),
inference(pattern_uni,[status(thm)],[47191:[bind(A,$thf( e ))]]) ).
thf(23,axiom,
! [A: knowheyan,B: knowheyan] :
( ( ( ( B @ job_of )
= synthetic_food_nutitionist )
& ( ( A @ job_of )
= space_planner ) )
=> ( B @ age_of @ ( A @ age_of @ greater ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',age_job2) ).
thf(108,plain,
! [A: knowheyan,B: knowheyan] :
( ( ( ( B @ job_of )
= synthetic_food_nutitionist )
& ( ( A @ job_of )
= space_planner ) )
=> ( B @ age_of @ ( A @ age_of @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(109,plain,
! [B: knowheyan,A: knowheyan] :
( ( B @ age_of @ ( A @ age_of @ greater ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(cnf,[status(esa)],[108]) ).
thf(110,plain,
! [B: knowheyan,A: knowheyan] :
( ( B @ age_of @ ( A @ age_of @ greater ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(lifteq,[status(thm)],[109]) ).
thf(28,axiom,
c != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_not_d) ).
thf(123,plain,
c != d,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(124,plain,
c != d,
inference(polarity_switch,[status(thm)],[123]) ).
thf(125,plain,
d != c,
inference(lifteq,[status(thm)],[124]) ).
thf(1029,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,973]) ).
thf(1030,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[1029]) ).
thf(1031,plain,
! [A: age] :
( ~ ( d @ age_of @ ( A @ greater ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1030:[bind(A,$thf( c @ age_of )),bind(B,$thf( B )),bind(C,$thf( d @ age_of ))]]) ).
thf(1064,plain,
! [A: age] :
( ~ ( d @ age_of @ ( A @ greater ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[1031]) ).
thf(47115,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ~ ( d @ age_of @ ( A @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47048,1064]) ).
thf(47116,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ~ ( d @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[47115]) ).
thf(47117,plain,
~ ( d @ age_of @ ( e @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[47116:[bind(A,$thf( e @ age_of ))]]) ).
thf(176,plain,
! [C: age,B: age,A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[74,47]) ).
thf(177,plain,
! [C: age,B: age,A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(178,plain,
! [A: age] :
( ( A @ ( b @ age_of @ greater ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[177:[bind(A,$thf( b @ age_of )),bind(B,$thf( c @ age_of )),bind(C,$thf( C ))]]) ).
thf(196,plain,
! [A: age] :
( ( A @ ( b @ age_of @ greater ) )
| ~ ( A @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(2663,plain,
! [B: age,A: age] :
( ( ( sk3 @ age_of @ ( d @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2596,61]) ).
thf(2664,plain,
! [B: age,A: age] :
( ( ( sk3 @ age_of @ ( d @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[2663]) ).
thf(2665,plain,
~ ( d @ age_of @ ( sk3 @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[2664:[bind(A,$thf( d @ age_of )),bind(B,$thf( sk3 @ age_of ))]]) ).
thf(2743,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,2665]) ).
thf(2744,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[2743]) ).
thf(2745,plain,
( ( ( d @ job_of )
!= synthetic_food_nutitionist )
| ( ( sk3 @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[2744:[bind(A,$thf( sk3 )),bind(B,$thf( d ))]]) ).
thf(20620,plain,
! [A: knowheyan] :
( ( ( A @ job_of @ sk2 )
!= ( synthetic_food_nutitionist @ sk2 ) )
| ( d = A )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[20319,231]) ).
thf(20697,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( d = A )
| ( ( d @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[20620]) ).
thf(18,axiom,
a != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_c) ).
thf(91,plain,
a != c,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(92,plain,
a != c,
inference(polarity_switch,[status(thm)],[91]) ).
thf(93,plain,
c != a,
inference(lifteq,[status(thm)],[92]) ).
thf(44,plain,
? [A: age > knowheyan] :
! [B: knowheyan] :
( ( B @ age_of @ A )
= B ),
inference(detectInverse,[status(thm)],[43]) ).
thf(45,plain,
! [A: knowheyan] :
( ( A @ age_of @ sk1 )
= A ),
inference(cnf,[status(esa)],[44]) ).
thf(152,plain,
! [A: knowheyan] :
( ( A @ age_of @ sk1 )
= A ),
inference(lifteq,[status(thm)],[45]) ).
thf(20618,plain,
! [A: knowheyan] :
( ( ( d @ job_of )
!= ( A @ job_of ) )
| ( ( airfoil_technician @ sk2 )
= A )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(paramod_ordered,[status(thm)],[20319,231]) ).
thf(20619,plain,
( ( ( airfoil_technician @ sk2 )
= d )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d ) ),
inference(pattern_uni,[status(thm)],[20618:[bind(A,$thf( d ))]]) ).
thf(20839,plain,
( ( d != d )
| ( ( synthetic_food_nutitionist @ sk2 )
!= ( airfoil_technician @ sk2 ) )
| ( ( airfoil_technician @ sk2 )
= d )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(eqfactor_ordered,[status(thm)],[20619]) ).
thf(20841,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
!= ( airfoil_technician @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( airfoil_technician @ sk2 )
= d ) ),
inference(simp,[status(thm)],[20839]) ).
thf(288,plain,
! [B: age,A: age] :
( ( B
!= ( c @ age_of ) )
| ( A @ ( b @ age_of @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,74]) ).
thf(289,plain,
! [A: age] :
( ( A @ ( b @ age_of @ greater ) )
| ( A @ ( c @ age_of @ greater ) )
| ( c @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[288:[bind(A,$thf( A )),bind(B,$thf( c @ age_of ))]]) ).
thf(320,plain,
! [B: age,A: age] :
( ( B
!= ( d @ age_of ) )
| ( A @ ( a @ age_of @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,90]) ).
thf(321,plain,
! [A: age] :
( ( A @ ( a @ age_of @ greater ) )
| ( A @ ( d @ age_of @ greater ) )
| ( d @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[320:[bind(A,$thf( A )),bind(B,$thf( d @ age_of ))]]) ).
thf(251,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ $true
| ~ ( D @ ( C @ greater ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,47]) ).
thf(252,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ ( D @ ( C @ greater ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[251]) ).
thf(253,plain,
! [C: age,B: age,A: age] :
( ( B @ ( C @ greater ) )
| ~ ( A @ ( C @ greater ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(pattern_uni,[status(thm)],[252:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(1471,plain,
! [C: age,B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( C @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,56]) ).
thf(1472,plain,
! [C: age,B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( C @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1471]) ).
thf(1473,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1472:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B @ age_of ))]]) ).
thf(1526,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1473]) ).
thf(16,axiom,
b != e,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_e) ).
thf(87,plain,
b != e,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(88,plain,
b != e,
inference(polarity_switch,[status(thm)],[87]) ).
thf(89,plain,
e != b,
inference(lifteq,[status(thm)],[88]) ).
thf(31,axiom,
airfoil_technician != space_planner,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',airfoil_technician_not_space_planner) ).
thf(131,plain,
airfoil_technician != space_planner,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(132,plain,
airfoil_technician != space_planner,
inference(polarity_switch,[status(thm)],[131]) ).
thf(133,plain,
space_planner != airfoil_technician,
inference(lifteq,[status(thm)],[132]) ).
thf(21,axiom,
airfoil_technician != communications_consultant,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',airfoil_technician_not_communications_consultant) ).
thf(102,plain,
airfoil_technician != communications_consultant,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(278,plain,
! [D: knowheyan,C: knowheyan,B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( C @ age_of @ ( D @ age_of @ greater ) ) )
| ~ $true
| ( ( C @ job_of )
!= communications_consultant )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,116]) ).
thf(279,plain,
! [D: knowheyan,C: knowheyan,B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( C @ age_of @ ( D @ age_of @ greater ) ) )
| ( ( C @ job_of )
!= communications_consultant )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[278]) ).
thf(280,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ job_of )
!= communications_consultant )
| ( A @ age_of @ ( B @ age_of @ greater ) )
| ( ( A @ age_of )
= ( B @ age_of ) ) ),
inference(pattern_uni,[status(thm)],[279:[bind(A,$thf( E @ age_of )),bind(B,$thf( F @ age_of )),bind(C,$thf( F )),bind(D,$thf( E ))]]) ).
thf(334,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ job_of )
!= communications_consultant )
| ( A @ age_of @ ( B @ age_of @ greater ) )
| ( ( A @ age_of )
= ( B @ age_of ) ) ),
inference(simp,[status(thm)],[280]) ).
thf(1221,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,973]) ).
thf(1222,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1221]) ).
thf(1223,plain,
( ( ( d @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1222:[bind(A,$thf( c )),bind(B,$thf( d ))]]) ).
thf(41624,plain,
! [A: knowheyan] :
( ( ( b @ job_of )
!= ( A @ job_of ) )
| ( ( airfoil_technician @ sk2 )
= A )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(paramod_ordered,[status(thm)],[41267,231]) ).
thf(41625,plain,
( ( ( airfoil_technician @ sk2 )
= b )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(pattern_uni,[status(thm)],[41624:[bind(A,$thf( b ))]]) ).
thf(155,plain,
! [A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[90,56]) ).
thf(156,plain,
! [A: age] :
( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[155]) ).
thf(158,plain,
! [A: age] :
( ( ( d @ age_of )
!= A )
| ( ( a @ age_of )
!= A ) ),
inference(simp,[status(thm)],[156]) ).
thf(160,plain,
( ( d @ age_of )
!= ( a @ age_of ) ),
inference(simp,[status(thm)],[158]) ).
thf(9,axiom,
space_planner != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',space_planner_not_synthetic_food_nutitionist) ).
thf(68,plain,
space_planner != synthetic_food_nutitionist,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(69,plain,
space_planner != synthetic_food_nutitionist,
inference(polarity_switch,[status(thm)],[68]) ).
thf(70,plain,
synthetic_food_nutitionist != space_planner,
inference(lifteq,[status(thm)],[69]) ).
thf(33,axiom,
communications_consultant != space_planner,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_space_planner) ).
thf(137,plain,
communications_consultant != space_planner,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(1236,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,397]) ).
thf(1237,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1236]) ).
thf(1238,plain,
( ( ( a @ job_of )
!= synthetic_food_nutitionist )
| ( ( d @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1237:[bind(A,$thf( d )),bind(B,$thf( a ))]]) ).
thf(359,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ~ ( D @ ( E @ greater ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,61]) ).
thf(360,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ~ ( D @ ( E @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[359]) ).
thf(361,plain,
! [C: age,B: age,A: age] :
( ~ ( A @ ( C @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[360:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(8,axiom,
lunar_energy_engineer != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lunar_energy_engineer_not_synthetic_food_nutitionist) ).
thf(65,plain,
lunar_energy_engineer != synthetic_food_nutitionist,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(548,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( c @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,391]) ).
thf(549,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( c @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[548]) ).
thf(550,plain,
! [A: age] :
( ~ ( c @ age_of @ ( A @ greater ) )
| ~ ( A @ ( sk3 @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[549:[bind(A,$thf( sk3 @ age_of )),bind(B,$thf( B )),bind(C,$thf( c @ age_of ))]]) ).
thf(578,plain,
! [A: age] :
( ~ ( c @ age_of @ ( A @ greater ) )
| ~ ( A @ ( sk3 @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[550]) ).
thf(47174,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ~ ( b @ age_of @ ( A @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47048,434]) ).
thf(47175,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ~ ( b @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[47174]) ).
thf(47176,plain,
~ ( b @ age_of @ ( e @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[47175:[bind(A,$thf( e @ age_of ))]]) ).
thf(42026,plain,
( ( ( synthetic_food_nutitionist @ sk2 )
!= ( synthetic_food_nutitionist @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( d = b )
| ( ( airfoil_technician @ sk2 )
= b )
| ( ( space_planner @ sk2 )
= b ) ),
inference(paramod_ordered,[status(thm)],[41625,31992]) ).
thf(42027,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( d = b )
| ( ( airfoil_technician @ sk2 )
= b )
| ( ( space_planner @ sk2 )
= b ) ),
inference(pattern_uni,[status(thm)],[42026:[]]) ).
thf(50489,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( airfoil_technician @ sk2 )
= b )
| ( ( space_planner @ sk2 )
= b ) ),
inference(simplifyReflect,[status(thm)],[42027,113]) ).
thf(52659,plain,
( ( ( space_planner @ sk2 )
!= ( space_planner @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( airfoil_technician @ sk2 )
= b )
| ( sk3 = b )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[52255,50489]) ).
thf(52660,plain,
( ( ( space_planner @ sk2 )
!= ( space_planner @ sk2 ) )
| ( ( airfoil_technician @ sk2 )
= b )
| ( sk3 = b )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[52659]) ).
thf(52661,plain,
( ( ( airfoil_technician @ sk2 )
= b )
| ( sk3 = b )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(pattern_uni,[status(thm)],[52660:[]]) ).
thf(52874,plain,
( ( ( airfoil_technician @ sk2 )
= b )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simplifyReflect,[status(thm)],[52661,448]) ).
thf(1342,plain,
! [B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,996]) ).
thf(1343,plain,
! [B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[1342]) ).
thf(1344,plain,
( ( sk3 @ age_of @ ( b @ age_of @ greater ) )
| ( ( sk3 @ age_of )
= ( b @ age_of ) ) ),
inference(pattern_uni,[status(thm)],[1343:[bind(A,$thf( sk3 @ age_of )),bind(B,$thf( b @ age_of ))]]) ).
thf(1397,plain,
sk3 @ age_of @ ( b @ age_of @ greater ),
inference(simplifyReflect,[status(thm)],[1344,438]) ).
thf(1257,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,391]) ).
thf(1258,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1257]) ).
thf(1259,plain,
( ( ( c @ job_of )
!= synthetic_food_nutitionist )
| ( ( sk3 @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1258:[bind(A,$thf( sk3 )),bind(B,$thf( c ))]]) ).
thf(2925,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[193,973]) ).
thf(2926,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2925]) ).
thf(2927,plain,
~ ( a @ age_of @ ( c @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[2926:[bind(A,$thf( c @ age_of ))]]) ).
thf(3120,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,2927]) ).
thf(3121,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[3120]) ).
thf(3122,plain,
( ( ( a @ job_of )
!= space_planner )
| ( ( c @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[3121:[bind(A,$thf( c )),bind(B,$thf( a ))]]) ).
thf(266,plain,
! [C: knowheyan,B: age,A: age] :
( ( A
!= ( C @ age_of ) )
| ( ( B @ sk1 )
= C )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,152]) ).
thf(267,plain,
! [B: knowheyan,A: age] :
( ( ( A @ sk1 )
= B )
| ( B @ age_of @ ( A @ greater ) )
| ( A @ ( B @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[266:[bind(A,$thf( D @ age_of )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(328,plain,
! [B: knowheyan,A: age] :
( ( ( A @ sk1 )
= B )
| ( B @ age_of @ ( A @ greater ) )
| ( A @ ( B @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(662,plain,
! [C: knowheyan,B: age,A: age] :
( ( A
!= ( C @ age_of ) )
| ( b @ age_of @ ( B @ greater ) )
| ( ( C @ job_of )
!= lunar_energy_engineer )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,77]) ).
thf(663,plain,
! [B: knowheyan,A: age] :
( ( b @ age_of @ ( A @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer )
| ( B @ age_of @ ( A @ greater ) )
| ( A @ ( B @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( D @ age_of )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(679,plain,
! [B: knowheyan,A: age] :
( ( b @ age_of @ ( A @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer )
| ( B @ age_of @ ( A @ greater ) )
| ( A @ ( B @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[663]) ).
thf(209,plain,
! [A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[149,56]) ).
thf(210,plain,
! [A: age] :
( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[209]) ).
thf(211,plain,
! [A: age] :
( ( ( b @ age_of )
!= A )
| ( ( d @ age_of )
!= A ) ),
inference(simp,[status(thm)],[210]) ).
thf(212,plain,
( ( d @ age_of )
!= ( b @ age_of ) ),
inference(simp,[status(thm)],[211]) ).
thf(1459,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,973]) ).
thf(1460,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1459]) ).
thf(1461,plain,
( ( ( d @ job_of )
!= space_planner )
| ( ( c @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1460:[bind(A,$thf( c )),bind(B,$thf( d ))]]) ).
thf(32,axiom,
communications_consultant != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_synthetic_food_nutitionist) ).
thf(134,plain,
communications_consultant != synthetic_food_nutitionist,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(30,axiom,
b != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_c) ).
thf(128,plain,
b != c,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(47065,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ( A @ ( b @ age_of @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47048,196]) ).
thf(47066,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( c @ age_of @ greater ) ) )
| ( A @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[47065]) ).
thf(47067,plain,
e @ age_of @ ( b @ age_of @ greater ),
inference(pattern_uni,[status(thm)],[47066:[bind(A,$thf( e @ age_of ))]]) ).
thf(203,plain,
! [C: age,B: age,A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[149,47]) ).
thf(204,plain,
! [C: age,B: age,A: age] :
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(205,plain,
! [A: age] :
( ( A @ ( d @ age_of @ greater ) )
| ~ ( A @ ( b @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[204:[bind(A,$thf( d @ age_of )),bind(B,$thf( b @ age_of )),bind(C,$thf( C ))]]) ).
thf(213,plain,
! [A: age] :
( ( A @ ( d @ age_of @ greater ) )
| ~ ( A @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[205]) ).
thf(47589,plain,
! [A: age] :
( ( ( e @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ ( b @ age_of @ greater ) ) )
| ( A @ ( d @ age_of @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47067,213]) ).
thf(47590,plain,
! [A: age] :
( ( ( e @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ ( b @ age_of @ greater ) ) )
| ( A @ ( d @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[47589]) ).
thf(47591,plain,
e @ age_of @ ( d @ age_of @ greater ),
inference(pattern_uni,[status(thm)],[47590:[bind(A,$thf( e @ age_of ))]]) ).
thf(3103,plain,
! [B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( a @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,2927]) ).
thf(3104,plain,
! [B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( a @ age_of @ ( c @ age_of @ greater ) ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[3103]) ).
thf(3105,plain,
( ( c @ age_of @ ( a @ age_of @ greater ) )
| ( ( c @ age_of )
= ( a @ age_of ) ) ),
inference(pattern_uni,[status(thm)],[3104:[bind(A,$thf( c @ age_of )),bind(B,$thf( a @ age_of ))]]) ).
thf(1054,plain,
( ( ( d @ age_of @ ( c @ age_of @ greater ) )
!= ( d @ age_of @ ( a @ age_of @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[90,973]) ).
thf(1055,plain,
( ( d @ age_of @ ( c @ age_of @ greater ) )
!= ( d @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[1054]) ).
thf(1056,plain,
( ( ( d @ age_of )
!= ( d @ age_of ) )
| ( ( c @ age_of )
!= ( a @ age_of ) ) ),
inference(simp,[status(thm)],[1055]) ).
thf(1061,plain,
( ( c @ age_of )
!= ( a @ age_of ) ),
inference(simp,[status(thm)],[1056]) ).
thf(3641,plain,
c @ age_of @ ( a @ age_of @ greater ),
inference(simplifyReflect,[status(thm)],[3105,1061]) ).
thf(3673,plain,
! [A: age] :
( ( ( c @ age_of @ ( a @ age_of @ greater ) )
!= ( c @ age_of @ ( A @ greater ) ) )
| ( sk3 @ age_of @ ( A @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3641,187]) ).
thf(3674,plain,
! [A: age] :
( ( ( c @ age_of @ ( a @ age_of @ greater ) )
!= ( c @ age_of @ ( A @ greater ) ) )
| ( sk3 @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[3673]) ).
thf(3675,plain,
sk3 @ age_of @ ( a @ age_of @ greater ),
inference(pattern_uni,[status(thm)],[3674:[bind(A,$thf( a @ age_of ))]]) ).
thf(49039,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,47176]) ).
thf(49040,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[49039]) ).
thf(49041,plain,
( ( ( b @ job_of )
!= space_planner )
| ( ( e @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[49040:[bind(A,$thf( e )),bind(B,$thf( b ))]]) ).
thf(2928,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[193,373]) ).
thf(2929,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2928]) ).
thf(2930,plain,
~ ( a @ age_of @ ( b @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[2929:[bind(A,$thf( b @ age_of ))]]) ).
thf(3188,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,2930]) ).
thf(3189,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( b @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[3188]) ).
thf(3190,plain,
( ( ( a @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[3189:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(21450,plain,
! [A: knowheyan] :
( ( ( A @ job_of @ sk2 )
!= ( synthetic_food_nutitionist @ sk2 ) )
| ( A
!= ( airfoil_technician @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( airfoil_technician @ sk2 )
= d ) ),
inference(paramod_ordered,[status(thm)],[231,20841]) ).
thf(21473,plain,
( ( ( airfoil_technician @ sk2 @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( airfoil_technician @ sk2 )
= d ) ),
inference(simp,[status(thm)],[21450]) ).
thf(24628,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( a @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[15202,116]) ).
thf(24629,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( a @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[24628]) ).
thf(24630,plain,
( ( ( a @ job_of )
!= communications_consultant )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[24629:[bind(A,$thf( a )),bind(B,$thf( e ))]]) ).
thf(25244,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( e @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[24630,116]) ).
thf(25245,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( e @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[25244]) ).
thf(25246,plain,
( ( ( e @ job_of )
!= communications_consultant )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(pattern_uni,[status(thm)],[25245:[bind(A,$thf( e )),bind(B,$thf( a ))]]) ).
thf(25554,plain,
( ( communications_consultant != communications_consultant )
| ( ( e @ job_of )
!= ( a @ job_of ) )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(eqfactor_ordered,[status(thm)],[25246]) ).
thf(25556,plain,
( ( ( e @ job_of )
!= ( a @ job_of ) )
| ( ( a @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[25554]) ).
thf(36,axiom,
airfoil_technician != lunar_energy_engineer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',airfoil_technician_not_lunar_energy_engineer) ).
thf(146,plain,
airfoil_technician != lunar_energy_engineer,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(147,plain,
airfoil_technician != lunar_energy_engineer,
inference(polarity_switch,[status(thm)],[146]) ).
thf(148,plain,
lunar_energy_engineer != airfoil_technician,
inference(lifteq,[status(thm)],[147]) ).
thf(44510,plain,
( ( ( c @ job_of )
!= ( c @ job_of ) )
| ( space_planner != space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[44492,31992]) ).
thf(44511,plain,
( ( ( c @ job_of )
!= ( c @ job_of ) )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[44510]) ).
thf(44512,plain,
( ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[44511:[]]) ).
thf(737,plain,
! [C: knowheyan,B: knowheyan,A: job] :
( ( A
!= ( B @ job_of ) )
| ( ( C @ job_of )
!= synthetic_food_nutitionist )
| ( B = C )
| ( A = lunar_energy_engineer )
| ( A = space_planner )
| ( A = communications_consultant )
| ( A = airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[73,96]) ).
thf(738,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( B = A )
| ( ( B @ job_of )
= lunar_energy_engineer )
| ( ( B @ job_of )
= space_planner )
| ( ( B @ job_of )
= communications_consultant )
| ( ( B @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[737:[bind(A,$thf( D @ job_of )),bind(B,$thf( D ))]]) ).
thf(745,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( B = A )
| ( ( B @ job_of )
= lunar_energy_engineer )
| ( ( B @ job_of )
= space_planner )
| ( ( B @ job_of )
= communications_consultant )
| ( ( B @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[738]) ).
thf(7,axiom,
communications_consultant != lunar_energy_engineer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',communications_consultant_not_lunar_energy_engineer) ).
thf(62,plain,
communications_consultant != lunar_energy_engineer,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(63,plain,
communications_consultant != lunar_energy_engineer,
inference(polarity_switch,[status(thm)],[62]) ).
thf(64,plain,
lunar_energy_engineer != communications_consultant,
inference(lifteq,[status(thm)],[63]) ).
thf(290,plain,
! [B: age,A: age] :
( ( B
!= ( b @ age_of ) )
| ( c @ age_of @ ( A @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,74]) ).
thf(291,plain,
! [A: age] :
( ( c @ age_of @ ( A @ greater ) )
| ( A @ ( b @ age_of @ greater ) )
| ( b @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[290:[bind(A,$thf( A )),bind(B,$thf( b @ age_of ))]]) ).
thf(257,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( A @ ( B @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ $true
| ~ ( D @ ( C @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,47]) ).
thf(258,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( A @ ( B @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ ( D @ ( C @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[257]) ).
thf(259,plain,
! [C: age,B: age,A: age] :
( ( A @ ( C @ greater ) )
| ~ ( B @ ( C @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(pattern_uni,[status(thm)],[258:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( A ))]]) ).
thf(1224,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,373]) ).
thf(1225,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1224]) ).
thf(1226,plain,
( ( ( d @ job_of )
!= synthetic_food_nutitionist )
| ( ( b @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1225:[bind(A,$thf( b )),bind(B,$thf( d ))]]) ).
thf(48244,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[193,47117]) ).
thf(48245,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( e @ age_of @ greater ) ) )
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[48244]) ).
thf(48246,plain,
~ ( a @ age_of @ ( e @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[48245:[bind(A,$thf( e @ age_of ))]]) ).
thf(49385,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,48246]) ).
thf(49386,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[49385]) ).
thf(49387,plain,
( ( ( a @ job_of )
!= space_planner )
| ( ( e @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[49386:[bind(A,$thf( e )),bind(B,$thf( a ))]]) ).
thf(3171,plain,
! [B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( a @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,2930]) ).
thf(3172,plain,
! [B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( a @ age_of @ ( b @ age_of @ greater ) ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[3171]) ).
thf(3173,plain,
( ( b @ age_of @ ( a @ age_of @ greater ) )
| ( ( b @ age_of )
= ( a @ age_of ) ) ),
inference(pattern_uni,[status(thm)],[3172:[bind(A,$thf( b @ age_of )),bind(B,$thf( a @ age_of ))]]) ).
thf(528,plain,
( ( ( d @ age_of @ ( b @ age_of @ greater ) )
!= ( d @ age_of @ ( a @ age_of @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[90,373]) ).
thf(529,plain,
( ( d @ age_of @ ( b @ age_of @ greater ) )
!= ( d @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[528]) ).
thf(532,plain,
( ( ( d @ age_of )
!= ( d @ age_of ) )
| ( ( b @ age_of )
!= ( a @ age_of ) ) ),
inference(simp,[status(thm)],[529]) ).
thf(536,plain,
( ( b @ age_of )
!= ( a @ age_of ) ),
inference(simp,[status(thm)],[532]) ).
thf(4251,plain,
b @ age_of @ ( a @ age_of @ greater ),
inference(simplifyReflect,[status(thm)],[3173,536]) ).
thf(312,plain,
! [B: age,A: age] :
( ( B
!= ( sk3 @ age_of ) )
| ( A @ ( c @ age_of @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,127]) ).
thf(313,plain,
! [A: age] :
( ( A @ ( c @ age_of @ greater ) )
| ( A @ ( sk3 @ age_of @ greater ) )
| ( sk3 @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[312:[bind(A,$thf( A )),bind(B,$thf( sk3 @ age_of ))]]) ).
thf(45278,plain,
! [A: knowheyan] :
( ( ( c @ job_of )
!= ( A @ job_of ) )
| ( ( airfoil_technician @ sk2 )
= A )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( synthetic_food_nutitionist @ sk2 )
= c ) ),
inference(paramod_ordered,[status(thm)],[44512,231]) ).
thf(45279,plain,
( ( ( airfoil_technician @ sk2 )
= c )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( synthetic_food_nutitionist @ sk2 )
= c ) ),
inference(pattern_uni,[status(thm)],[45278:[bind(A,$thf( c ))]]) ).
thf(153,plain,
! [A: age] :
( ( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[74,56]) ).
thf(154,plain,
! [A: age] :
( ( c @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[153]) ).
thf(157,plain,
! [A: age] :
( ( ( c @ age_of )
!= A )
| ( ( b @ age_of )
!= A ) ),
inference(simp,[status(thm)],[154]) ).
thf(159,plain,
( ( c @ age_of )
!= ( b @ age_of ) ),
inference(simp,[status(thm)],[157]) ).
thf(170,plain,
! [F: age,E: age,D: age,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( F @ ( E @ greater ) ) )
| ( F @ ( D @ greater ) )
| ~ $true
| ~ ( E @ ( D @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,47]) ).
thf(171,plain,
! [F: age,E: age,D: age,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( F @ ( E @ greater ) ) )
| ( F @ ( D @ greater ) )
| ~ ( E @ ( D @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(172,plain,
! [D: age,C: age,B: age,A: age] :
( ( C @ ( D @ greater ) )
| ~ ( A @ ( D @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[171:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(14,axiom,
space_planner != lunar_energy_engineer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',space_planner_not_lunar_energy_engineer) ).
thf(81,plain,
space_planner != lunar_energy_engineer,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(215,plain,
! [E: knowheyan,D: knowheyan,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( D @ age_of @ ( E @ age_of @ greater ) ) )
| ~ $true
| ( ( D @ job_of )
!= communications_consultant )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,116]) ).
thf(216,plain,
! [E: knowheyan,D: knowheyan,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( D @ age_of @ ( E @ age_of @ greater ) ) )
| ( ( D @ job_of )
!= communications_consultant )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[215]) ).
thf(217,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ( ( C @ job_of )
!= communications_consultant )
| ~ ( C @ age_of @ ( A @ greater ) )
| ~ ( A @ ( B @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[216:[bind(A,$thf( F @ age_of )),bind(B,$thf( B )),bind(C,$thf( G @ age_of )),bind(D,$thf( G )),bind(E,$thf( F ))]]) ).
thf(230,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ( ( C @ job_of )
!= communications_consultant )
| ~ ( C @ age_of @ ( A @ greater ) )
| ~ ( A @ ( B @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[217]) ).
thf(302,plain,
! [B: age,A: age] :
( ( B
!= ( b @ age_of ) )
| ( A @ ( d @ age_of @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,149]) ).
thf(303,plain,
! [A: age] :
( ( A @ ( d @ age_of @ greater ) )
| ( A @ ( b @ age_of @ greater ) )
| ( b @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[302:[bind(A,$thf( A )),bind(B,$thf( b @ age_of ))]]) ).
thf(43610,plain,
! [A: knowheyan] :
( ( ( sk3 @ job_of )
!= ( A @ job_of ) )
| ( ( space_planner @ sk2 )
= A )
| ( ( synthetic_food_nutitionist @ sk2 )
= sk3 )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[43378,231]) ).
thf(43611,plain,
( ( ( space_planner @ sk2 )
= sk3 )
| ( ( synthetic_food_nutitionist @ sk2 )
= sk3 )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[43610:[bind(A,$thf( sk3 ))]]) ).
thf(44044,plain,
! [A: knowheyan] :
( ( ( sk3 @ job_of )
!= ( A @ job_of ) )
| ( ( airfoil_technician @ sk2 )
= A )
| ( ( space_planner @ sk2 )
= sk3 )
| ( ( synthetic_food_nutitionist @ sk2 )
= sk3 ) ),
inference(paramod_ordered,[status(thm)],[43611,231]) ).
thf(44045,plain,
( ( ( airfoil_technician @ sk2 )
= sk3 )
| ( ( space_planner @ sk2 )
= sk3 )
| ( ( synthetic_food_nutitionist @ sk2 )
= sk3 ) ),
inference(pattern_uni,[status(thm)],[44044:[bind(A,$thf( sk3 ))]]) ).
thf(3014,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[193,2665]) ).
thf(3015,plain,
! [A: age] :
( ( ( d @ age_of @ ( A @ greater ) )
!= ( d @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ ( a @ age_of @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[3014]) ).
thf(3016,plain,
~ ( a @ age_of @ ( sk3 @ age_of @ greater ) ),
inference(pattern_uni,[status(thm)],[3015:[bind(A,$thf( sk3 @ age_of ))]]) ).
thf(3217,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,3016]) ).
thf(3218,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[3217]) ).
thf(3219,plain,
( ( ( a @ job_of )
!= synthetic_food_nutitionist )
| ( ( sk3 @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[3218:[bind(A,$thf( sk3 )),bind(B,$thf( a ))]]) ).
thf(44605,plain,
( ( ( c @ job_of )
!= ( c @ job_of ) )
| ( space_planner != space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[44492,13344]) ).
thf(44606,plain,
( ( ( c @ job_of )
!= ( c @ job_of ) )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[44605]) ).
thf(44607,plain,
( ( ( b @ job_of )
!= airfoil_technician )
| ( ( d @ job_of )
!= lunar_energy_engineer )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= c )
| ( ( c @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[44606:[]]) ).
thf(322,plain,
! [B: age,A: age] :
( ( B
!= ( a @ age_of ) )
| ( d @ age_of @ ( A @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,90]) ).
thf(323,plain,
! [A: age] :
( ( d @ age_of @ ( A @ greater ) )
| ( A @ ( a @ age_of @ greater ) )
| ( a @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[322:[bind(A,$thf( A )),bind(B,$thf( a @ age_of ))]]) ).
thf(182,plain,
! [C: age,B: age,A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[127,47]) ).
thf(183,plain,
! [C: age,B: age,A: age] :
( ( ( sk3 @ age_of @ ( c @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[182]) ).
thf(184,plain,
! [A: age] :
( ( A @ ( c @ age_of @ greater ) )
| ~ ( A @ ( sk3 @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[183:[bind(A,$thf( c @ age_of )),bind(B,$thf( sk3 @ age_of )),bind(C,$thf( C ))]]) ).
thf(198,plain,
! [A: age] :
( ( A @ ( c @ age_of @ greater ) )
| ~ ( A @ ( sk3 @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(270,plain,
! [D: knowheyan,C: knowheyan,B: age,A: age] :
( ( A
!= ( C @ age_of ) )
| ~ ( B @ ( D @ age_of @ greater ) )
| ( ( C @ job_of )
!= communications_consultant )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,116]) ).
thf(271,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ~ ( A @ ( B @ age_of @ greater ) )
| ( ( C @ job_of )
!= communications_consultant )
| ( C @ age_of @ ( A @ greater ) )
| ( A @ ( C @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[270:[bind(A,$thf( E @ age_of )),bind(B,$thf( B )),bind(C,$thf( E ))]]) ).
thf(330,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ~ ( A @ ( B @ age_of @ greater ) )
| ( ( C @ job_of )
!= communications_consultant )
| ( C @ age_of @ ( A @ greater ) )
| ( A @ ( C @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[271]) ).
thf(3148,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,2930]) ).
thf(3149,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( b @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[3148]) ).
thf(3150,plain,
( ( ( a @ job_of )
!= synthetic_food_nutitionist )
| ( ( b @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[3149:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(129,plain,
b != c,
inference(polarity_switch,[status(thm)],[128]) ).
thf(130,plain,
c != b,
inference(lifteq,[status(thm)],[129]) ).
thf(32028,plain,
! [A: knowheyan] :
( ( ( A @ job_of @ sk2 )
!= ( synthetic_food_nutitionist @ sk2 ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = d ) ),
inference(paramod_ordered,[status(thm)],[231,31992]) ).
thf(32050,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( A = d ) ),
inference(simp,[status(thm)],[32028]) ).
thf(24599,plain,
! [A: age] :
( ( ( a @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[15202,56]) ).
thf(24600,plain,
! [A: age] :
( ( ( a @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[24599]) ).
thf(24807,plain,
! [A: age] :
( ( ( a @ age_of )
!= A )
| ( ( e @ age_of )
!= A )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[24600]) ).
thf(24879,plain,
( ( ( e @ age_of )
!= ( a @ age_of ) )
| ( e @ age_of @ ( a @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[24807]) ).
thf(32993,plain,
! [A: age] :
( ( ( e @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( ( e @ age_of )
!= ( a @ age_of ) ) ),
inference(paramod_ordered,[status(thm)],[24879,56]) ).
thf(32994,plain,
! [A: age] :
( ( ( e @ age_of @ ( a @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( ( e @ age_of )
!= ( a @ age_of ) ) ),
inference(simp,[status(thm)],[32993]) ).
thf(33259,plain,
! [A: age] :
( ( ( e @ age_of )
!= A )
| ( ( a @ age_of )
!= A )
| ( ( e @ age_of )
!= ( a @ age_of ) ) ),
inference(simp,[status(thm)],[32994]) ).
thf(33464,plain,
( ( e @ age_of )
!= ( a @ age_of ) ),
inference(simp,[status(thm)],[33259]) ).
thf(642,plain,
! [D: age,C: age,B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( D @ ( B @ greater ) )
| ~ ( D @ ( C @ greater ) )
| ~ $true
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,47]) ).
thf(643,plain,
! [D: age,C: age,B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( D @ ( B @ greater ) )
| ~ ( D @ ( C @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[642]) ).
thf(644,plain,
! [B: knowheyan,A: age] :
( ( A @ ( B @ age_of @ greater ) )
| ~ ( A @ ( b @ age_of @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer ) ),
inference(pattern_uni,[status(thm)],[643:[bind(A,$thf( E )),bind(B,$thf( E @ age_of )),bind(C,$thf( b @ age_of )),bind(D,$thf( D ))]]) ).
thf(675,plain,
! [B: knowheyan,A: age] :
( ( A @ ( B @ age_of @ greater ) )
| ~ ( A @ ( b @ age_of @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[644]) ).
thf(41425,plain,
( ( ( b @ job_of )
!= ( b @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( airfoil_technician != airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(paramod_ordered,[status(thm)],[41267,31992]) ).
thf(41426,plain,
( ( ( b @ job_of )
!= ( b @ job_of ) )
| ( ( c @ job_of )
!= space_planner )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(simp,[status(thm)],[41425]) ).
thf(41427,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( synthetic_food_nutitionist @ sk2 )
= d )
| ( ( space_planner @ sk2 )
= b )
| ( ( synthetic_food_nutitionist @ sk2 )
= b ) ),
inference(pattern_uni,[status(thm)],[41426:[]]) ).
thf(48865,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,47176]) ).
thf(48866,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[48865]) ).
thf(48867,plain,
( ( ( b @ job_of )
!= synthetic_food_nutitionist )
| ( ( e @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[48866:[bind(A,$thf( e )),bind(B,$thf( b ))]]) ).
thf(46357,plain,
! [A: knowheyan] :
( ( ( c @ job_of )
!= ( A @ job_of ) )
| ( ( airfoil_technician @ sk2 )
= A )
| ( ( space_planner @ sk2 )
= c )
| ( ( synthetic_food_nutitionist @ sk2 )
= c ) ),
inference(paramod_ordered,[status(thm)],[44757,231]) ).
thf(46358,plain,
( ( ( airfoil_technician @ sk2 )
= c )
| ( ( space_planner @ sk2 )
= c )
| ( ( synthetic_food_nutitionist @ sk2 )
= c ) ),
inference(pattern_uni,[status(thm)],[46357:[bind(A,$thf( c ))]]) ).
thf(14198,plain,
! [B: knowheyan,A: knowheyan] :
( ( B != e )
| ( A != d )
| ( B @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( B @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[346,101]) ).
thf(14199,plain,
! [A: knowheyan] :
( ( A != d )
| ( e @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( e @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[14198:[bind(A,$thf( A )),bind(B,$thf( e ))]]) ).
thf(15344,plain,
( ( e @ age_of @ ( d @ age_of @ greater ) )
| ( d @ age_of @ ( e @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[14199]) ).
thf(27672,plain,
( ~ $true
| ( ( d @ age_of @ ( e @ age_of @ greater ) )
!= ( e @ age_of @ ( d @ age_of @ greater ) ) )
| ( e @ age_of @ ( d @ age_of @ greater ) ) ),
inference(eqfactor_ordered,[status(thm)],[15344]) ).
thf(27695,plain,
( ( ( e @ age_of )
!= ( d @ age_of ) )
| ( ( e @ age_of )
!= ( d @ age_of ) )
| ( e @ age_of @ ( d @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[27672]) ).
thf(27738,plain,
( ( ( e @ age_of )
!= ( d @ age_of ) )
| ( e @ age_of @ ( d @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[27695]) ).
thf(42097,plain,
! [A: age] :
( ( ( e @ age_of @ ( d @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( ( e @ age_of )
!= ( d @ age_of ) ) ),
inference(paramod_ordered,[status(thm)],[27738,56]) ).
thf(42098,plain,
! [A: age] :
( ( ( e @ age_of @ ( d @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( ( e @ age_of )
!= ( d @ age_of ) ) ),
inference(simp,[status(thm)],[42097]) ).
thf(42444,plain,
! [A: age] :
( ( ( e @ age_of )
!= A )
| ( ( d @ age_of )
!= A )
| ( ( e @ age_of )
!= ( d @ age_of ) ) ),
inference(simp,[status(thm)],[42098]) ).
thf(42570,plain,
( ( e @ age_of )
!= ( d @ age_of ) ),
inference(simp,[status(thm)],[42444]) ).
thf(35,axiom,
airfoil_technician != synthetic_food_nutitionist,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',airfoil_technician_not_synthetic_food_nutitionist) ).
thf(143,plain,
airfoil_technician != synthetic_food_nutitionist,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(144,plain,
airfoil_technician != synthetic_food_nutitionist,
inference(polarity_switch,[status(thm)],[143]) ).
thf(145,plain,
synthetic_food_nutitionist != airfoil_technician,
inference(lifteq,[status(thm)],[144]) ).
thf(664,plain,
! [C: knowheyan,B: age,A: age] :
( ( A
!= ( b @ age_of ) )
| ( B @ ( C @ age_of @ greater ) )
| ( ( C @ job_of )
!= lunar_energy_engineer )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,77]) ).
thf(665,plain,
! [B: knowheyan,A: age] :
( ( A @ ( B @ age_of @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer )
| ( b @ age_of @ ( A @ greater ) )
| ( A @ ( b @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[664:[bind(A,$thf( b @ age_of )),bind(B,$thf( B )),bind(C,$thf( C ))]]) ).
thf(680,plain,
! [B: knowheyan,A: age] :
( ( A @ ( B @ age_of @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer )
| ( b @ age_of @ ( A @ greater ) )
| ( A @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[665]) ).
thf(1514,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,367]) ).
thf(1515,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1514]) ).
thf(1516,plain,
( ( ( b @ job_of )
!= space_planner )
| ( ( c @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1515:[bind(A,$thf( c )),bind(B,$thf( b ))]]) ).
thf(3080,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,2927]) ).
thf(3081,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[3080]) ).
thf(3082,plain,
( ( ( a @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[3081:[bind(A,$thf( c )),bind(B,$thf( a ))]]) ).
thf(47984,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,47085]) ).
thf(47985,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[47984]) ).
thf(47986,plain,
( ( ( c @ job_of )
!= space_planner )
| ( ( e @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[47985:[bind(A,$thf( e )),bind(B,$thf( c ))]]) ).
thf(66,plain,
lunar_energy_engineer != synthetic_food_nutitionist,
inference(polarity_switch,[status(thm)],[65]) ).
thf(67,plain,
synthetic_food_nutitionist != lunar_energy_engineer,
inference(lifteq,[status(thm)],[66]) ).
thf(167,plain,
! [F: age,E: age,D: age,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ( F @ ( D @ greater ) )
| ~ ( F @ ( E @ greater ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,47]) ).
thf(168,plain,
! [F: age,E: age,D: age,C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( E @ ( D @ greater ) ) )
| ( F @ ( D @ greater ) )
| ~ ( F @ ( E @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[167]) ).
thf(169,plain,
! [D: age,C: age,B: age,A: age] :
( ( D @ ( A @ greater ) )
| ~ ( D @ ( C @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[168:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(199,plain,
! [D: age,C: age,B: age,A: age] :
( ( D @ ( A @ greater ) )
| ~ ( D @ ( C @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(272,plain,
! [D: knowheyan,C: knowheyan,B: age,A: age] :
( ( A
!= ( D @ age_of ) )
| ~ ( C @ age_of @ ( B @ greater ) )
| ( ( C @ job_of )
!= communications_consultant )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,116]) ).
thf(273,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ~ ( B @ age_of @ ( A @ greater ) )
| ( ( B @ job_of )
!= communications_consultant )
| ( C @ age_of @ ( A @ greater ) )
| ( A @ ( C @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[272:[bind(A,$thf( E @ age_of )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(331,plain,
! [C: knowheyan,B: knowheyan,A: age] :
( ~ ( B @ age_of @ ( A @ greater ) )
| ( ( B @ job_of )
!= communications_consultant )
| ( C @ age_of @ ( A @ greater ) )
| ( A @ ( C @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[273]) ).
thf(14376,plain,
! [B: knowheyan,A: knowheyan] :
( ( B != e )
| ( A != b )
| ( B @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( B @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[346,89]) ).
thf(14377,plain,
! [A: knowheyan] :
( ( A != b )
| ( e @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( e @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[14376:[bind(A,$thf( A )),bind(B,$thf( e ))]]) ).
thf(15114,plain,
( ( e @ age_of @ ( b @ age_of @ greater ) )
| ( b @ age_of @ ( e @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[14377]) ).
thf(21580,plain,
! [A: age] :
( ( ( b @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( e @ age_of @ ( b @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[15114,56]) ).
thf(21581,plain,
! [A: age] :
( ( ( b @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( e @ age_of @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[21580]) ).
thf(21806,plain,
! [A: age] :
( ( ( b @ age_of )
!= A )
| ( ( e @ age_of )
!= A )
| ( e @ age_of @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[21581]) ).
thf(21843,plain,
( ( ( e @ age_of )
!= ( b @ age_of ) )
| ( e @ age_of @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[21806]) ).
thf(26382,plain,
! [A: age] :
( ( ( e @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( ( e @ age_of )
!= ( b @ age_of ) ) ),
inference(paramod_ordered,[status(thm)],[21843,56]) ).
thf(26383,plain,
! [A: age] :
( ( ( e @ age_of @ ( b @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( ( e @ age_of )
!= ( b @ age_of ) ) ),
inference(simp,[status(thm)],[26382]) ).
thf(26679,plain,
! [A: age] :
( ( ( e @ age_of )
!= A )
| ( ( b @ age_of )
!= A )
| ( ( e @ age_of )
!= ( b @ age_of ) ) ),
inference(simp,[status(thm)],[26383]) ).
thf(26757,plain,
( ( e @ age_of )
!= ( b @ age_of ) ),
inference(simp,[status(thm)],[26679]) ).
thf(47089,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ~ $true
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(paramod_ordered,[status(thm)],[47048,116]) ).
thf(47090,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ age_of @ ( B @ age_of @ greater ) ) )
| ( ( A @ job_of )
!= communications_consultant ) ),
inference(simp,[status(thm)],[47089]) ).
thf(47091,plain,
( ( e @ job_of )
!= communications_consultant ),
inference(pattern_uni,[status(thm)],[47090:[bind(A,$thf( e )),bind(B,$thf( c ))]]) ).
thf(507,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,373]) ).
thf(508,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( d @ age_of @ ( b @ age_of @ greater ) ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[507]) ).
thf(509,plain,
! [A: age] :
( ~ ( d @ age_of @ ( A @ greater ) )
| ~ ( A @ ( b @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[508:[bind(A,$thf( b @ age_of )),bind(B,$thf( B )),bind(C,$thf( d @ age_of ))]]) ).
thf(539,plain,
! [A: age] :
( ~ ( d @ age_of @ ( A @ greater ) )
| ~ ( A @ ( b @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[509]) ).
thf(47805,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,47085]) ).
thf(47806,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( c @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[47805]) ).
thf(47807,plain,
( ( ( c @ job_of )
!= synthetic_food_nutitionist )
| ( ( e @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[47806:[bind(A,$thf( e )),bind(B,$thf( c ))]]) ).
thf(103,plain,
airfoil_technician != communications_consultant,
inference(polarity_switch,[status(thm)],[102]) ).
thf(104,plain,
communications_consultant != airfoil_technician,
inference(lifteq,[status(thm)],[103]) ).
thf(1233,plain,
! [C: age,B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( C @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,56]) ).
thf(1234,plain,
! [C: age,B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( C @ ( C @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1233]) ).
thf(1235,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1234:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B @ age_of ))]]) ).
thf(1289,plain,
! [A: knowheyan] :
( ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1235]) ).
thf(1274,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,367]) ).
thf(1275,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1274]) ).
thf(1276,plain,
( ( ( b @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1275:[bind(A,$thf( c )),bind(B,$thf( b ))]]) ).
thf(48181,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,47117]) ).
thf(48182,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[48181]) ).
thf(48183,plain,
( ( ( d @ job_of )
!= synthetic_food_nutitionist )
| ( ( e @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[48182:[bind(A,$thf( e )),bind(B,$thf( d ))]]) ).
thf(1324,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,996]) ).
thf(1325,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( b @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[1324]) ).
thf(1326,plain,
( ( ( b @ job_of )
!= synthetic_food_nutitionist )
| ( ( sk3 @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[1325:[bind(A,$thf( sk3 )),bind(B,$thf( b ))]]) ).
thf(1474,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,397]) ).
thf(1475,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[1474]) ).
thf(1476,plain,
( ( ( a @ job_of )
!= space_planner )
| ( ( d @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[1475:[bind(A,$thf( d )),bind(B,$thf( a ))]]) ).
thf(138,plain,
communications_consultant != space_planner,
inference(polarity_switch,[status(thm)],[137]) ).
thf(139,plain,
space_planner != communications_consultant,
inference(lifteq,[status(thm)],[138]) ).
thf(695,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[47,397]) ).
thf(696,plain,
! [C: age,B: age,A: age] :
( ( ( C @ ( A @ greater ) )
!= ( a @ age_of @ ( d @ age_of @ greater ) ) )
| ~ ( C @ ( B @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[695]) ).
thf(697,plain,
! [A: age] :
( ~ ( a @ age_of @ ( A @ greater ) )
| ~ ( A @ ( d @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[696:[bind(A,$thf( d @ age_of )),bind(B,$thf( B )),bind(C,$thf( a @ age_of ))]]) ).
thf(731,plain,
! [A: age] :
( ~ ( a @ age_of @ ( A @ greater ) )
| ~ ( A @ ( d @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[697]) ).
thf(409,plain,
( ( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[149,367]) ).
thf(410,plain,
( ( b @ age_of @ ( d @ age_of @ greater ) )
!= ( b @ age_of @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[409]) ).
thf(432,plain,
( ( ( b @ age_of )
!= ( b @ age_of ) )
| ( ( d @ age_of )
!= ( c @ age_of ) ) ),
inference(simp,[status(thm)],[410]) ).
thf(433,plain,
( ( d @ age_of )
!= ( c @ age_of ) ),
inference(simp,[status(thm)],[432]) ).
thf(49216,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(paramod_ordered,[status(thm)],[110,48246]) ).
thf(49217,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= synthetic_food_nutitionist )
| ( ( A @ job_of )
!= space_planner ) ),
inference(simp,[status(thm)],[49216]) ).
thf(49218,plain,
( ( ( a @ job_of )
!= synthetic_food_nutitionist )
| ( ( e @ job_of )
!= space_planner ) ),
inference(pattern_uni,[status(thm)],[49217:[bind(A,$thf( e )),bind(B,$thf( a ))]]) ).
thf(14866,plain,
! [B: knowheyan,A: knowheyan] :
( ( B != e )
| ( A != c )
| ( B @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( B @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[346,80]) ).
thf(14867,plain,
! [A: knowheyan] :
( ( A != c )
| ( e @ age_of @ ( A @ age_of @ greater ) )
| ( A @ age_of @ ( e @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[14866:[bind(A,$thf( A )),bind(B,$thf( e ))]]) ).
thf(15273,plain,
( ( e @ age_of @ ( c @ age_of @ greater ) )
| ( c @ age_of @ ( e @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[14867]) ).
thf(25749,plain,
! [A: age] :
( ( ( c @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( e @ age_of @ ( c @ age_of @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[15273,56]) ).
thf(25750,plain,
! [A: age] :
( ( ( c @ age_of @ ( e @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( e @ age_of @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[25749]) ).
thf(25984,plain,
! [A: age] :
( ( ( c @ age_of )
!= A )
| ( ( e @ age_of )
!= A )
| ( e @ age_of @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[25750]) ).
thf(25990,plain,
( ( ( e @ age_of )
!= ( c @ age_of ) )
| ( e @ age_of @ ( c @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[25984]) ).
thf(35890,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( ( e @ age_of )
!= ( c @ age_of ) ) ),
inference(paramod_ordered,[status(thm)],[25990,56]) ).
thf(35891,plain,
! [A: age] :
( ( ( e @ age_of @ ( c @ age_of @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( ( e @ age_of )
!= ( c @ age_of ) ) ),
inference(simp,[status(thm)],[35890]) ).
thf(36245,plain,
! [A: age] :
( ( ( e @ age_of )
!= A )
| ( ( c @ age_of )
!= A )
| ( ( e @ age_of )
!= ( c @ age_of ) ) ),
inference(simp,[status(thm)],[35891]) ).
thf(36335,plain,
( ( e @ age_of )
!= ( c @ age_of ) ),
inference(simp,[status(thm)],[36245]) ).
thf(51643,plain,
! [A: knowheyan] :
( ( ( sk3 @ job_of )
!= ( A @ job_of ) )
| ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( space_planner != space_planner )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[51309,1289]) ).
thf(51644,plain,
! [A: knowheyan] :
( ( ( sk3 @ job_of )
!= ( A @ job_of ) )
| ( ( A @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(simp,[status(thm)],[51643]) ).
thf(51645,plain,
( ( ( sk3 @ job_of )
!= synthetic_food_nutitionist )
| ( ( c @ job_of )
!= space_planner )
| ( ( b @ job_of )
!= airfoil_technician )
| ( ( a @ job_of )
!= communications_consultant )
| ( ( sk3 @ job_of )
= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[51644:[bind(A,$thf( sk3 ))]]) ).
thf(314,plain,
! [B: age,A: age] :
( ( B
!= ( c @ age_of ) )
| ( sk3 @ age_of @ ( A @ greater ) )
| ( A @ ( B @ greater ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[54,127]) ).
thf(315,plain,
! [A: age] :
( ( sk3 @ age_of @ ( A @ greater ) )
| ( A @ ( c @ age_of @ greater ) )
| ( c @ age_of @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[314:[bind(A,$thf( A )),bind(B,$thf( c @ age_of ))]]) ).
thf(48358,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( e @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,47117]) ).
thf(48359,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( e @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[48358]) ).
thf(48360,plain,
( ( ( d @ job_of )
!= space_planner )
| ( ( e @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[48359:[bind(A,$thf( e )),bind(B,$thf( d ))]]) ).
thf(2781,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,2665]) ).
thf(2782,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( d @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[2781]) ).
thf(2783,plain,
( ( ( d @ job_of )
!= space_planner )
| ( ( sk3 @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[2782:[bind(A,$thf( sk3 )),bind(B,$thf( d ))]]) ).
thf(254,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( A @ ( B @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ ( E @ ( D @ greater ) )
| ~ $true
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,47]) ).
thf(255,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( A @ ( B @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ ( E @ ( D @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[254]) ).
thf(256,plain,
! [C: age,B: age,A: age] :
( ( C @ ( B @ greater ) )
| ~ ( C @ ( A @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(pattern_uni,[status(thm)],[255:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(326,plain,
! [C: age,B: age,A: age] :
( ( C @ ( B @ greater ) )
| ~ ( C @ ( A @ greater ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[256]) ).
thf(135,plain,
communications_consultant != synthetic_food_nutitionist,
inference(polarity_switch,[status(thm)],[134]) ).
thf(136,plain,
synthetic_food_nutitionist != communications_consultant,
inference(lifteq,[status(thm)],[135]) ).
thf(3257,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ~ $true
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(paramod_ordered,[status(thm)],[119,3016]) ).
thf(3258,plain,
! [B: knowheyan,A: knowheyan] :
( ( ( B @ age_of @ ( A @ age_of @ greater ) )
!= ( a @ age_of @ ( sk3 @ age_of @ greater ) ) )
| ( ( B @ job_of )
!= space_planner )
| ( ( A @ job_of )
!= airfoil_technician ) ),
inference(simp,[status(thm)],[3257]) ).
thf(3259,plain,
( ( ( a @ job_of )
!= space_planner )
| ( ( sk3 @ job_of )
!= airfoil_technician ) ),
inference(pattern_uni,[status(thm)],[3258:[bind(A,$thf( sk3 )),bind(B,$thf( a ))]]) ).
thf(188,plain,
! [C: age,B: age,A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[90,47]) ).
thf(189,plain,
! [C: age,B: age,A: age] :
( ( ( d @ age_of @ ( a @ age_of @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[188]) ).
thf(190,plain,
! [A: age] :
( ( A @ ( a @ age_of @ greater ) )
| ~ ( A @ ( d @ age_of @ greater ) ) ),
inference(pattern_uni,[status(thm)],[189:[bind(A,$thf( a @ age_of )),bind(B,$thf( d @ age_of )),bind(C,$thf( C ))]]) ).
thf(200,plain,
! [A: age] :
( ( A @ ( a @ age_of @ greater ) )
| ~ ( A @ ( d @ age_of @ greater ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(121,plain,
a != d,
inference(polarity_switch,[status(thm)],[120]) ).
thf(122,plain,
d != a,
inference(lifteq,[status(thm)],[121]) ).
thf(645,plain,
! [D: age,C: age,B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ( D @ ( B @ greater ) )
| ~ $true
| ~ ( C @ ( B @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(paramod_ordered,[status(thm)],[77,47]) ).
thf(646,plain,
! [D: age,C: age,B: age,A: knowheyan] :
( ( ( b @ age_of @ ( A @ age_of @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ( D @ ( B @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ( ( A @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[645]) ).
thf(647,plain,
! [B: knowheyan,A: age] :
( ( b @ age_of @ ( A @ greater ) )
| ~ ( B @ age_of @ ( A @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer ) ),
inference(pattern_uni,[status(thm)],[646:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ age_of )),bind(D,$thf( b @ age_of ))]]) ).
thf(676,plain,
! [B: knowheyan,A: age] :
( ( b @ age_of @ ( A @ greater ) )
| ~ ( B @ age_of @ ( A @ greater ) )
| ( ( B @ job_of )
!= lunar_energy_engineer ) ),
inference(simp,[status(thm)],[647]) ).
thf(248,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ ( E @ ( D @ greater ) )
| ~ $true
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[54,47]) ).
thf(249,plain,
! [E: age,D: age,C: age,B: age,A: age] :
( ( ( B @ ( A @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ( E @ ( C @ greater ) )
| ~ ( E @ ( D @ greater ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[248]) ).
thf(250,plain,
! [C: age,B: age,A: age] :
( ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(pattern_uni,[status(thm)],[249:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(354,plain,
! [C: age,B: age,A: age] :
( ( C @ ( A @ greater ) )
| ~ ( C @ ( B @ greater ) )
| ( A @ ( B @ greater ) )
| ( A = B ) ),
inference(simp,[status(thm)],[250]) ).
thf(82,plain,
space_planner != lunar_energy_engineer,
inference(polarity_switch,[status(thm)],[81]) ).
thf(83,plain,
lunar_energy_engineer != space_planner,
inference(lifteq,[status(thm)],[82]) ).
thf(106623,plain,
$false,
inference(e,[status(thm)],[41,101,42735,52255,44757,47794,120,677,202,56,31992,1310,142,1063,1507,41496,973,1359,301,47192,110,125,47117,196,2745,20697,46,93,152,20841,289,448,78,164,321,253,51309,84,397,61,1526,116,74,89,133,117,220,102,334,1223,43378,2596,41625,38,160,70,137,1238,229,361,65,578,650,1064,47176,52874,2724,13344,1397,1259,3122,328,77,679,212,96,193,1461,134,73,128,105,47591,3675,49041,3190,21473,2729,25556,148,44512,745,64,149,291,59,259,1226,49387,4251,54,313,45279,3641,181,1464,71,391,86,159,187,172,113,81,996,230,434,303,208,44045,3219,44607,367,323,213,91,198,47067,140,108,330,3150,1061,130,41057,1015,223,3016,32050,1496,80,226,33464,505,438,675,41427,48867,2665,2927,123,46358,42570,145,2271,680,44492,48,1516,3082,47986,67,199,331,127,47085,26757,42006,47091,143,43,231,99,539,87,47807,104,1289,1276,48183,1326,43611,1476,114,139,731,75,119,433,49218,536,346,36335,51645,2930,315,146,373,41267,48360,94,2783,326,107,126,136,48246,47048,3259,200,68,62,131,47,1331,122,639,676,90,111,354,83]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ134_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.61 % Computer : n002.cluster.edu
% 0.14/0.61 % Model : x86_64 x86_64
% 0.14/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.61 % Memory : 8046.5625MB
% 0.14/0.61 % OS : Linux 6.8.0-71-generic
% 0.14/0.61 % CPULimit : 300
% 0.14/0.61 % WCLimit : 300
% 0.14/0.61 % DateTime : Sat Sep 26 05:21:51 UTC 2026
% 0.14/0.62 % CPUTime :
% 0.14/0.62 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.01/1.20 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.41/1.42 % [INFO] Parsing done (216ms).
% 1.41/1.44 % [INFO] Running in sequential loop mode.
% 2.09/1.84 % [INFO] eprover registered as external prover.
% 2.09/1.85 % [INFO] Scanning for conjecture ...
% 2.30/1.96 % [INFO] Found a conjecture (or negated_conjecture) and 35 axioms. Running axiom selection ...
% 2.53/2.04 % [INFO] Axiom selection finished. Selected 35 axioms (removed 0 axioms).
% 2.53/2.09 % [INFO] Problem is typed first-order (TPTP TFF).
% 2.53/2.10 % [INFO] Type checking passed.
% 2.53/2.11 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 3.28/2.42 % [INFO] [Domain constraints] Detected constraint on job
% 3.28/2.42 % [INFO] [Domain constraints] dom(job) ⊆ {synthetic_food_nutitionist,lunar_energy_engineer,communications_consultant,space_planner,airfoil_technician}
% 3.28/2.47 % [INFO] [Domain constraints] Detected constraint on knowheyan
% 3.28/2.47 % [INFO] [Domain constraints] dom(knowheyan) ⊆ {e,a,b,c,d}
% 110.58/28.92 % External prover 'e' found a proof!
% 110.58/28.93 % [INFO] Killing All external provers ...
% 110.58/28.93 % Time passed: 28158ms (effective reasoning time: 27484ms)
% 110.58/28.93 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 110.58/28.93 % Axioms used in derivation (35): b_not_e, age_info4, unique_ages, space_planner_not_synthetic_food_nutitionist, b_not_c, age_job2, unique_jobs, age_info1, space_planner_not_lunar_energy_engineer, airfoil_technician_not_synthetic_food_nutitionist, airfoil_technician_not_lunar_energy_engineer, communications_consultant_not_lunar_energy_engineer, age_job1, age_irreflexive, c_not_youngest, lunar_energy_engineer_not_synthetic_food_nutitionist, communications_consultant_not_space_planner, a_not_d, a_not_c, communications_consultant_not_younger, age_info2, c_not_e, b_not_d, a_not_b, c_not_d, airfoil_technician_not_space_planner, age_greater, airfoil_technician_not_communications_consultant, only_jobs, age_transitive, d_not_e, a_not_e, age_info3, only_knowheyans, communications_consultant_not_synthetic_food_nutitionist
% 110.58/28.93 % No. of inferences in proof: 693
% 110.58/28.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 28158 ms resp. 27484 ms w/o parsing
% 111.80/29.16 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 111.80/29.17 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------