%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MSC007-2.005 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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 : Fri Sep 25 02:13:56 PM UTC 2026
% Result : Unsatisfiable 2.80s 6.29s
% Output : CNFRefutation 3.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 30
% Syntax : Number of formulae : 472 ( 68 unt; 0 def)
% Number of atoms : 2124 (1515 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 2364 ( 712 ~;1652 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-1 aty)
% Number of variables : 214 ( 0 sgn 214 !; 0 ?; 207 :)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
pigeon(pigeon_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_1) ).
fof(f6,axiom,
pigeon(pigeon_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_2) ).
fof(f7,axiom,
pigeon(pigeon_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_3) ).
fof(f8,axiom,
pigeon(pigeon_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_4) ).
fof(f9,axiom,
pigeon(pigeon_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_5) ).
fof(f10,axiom,
pigeon_1 != pigeon_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_1_is_not_pigeon_2) ).
fof(f11,axiom,
pigeon_1 != pigeon_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_1_is_not_pigeon_3) ).
fof(f12,axiom,
pigeon_1 != pigeon_4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_1_is_not_pigeon_4) ).
fof(f13,axiom,
pigeon_1 != pigeon_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_1_is_not_pigeon_5) ).
fof(f14,axiom,
pigeon_2 != pigeon_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_2_is_not_pigeon_3) ).
fof(f15,axiom,
pigeon_2 != pigeon_4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_2_is_not_pigeon_4) ).
fof(f16,axiom,
pigeon_2 != pigeon_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_2_is_not_pigeon_5) ).
fof(f17,axiom,
pigeon_3 != pigeon_4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_3_is_not_pigeon_4) ).
fof(f18,axiom,
pigeon_3 != pigeon_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_3_is_not_pigeon_5) ).
fof(f19,axiom,
pigeon_4 != pigeon_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pigeon_4_is_not_pigeon_5) ).
fof(f20,axiom,
hole(hole_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hole_1) ).
fof(f21,axiom,
hole(hole_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hole_2) ).
fof(f22,axiom,
hole(hole_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hole_3) ).
fof(f24,axiom,
hole_1 != hole_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hole_1_is_not_hole_2) ).
fof(f27,axiom,
hole_2 != hole_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hole_2_is_not_hole_3) ).
fof(f28,axiom,
hole_2 != hole_4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hole_2_is_not_hole_4) ).
fof(f30,axiom,
! [X0] :
( X0 = hole_4
| X0 = hole_3
| X0 = hole_2
| X0 = hole_1
| ~ hole(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',all_holes) ).
fof(f31,plain,
! [X0] :
( hole_4 = X0
| hole_3 = X0
| hole_2 = X0
| hole_1 = X0
| ~ hole(X0) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,axiom,
! [X0] :
( hole(hole_of(X0))
| ~ pigeon(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',each_pigeons_hole1) ).
fof(f33,axiom,
! [X0] :
( in(X0,hole_of(X0))
| ~ pigeon(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',each_pigeons_hole2) ).
fof(f34,negated_conjecture,
! [X2,X0,X1] :
( X1 = X2
| ~ in(X2,X0)
| ~ in(X1,X0)
| ~ pigeon(X2)
| ~ pigeon(X1)
| ~ hole(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',only_one_per_hole) ).
tcf(c_81,plain,
pigeon(pigeon_1),
inference(cnf_transformation,[],[f5]) ).
tcf(c_82,plain,
pigeon(pigeon_2),
inference(cnf_transformation,[],[f6]) ).
tcf(c_83,plain,
pigeon(pigeon_3),
inference(cnf_transformation,[],[f7]) ).
tcf(c_84,plain,
pigeon(pigeon_4),
inference(cnf_transformation,[],[f8]) ).
tcf(c_85,plain,
pigeon(pigeon_5),
inference(cnf_transformation,[],[f9]) ).
tcf(c_86,plain,
pigeon_1 != pigeon_2,
inference(cnf_transformation,[],[f10]) ).
tcf(c_87,plain,
pigeon_1 != pigeon_3,
inference(cnf_transformation,[],[f11]) ).
tcf(c_88,plain,
pigeon_1 != pigeon_4,
inference(cnf_transformation,[],[f12]) ).
tcf(c_89,plain,
pigeon_1 != pigeon_5,
inference(cnf_transformation,[],[f13]) ).
tcf(c_90,plain,
pigeon_2 != pigeon_3,
inference(cnf_transformation,[],[f14]) ).
tcf(c_91,plain,
pigeon_2 != pigeon_4,
inference(cnf_transformation,[],[f15]) ).
tcf(c_92,plain,
pigeon_2 != pigeon_5,
inference(cnf_transformation,[],[f16]) ).
tcf(c_93,plain,
pigeon_3 != pigeon_4,
inference(cnf_transformation,[],[f17]) ).
tcf(c_94,plain,
pigeon_3 != pigeon_5,
inference(cnf_transformation,[],[f18]) ).
tcf(c_95,plain,
pigeon_4 != pigeon_5,
inference(cnf_transformation,[],[f19]) ).
tcf(c_96,plain,
hole(hole_1),
inference(cnf_transformation,[],[f20]) ).
tcf(c_97,plain,
hole(hole_2),
inference(cnf_transformation,[],[f21]) ).
tcf(c_98,plain,
hole(hole_3),
inference(cnf_transformation,[],[f22]) ).
tcf(c_100,plain,
hole_1 != hole_2,
inference(cnf_transformation,[],[f24]) ).
tcf(c_103,plain,
hole_2 != hole_3,
inference(cnf_transformation,[],[f27]) ).
tcf(c_104,plain,
hole_2 != hole_4,
inference(cnf_transformation,[],[f28]) ).
tcf(c_106,plain,
! [X0: $i] :
( ( X0 = hole_4 )
| ( X0 = hole_3 )
| ( X0 = hole_2 )
| ( X0 = hole_1 )
| ~ hole(X0) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_107,plain,
! [X0: $i] :
( hole(hole_of(X0))
| ~ pigeon(X0) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_108,plain,
! [X0: $i] :
( in(X0,hole_of(X0))
| ~ pigeon(X0) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_109,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ~ hole(X1)
| ~ pigeon(X2)
| ~ pigeon(X0)
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_350,negated_conjecture,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ hole(X0_iProver_hole_1)
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X1_iProver_pigeon_1,X0_iProver_hole_1)
| ~ in(X0_iProver_pigeon_1,X0_iProver_hole_1) ),
inference(subtyping,[status(esa)],[c_109]) ).
tcf(c_351,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_of(X0_iProver_pigeon_1))
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(subtyping,[status(esa)],[c_108]) ).
tcf(c_352,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( hole(hole_of(X0_iProver_pigeon_1))
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(subtyping,[status(esa)],[c_107]) ).
tcf(c_353,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( X0_iProver_hole_1 = hole_4 )
| ( X0_iProver_hole_1 = hole_3 )
| ( X0_iProver_hole_1 = hole_2 )
| ( X0_iProver_hole_1 = hole_1 )
| ~ hole(X0_iProver_hole_1) ),
inference(subtyping,[status(esa)],[c_106]) ).
tcf(c_355,plain,
hole_2 != hole_4,
inference(subtyping,[status(esa)],[c_104]) ).
tcf(c_356,plain,
hole_2 != hole_3,
inference(subtyping,[status(esa)],[c_103]) ).
tcf(c_359,plain,
hole_1 != hole_2,
inference(subtyping,[status(esa)],[c_100]) ).
tcf(c_364,plain,
pigeon_4 != pigeon_5,
inference(subtyping,[status(esa)],[c_95]) ).
tcf(c_365,plain,
pigeon_3 != pigeon_5,
inference(subtyping,[status(esa)],[c_94]) ).
tcf(c_366,plain,
pigeon_3 != pigeon_4,
inference(subtyping,[status(esa)],[c_93]) ).
tcf(c_367,plain,
pigeon_2 != pigeon_5,
inference(subtyping,[status(esa)],[c_92]) ).
tcf(c_368,plain,
pigeon_2 != pigeon_4,
inference(subtyping,[status(esa)],[c_91]) ).
tcf(c_369,plain,
pigeon_2 != pigeon_3,
inference(subtyping,[status(esa)],[c_90]) ).
tcf(c_370,plain,
pigeon_1 != pigeon_5,
inference(subtyping,[status(esa)],[c_89]) ).
tcf(c_371,plain,
pigeon_1 != pigeon_4,
inference(subtyping,[status(esa)],[c_88]) ).
tcf(c_372,plain,
pigeon_1 != pigeon_3,
inference(subtyping,[status(esa)],[c_87]) ).
tcf(c_373,plain,
pigeon_1 != pigeon_2,
inference(subtyping,[status(esa)],[c_86]) ).
tcf(c_374,plain,
pigeon(pigeon_5),
inference(subtyping,[status(esa)],[c_85]) ).
tcf(c_375,plain,
pigeon(pigeon_4),
inference(subtyping,[status(esa)],[c_84]) ).
tcf(c_376,plain,
pigeon(pigeon_3),
inference(subtyping,[status(esa)],[c_83]) ).
tcf(c_377,plain,
pigeon(pigeon_2),
inference(subtyping,[status(esa)],[c_82]) ).
tcf(c_378,plain,
pigeon(pigeon_1),
inference(subtyping,[status(esa)],[c_81]) ).
tcf(c_380,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] : X0_iProver_pigeon_1 = X0_iProver_pigeon_1,
theory(equality) ).
tcf(c_381,plain,
! [X0_iProver_hole_1: iProver_hole_1] : X0_iProver_hole_1 = X0_iProver_hole_1,
theory(equality) ).
tcf(c_382,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1,X2_iProver_pigeon_1: iProver_pigeon_1] :
( ( X2_iProver_pigeon_1 = X0_iProver_pigeon_1 )
| ( X2_iProver_pigeon_1 != X1_iProver_pigeon_1 )
| ( X0_iProver_pigeon_1 != X1_iProver_pigeon_1 ) ),
theory(equality) ).
tcf(c_383,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1,X2_iProver_hole_1: iProver_hole_1] :
( ( X2_iProver_hole_1 = X0_iProver_hole_1 )
| ( X2_iProver_hole_1 != X1_iProver_hole_1 )
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
theory(equality) ).
tcf(c_386,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ~ in(X0_iProver_pigeon_1,X1_iProver_hole_1)
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
theory(equality) ).
tcf(c_389,plain,
hole_1 = hole_1,
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_390,plain,
( in(pigeon_1,hole_of(pigeon_1))
| ~ pigeon(pigeon_1) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_391,plain,
( hole(hole_of(pigeon_1))
| ~ pigeon(pigeon_1) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_622,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ~ in(X0_iProver_pigeon_1,hole_of(X0_iProver_pigeon_1))
| ( X0_iProver_hole_1 != hole_of(X0_iProver_pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_634,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_1 = hole_2 )
| ( hole_2 != X0_iProver_hole_1 )
| ( hole_1 != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_635,plain,
( ( hole_1 = hole_2 )
| ( hole_2 != hole_1 )
| ( hole_1 != hole_1 ) ),
inference(instantiation,[status(thm)],[c_634]) ).
tcf(c_636,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_4 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_4)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_4,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_637,plain,
( ( pigeon_4 = pigeon_5 )
| ~ hole(hole_1)
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_4)
| ~ in(pigeon_5,hole_1)
| ~ in(pigeon_4,hole_1) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_640,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_3 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_3)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_3,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_641,plain,
( ( pigeon_3 = pigeon_5 )
| ~ hole(hole_1)
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_3)
| ~ in(pigeon_5,hole_1)
| ~ in(pigeon_3,hole_1) ),
inference(instantiation,[status(thm)],[c_640]) ).
tcf(c_644,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_3 = pigeon_4 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_3)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_4,X0_iProver_hole_1)
| ~ in(pigeon_3,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_645,plain,
( ( pigeon_3 = pigeon_4 )
| ~ hole(hole_1)
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_3)
| ~ in(pigeon_4,hole_1)
| ~ in(pigeon_3,hole_1) ),
inference(instantiation,[status(thm)],[c_644]) ).
tcf(c_648,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_2 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_2)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_2,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_652,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_2 = pigeon_4 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_2)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_4,X0_iProver_hole_1)
| ~ in(pigeon_2,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_656,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_2 = pigeon_3 )
| ~ pigeon(pigeon_3)
| ~ pigeon(pigeon_2)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_3,X0_iProver_hole_1)
| ~ in(pigeon_2,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_660,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_1 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_1)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_1,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_664,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_1 = pigeon_4 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_1)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_4,X0_iProver_hole_1)
| ~ in(pigeon_1,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_668,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_1 = pigeon_3 )
| ~ pigeon(pigeon_3)
| ~ pigeon(pigeon_1)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_3,X0_iProver_hole_1)
| ~ in(pigeon_1,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_672,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( pigeon_1 = pigeon_2 )
| ~ pigeon(pigeon_2)
| ~ pigeon(pigeon_1)
| ~ hole(X0_iProver_hole_1)
| ~ in(pigeon_2,X0_iProver_hole_1)
| ~ in(pigeon_1,X0_iProver_hole_1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_677,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( X1_iProver_hole_1 = hole_of(X0_iProver_pigeon_1) )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_687,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_3 = X0_iProver_hole_1 )
| ( hole_3 != X1_iProver_hole_1 )
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_696,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_2 = X0_iProver_hole_1 )
| ( hole_2 != X1_iProver_hole_1 )
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_697,plain,
( ( pigeon_4 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_4)
| ~ hole(hole_of(pigeon_5))
| ~ in(pigeon_5,hole_of(pigeon_5))
| ~ in(pigeon_4,hole_of(pigeon_5)) ),
inference(instantiation,[status(thm)],[c_636]) ).
tcf(c_706,plain,
( ( pigeon_3 = pigeon_4 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_3)
| ~ hole(hole_of(pigeon_4))
| ~ in(pigeon_4,hole_of(pigeon_4))
| ~ in(pigeon_3,hole_of(pigeon_4)) ),
inference(instantiation,[status(thm)],[c_644]) ).
tcf(c_711,plain,
( ( pigeon_2 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_2)
| ~ hole(hole_of(pigeon_5))
| ~ in(pigeon_5,hole_of(pigeon_5))
| ~ in(pigeon_2,hole_of(pigeon_5)) ),
inference(instantiation,[status(thm)],[c_648]) ).
tcf(c_715,plain,
( ( pigeon_2 = pigeon_4 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_2)
| ~ hole(hole_of(pigeon_4))
| ~ in(pigeon_4,hole_of(pigeon_4))
| ~ in(pigeon_2,hole_of(pigeon_4)) ),
inference(instantiation,[status(thm)],[c_652]) ).
tcf(c_719,plain,
( ( pigeon_2 = pigeon_3 )
| ~ pigeon(pigeon_3)
| ~ pigeon(pigeon_2)
| ~ hole(hole_of(pigeon_3))
| ~ in(pigeon_3,hole_of(pigeon_3))
| ~ in(pigeon_2,hole_of(pigeon_3)) ),
inference(instantiation,[status(thm)],[c_656]) ).
tcf(c_724,plain,
( ( pigeon_1 = pigeon_5 )
| ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_1)
| ~ hole(hole_of(pigeon_5))
| ~ in(pigeon_5,hole_of(pigeon_5))
| ~ in(pigeon_1,hole_of(pigeon_5)) ),
inference(instantiation,[status(thm)],[c_660]) ).
tcf(c_728,plain,
( ( pigeon_1 = pigeon_4 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_1)
| ~ hole(hole_of(pigeon_4))
| ~ in(pigeon_4,hole_of(pigeon_4))
| ~ in(pigeon_1,hole_of(pigeon_4)) ),
inference(instantiation,[status(thm)],[c_664]) ).
tcf(c_732,plain,
( ( pigeon_1 = pigeon_3 )
| ~ pigeon(pigeon_3)
| ~ pigeon(pigeon_1)
| ~ hole(hole_of(pigeon_3))
| ~ in(pigeon_3,hole_of(pigeon_3))
| ~ in(pigeon_1,hole_of(pigeon_3)) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_736,plain,
( ( pigeon_1 = pigeon_2 )
| ~ pigeon(pigeon_2)
| ~ pigeon(pigeon_1)
| ~ hole(hole_of(pigeon_2))
| ~ in(pigeon_2,hole_of(pigeon_2))
| ~ in(pigeon_1,hole_of(pigeon_2)) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_741,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( ( X0_iProver_hole_1 = hole_of(X0_iProver_pigeon_1) )
| ( X0_iProver_hole_1 != hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_677]) ).
tcf(c_743,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_of(X0_iProver_pigeon_1) = X1_iProver_hole_1 )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_748,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_3 = X0_iProver_hole_1 )
| ( hole_3 != hole_3 )
| ( X0_iProver_hole_1 != hole_3 ) ),
inference(instantiation,[status(thm)],[c_687]) ).
tcf(c_751,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_2 = X0_iProver_hole_1 )
| ( hole_2 != hole_2 )
| ( X0_iProver_hole_1 != hole_2 ) ),
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_770,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(X1_iProver_pigeon_1))
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(superposition,[status(thm)],[c_351,c_350]) ).
tcf(c_775,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(X0_iProver_pigeon_1) = hole_4 )
| ( hole_of(X0_iProver_pigeon_1) = hole_3 )
| ( hole_of(X0_iProver_pigeon_1) = hole_2 )
| ( hole_of(X0_iProver_pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(superposition,[status(thm)],[c_352,c_353]) ).
tcf(c_780,plain,
( in(pigeon_5,hole_of(pigeon_5))
| ~ pigeon(pigeon_5) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_782,plain,
( in(pigeon_4,hole_of(pigeon_4))
| ~ pigeon(pigeon_4) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_784,plain,
( ( hole_of(pigeon_1) = hole_4 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(superposition,[status(thm)],[c_378,c_775]) ).
tcf(c_785,plain,
( ( hole_of(pigeon_2) = hole_4 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(superposition,[status(thm)],[c_377,c_775]) ).
tcf(c_786,plain,
( ( hole_of(pigeon_3) = hole_4 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(superposition,[status(thm)],[c_376,c_775]) ).
tcf(c_787,plain,
( ( hole_of(pigeon_4) = hole_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(superposition,[status(thm)],[c_375,c_775]) ).
tcf(c_788,plain,
( ( hole_of(pigeon_5) = hole_4 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 ) ),
inference(superposition,[status(thm)],[c_374,c_775]) ).
tcf(c_789,plain,
( in(pigeon_3,hole_of(pigeon_3))
| ~ pigeon(pigeon_3) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_791,plain,
( in(pigeon_2,hole_of(pigeon_2))
| ~ pigeon(pigeon_2) ),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_802,plain,
( ( hole_2 = hole_4 )
| ( hole_2 = hole_3 )
| ( hole_2 = hole_2 )
| ( hole_2 = hole_1 )
| ~ hole(hole_2) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_819,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_4,X0_iProver_hole_1)
| ~ in(pigeon_4,hole_of(pigeon_4))
| ( X0_iProver_hole_1 != hole_of(pigeon_4) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_820,plain,
( in(pigeon_4,hole_1)
| ~ in(pigeon_4,hole_of(pigeon_4))
| ( hole_1 != hole_of(pigeon_4) ) ),
inference(instantiation,[status(thm)],[c_819]) ).
tcf(c_821,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_5,hole_of(pigeon_5))
| ( X0_iProver_hole_1 != hole_of(pigeon_5) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_822,plain,
( in(pigeon_5,hole_1)
| ~ in(pigeon_5,hole_of(pigeon_5))
| ( hole_1 != hole_of(pigeon_5) ) ),
inference(instantiation,[status(thm)],[c_821]) ).
tcf(c_823,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_3,X0_iProver_hole_1)
| ~ in(pigeon_3,hole_of(pigeon_3))
| ( X0_iProver_hole_1 != hole_of(pigeon_3) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_824,plain,
( in(pigeon_3,hole_1)
| ~ in(pigeon_3,hole_of(pigeon_3))
| ( hole_1 != hole_of(pigeon_3) ) ),
inference(instantiation,[status(thm)],[c_823]) ).
tcf(c_829,plain,
( in(pigeon_1,hole_of(pigeon_5))
| ~ in(pigeon_1,hole_of(pigeon_1))
| ( hole_of(pigeon_5) != hole_of(pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_830,plain,
( in(pigeon_1,hole_of(pigeon_4))
| ~ in(pigeon_1,hole_of(pigeon_1))
| ( hole_of(pigeon_4) != hole_of(pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_831,plain,
( in(pigeon_1,hole_4)
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_784,c_351]) ).
tcf(c_833,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_1))
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_784,c_770]) ).
tcf(c_836,plain,
( hole(hole_of(pigeon_2))
| ~ pigeon(pigeon_2) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_841,plain,
( hole(hole_of(pigeon_3))
| ~ pigeon(pigeon_3) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_842,plain,
( in(pigeon_2,hole_4)
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2) ),
inference(superposition,[status(thm)],[c_785,c_351]) ).
tcf(c_844,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_2))
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_785,c_770]) ).
tcf(c_850,plain,
( hole(hole_of(pigeon_4))
| ~ pigeon(pigeon_4) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_853,plain,
( hole(hole_of(pigeon_5))
| ~ pigeon(pigeon_5) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_866,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_4)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_844,c_82,c_836,c_844]) ).
tcf(c_867,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(renaming,[status(thm)],[c_866]) ).
tcf(c_869,plain,
( in(pigeon_3,hole_4)
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_786,c_351]) ).
tcf(c_871,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_3))
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_786,c_770]) ).
tcf(c_880,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(X0_iProver_pigeon_1) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_743]) ).
tcf(c_884,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_4)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_871,c_83,c_841,c_871]) ).
tcf(c_885,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(renaming,[status(thm)],[c_884]) ).
tcf(c_894,plain,
( in(pigeon_4,hole_4)
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_787,c_351]) ).
tcf(c_896,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_4))
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_787,c_770]) ).
tcf(c_916,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_4)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_896,c_84,c_850,c_896]) ).
tcf(c_917,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(renaming,[status(thm)],[c_916]) ).
tcf(c_922,plain,
( in(pigeon_5,hole_4)
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_788,c_351]) ).
tcf(c_924,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ~ pigeon(pigeon_5)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_5))
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_788,c_770]) ).
tcf(c_988,plain,
( in(pigeon_1,hole_4)
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_831,c_81,c_831]) ).
tcf(c_991,plain,
( ( pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_988,c_917]) ).
tcf(c_993,plain,
( ( pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_988,c_867]) ).
tcf(c_1001,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_2 = hole_of(X0_iProver_pigeon_1) )
| ( hole_2 != hole_2 )
| ( hole_of(X0_iProver_pigeon_1) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_751]) ).
tcf(c_1002,plain,
( ( hole_2 = hole_of(pigeon_1) )
| ( hole_2 != hole_2 )
| ( hole_of(pigeon_1) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1001]) ).
tcf(c_1062,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_3 = hole_of(X0_iProver_pigeon_1) )
| ( hole_3 != hole_3 )
| ( hole_of(X0_iProver_pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_1063,plain,
( ( hole_3 = hole_of(pigeon_1) )
| ( hole_3 != hole_3 )
| ( hole_of(pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_1062]) ).
tcf(c_1070,plain,
( in(pigeon_2,hole_4)
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_842,c_82,c_842]) ).
tcf(c_1073,plain,
( ( pigeon_2 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2) ),
inference(superposition,[status(thm)],[c_1070,c_917]) ).
tcf(c_1074,plain,
( ( pigeon_2 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2) ),
inference(superposition,[status(thm)],[c_1070,c_885]) ).
tcf(c_1116,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( X0_iProver_hole_1 = hole_of(pigeon_4) )
| ( X0_iProver_hole_1 != hole_1 )
| ( hole_of(pigeon_4) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_1117,plain,
( ( hole_1 = hole_of(pigeon_4) )
| ( hole_1 != hole_1 )
| ( hole_of(pigeon_4) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_1116]) ).
tcf(c_1118,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( X0_iProver_hole_1 = hole_of(pigeon_5) )
| ( X0_iProver_hole_1 != hole_1 )
| ( hole_of(pigeon_5) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_1119,plain,
( ( hole_1 = hole_of(pigeon_5) )
| ( hole_1 != hole_1 )
| ( hole_of(pigeon_5) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_1118]) ).
tcf(c_1120,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( X0_iProver_hole_1 = hole_of(pigeon_3) )
| ( X0_iProver_hole_1 != hole_1 )
| ( hole_of(pigeon_3) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_1121,plain,
( ( hole_1 = hole_of(pigeon_3) )
| ( hole_1 != hole_1 )
| ( hole_of(pigeon_3) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_1120]) ).
tcf(c_1124,plain,
( ( hole_of(pigeon_5) = hole_of(pigeon_1) )
| ( hole_of(pigeon_5) != hole_1 )
| ( hole_of(pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_1125,plain,
( ( hole_of(pigeon_4) = hole_of(pigeon_1) )
| ( hole_of(pigeon_4) != hole_1 )
| ( hole_of(pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_741]) ).
tcf(c_1138,plain,
( in(pigeon_1,hole_of(pigeon_3))
| ~ in(pigeon_1,hole_of(pigeon_1))
| ( hole_of(pigeon_3) != hole_of(pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_1139,plain,
( in(pigeon_1,hole_of(pigeon_2))
| ~ in(pigeon_1,hole_of(pigeon_1))
| ( hole_of(pigeon_2) != hole_of(pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_1153,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(X1_iProver_pigeon_1))
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(superposition,[status(thm)],[c_351,c_350]) ).
tcf(c_1158,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(X0_iProver_pigeon_1) = hole_4 )
| ( hole_of(X0_iProver_pigeon_1) = hole_3 )
| ( hole_of(X0_iProver_pigeon_1) = hole_2 )
| ( hole_of(X0_iProver_pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(superposition,[status(thm)],[c_352,c_353]) ).
tcf(c_1159,plain,
( ( hole_of(pigeon_1) = hole_4 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(superposition,[status(thm)],[c_378,c_1158]) ).
tcf(c_1160,plain,
( ( hole_of(pigeon_2) = hole_4 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(superposition,[status(thm)],[c_377,c_1158]) ).
tcf(c_1161,plain,
( ( hole_of(pigeon_3) = hole_4 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(superposition,[status(thm)],[c_376,c_1158]) ).
tcf(c_1162,plain,
( ( hole_of(pigeon_4) = hole_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(superposition,[status(thm)],[c_375,c_1158]) ).
tcf(c_1163,plain,
( ( hole_of(pigeon_5) = hole_4 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 ) ),
inference(superposition,[status(thm)],[c_374,c_1158]) ).
tcf(c_1164,plain,
( in(pigeon_1,hole_4)
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_1159,c_351]) ).
tcf(c_1166,plain,
( in(pigeon_1,hole_4)
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1164,c_988]) ).
tcf(c_1168,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_1166,c_350]) ).
tcf(c_1171,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_1168,c_81,c_391,c_833]) ).
tcf(c_1176,plain,
( in(pigeon_2,hole_4)
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2) ),
inference(superposition,[status(thm)],[c_1160,c_351]) ).
tcf(c_1178,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_2))
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_1160,c_1153]) ).
tcf(c_1179,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_4)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_1178,c_82,c_836,c_844]) ).
tcf(c_1180,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(renaming,[status(thm)],[c_1179]) ).
tcf(c_1181,plain,
( ( pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_1166,c_1180]) ).
tcf(c_1182,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1181,c_81,c_373,c_993]) ).
tcf(c_1183,plain,
( ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_1182]) ).
tcf(c_1187,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_2)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_2))
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_1183,c_1153]) ).
tcf(c_1190,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_3)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_1187,c_82,c_836,c_1187]) ).
tcf(c_1191,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(renaming,[status(thm)],[c_1190]) ).
tcf(c_1198,plain,
( in(pigeon_3,hole_4)
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_1161,c_351]) ).
tcf(c_1201,plain,
( in(pigeon_4,hole_4)
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_1162,c_351]) ).
tcf(c_1204,plain,
( in(pigeon_5,hole_4)
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_1163,c_351]) ).
tcf(c_1207,plain,
( in(pigeon_2,hole_4)
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1176,c_1070]) ).
tcf(c_1212,plain,
( in(pigeon_3,hole_4)
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1198,c_83,c_869]) ).
tcf(c_1214,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_1212,c_350]) ).
tcf(c_1215,plain,
( ( pigeon_2 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_1212,c_1180]) ).
tcf(c_1216,plain,
( ( pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_1212,c_1171]) ).
tcf(c_1247,plain,
( in(pigeon_4,hole_4)
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1201,c_84,c_894]) ).
tcf(c_1249,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_1247,c_350]) ).
tcf(c_1253,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] : hole_of(X0_iProver_pigeon_1) = hole_of(X0_iProver_pigeon_1),
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_1276,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(X0_iProver_pigeon_1) = hole_of(pigeon_3) )
| ( hole_of(pigeon_3) != hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_880]) ).
tcf(c_1277,plain,
( ( hole_of(pigeon_1) = hole_of(pigeon_3) )
| ( hole_of(pigeon_3) != hole_1 )
| ( hole_of(pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_1276]) ).
tcf(c_1278,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(X0_iProver_pigeon_1) = hole_of(pigeon_2) )
| ( hole_of(pigeon_2) != hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_880]) ).
tcf(c_1279,plain,
( ( hole_of(pigeon_1) = hole_of(pigeon_2) )
| ( hole_of(pigeon_2) != hole_1 )
| ( hole_of(pigeon_1) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_1278]) ).
tcf(c_1284,plain,
( in(pigeon_5,hole_4)
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1204,c_85,c_922]) ).
tcf(c_1286,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_5)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_1284,c_350]) ).
tcf(c_1287,plain,
( ( pigeon_2 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_1284,c_1180]) ).
tcf(c_1288,plain,
( ( pigeon_1 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_1284,c_1171]) ).
tcf(c_1306,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_1214,c_885]) ).
tcf(c_1311,plain,
( ( pigeon_3 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_1247,c_1306]) ).
tcf(c_1312,plain,
( ( pigeon_3 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_1284,c_1306]) ).
tcf(c_1394,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X1_iProver_pigeon_1 = X0_iProver_pigeon_1 )
| ( X0_iProver_pigeon_1 != X1_iProver_pigeon_1 ) ),
inference(resolution,[status(thm)],[c_382,c_380]) ).
tcf(c_1433,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_1249,c_917]) ).
tcf(c_1435,plain,
( ( pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_1166,c_1433]) ).
tcf(c_1436,plain,
( ( pigeon_2 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2) ),
inference(superposition,[status(thm)],[c_1207,c_1433]) ).
tcf(c_1439,plain,
( ( pigeon_4 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_1284,c_1433]) ).
tcf(c_1577,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_1286,c_85,c_853,c_924]) ).
tcf(c_1580,plain,
( ( pigeon_1 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_1166,c_1577]) ).
tcf(c_1619,plain,
hole_of(pigeon_3) = hole_of(pigeon_3),
inference(instantiation,[status(thm)],[c_1253]) ).
tcf(c_1620,plain,
hole_of(pigeon_2) = hole_of(pigeon_2),
inference(instantiation,[status(thm)],[c_1253]) ).
tcf(c_1637,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1216,c_83,c_372,c_1216]) ).
tcf(c_1638,plain,
( ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_1637]) ).
tcf(c_1640,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_1638,c_351]) ).
tcf(c_1642,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_3))
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_1638,c_1153]) ).
tcf(c_1675,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_1640,c_83,c_1640]) ).
tcf(c_1678,plain,
( ( pigeon_2 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_1675,c_1191]) ).
tcf(c_1692,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(X1_iProver_pigeon_1))
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(resolution,[status(thm)],[c_350,c_351]) ).
tcf(c_1698,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1692,c_352]) ).
tcf(c_1722,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X1_iProver_pigeon_1 = X0_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(resolution,[status(thm)],[c_1698,c_1394]) ).
tcf(c_1749,plain,
hole_3 = hole_3,
inference(instantiation,[status(thm)],[c_381]) ).
tcf(c_1817,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_2 = X0_iProver_hole_1 )
| ( hole_2 != X1_iProver_hole_1 )
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_1818,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_5,X1_iProver_hole_1)
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1828,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( in(pigeon_4,X0_iProver_hole_1)
| ~ in(pigeon_4,X1_iProver_hole_1)
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1843,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( in(pigeon_3,X0_iProver_hole_1)
| ~ in(pigeon_3,X1_iProver_hole_1)
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1863,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( in(pigeon_2,X0_iProver_hole_1)
| ~ in(pigeon_2,X1_iProver_hole_1)
| ( X0_iProver_hole_1 != X1_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1875,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_2 = X0_iProver_hole_1 )
| ( hole_2 != hole_2 )
| ( X0_iProver_hole_1 != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1817]) ).
tcf(c_1878,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_5,X0_iProver_hole_1)
| ~ in(pigeon_5,hole_of(pigeon_5))
| ( X0_iProver_hole_1 != hole_of(pigeon_5) ) ),
inference(instantiation,[status(thm)],[c_1818]) ).
tcf(c_1885,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_4,X0_iProver_hole_1)
| ~ in(pigeon_4,hole_of(pigeon_4))
| ( X0_iProver_hole_1 != hole_of(pigeon_4) ) ),
inference(instantiation,[status(thm)],[c_1828]) ).
tcf(c_1892,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_3,X0_iProver_hole_1)
| ~ in(pigeon_3,hole_of(pigeon_3))
| ( X0_iProver_hole_1 != hole_of(pigeon_3) ) ),
inference(instantiation,[status(thm)],[c_1843]) ).
tcf(c_1899,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_2,X0_iProver_hole_1)
| ~ in(pigeon_2,hole_of(pigeon_2))
| ( X0_iProver_hole_1 != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_1863]) ).
tcf(c_1911,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_1,hole_of(pigeon_5))
| ~ in(pigeon_1,X0_iProver_hole_1)
| ( hole_of(pigeon_5) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1912,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( in(pigeon_1,hole_of(pigeon_4))
| ~ in(pigeon_1,X0_iProver_hole_1)
| ( hole_of(pigeon_4) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1929,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_5))
| ~ in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ( hole_of(pigeon_5) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1933,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_4))
| ~ in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ( hole_of(pigeon_4) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1936,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( X1_iProver_hole_1 = hole_of(pigeon_3) )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(pigeon_3) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_1937,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_3))
| ~ in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ( hole_of(pigeon_3) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_1940,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( X1_iProver_hole_1 = hole_of(pigeon_2) )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(pigeon_2) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_1945,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_5) = X1_iProver_hole_1 )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(pigeon_5) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_1948,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_4) = X1_iProver_hole_1 )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(pigeon_4) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_1951,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_3) = X1_iProver_hole_1 )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(pigeon_3) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_1954,plain,
! [X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_2) = X1_iProver_hole_1 )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(pigeon_2) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_2025,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_2) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_of(pigeon_2) )
| ( hole_of(pigeon_2) != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_1954]) ).
tcf(c_2135,plain,
( ( hole_2 = hole_of(pigeon_5) )
| ( hole_2 != hole_2 )
| ( hole_of(pigeon_5) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2136,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_5) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_2 )
| ( hole_of(pigeon_5) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1945]) ).
tcf(c_2137,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_5))
| ~ in(X0_iProver_pigeon_1,hole_2)
| ( hole_of(pigeon_5) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1929]) ).
tcf(c_2139,plain,
( in(pigeon_1,hole_of(pigeon_5))
| ~ in(pigeon_1,hole_2)
| ( hole_of(pigeon_5) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1911]) ).
tcf(c_2140,plain,
( ( hole_2 = hole_of(pigeon_4) )
| ( hole_2 != hole_2 )
| ( hole_of(pigeon_4) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2141,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_4) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_2 )
| ( hole_of(pigeon_4) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1948]) ).
tcf(c_2142,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_4))
| ~ in(X0_iProver_pigeon_1,hole_2)
| ( hole_of(pigeon_4) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1933]) ).
tcf(c_2144,plain,
( in(pigeon_1,hole_of(pigeon_4))
| ~ in(pigeon_1,hole_2)
| ( hole_of(pigeon_4) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1912]) ).
tcf(c_2147,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_3))
| ~ in(X0_iProver_pigeon_1,hole_2)
| ( hole_of(pigeon_3) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1937]) ).
tcf(c_2150,plain,
( ( hole_2 = hole_of(pigeon_2) )
| ( hole_2 != hole_2 )
| ( hole_of(pigeon_2) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_2157,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_5) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_3 )
| ( hole_of(pigeon_5) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_1945]) ).
tcf(c_2161,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,hole_2)
| ~ in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ( hole_2 != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_2166,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_4) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_3 )
| ( hole_of(pigeon_4) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_1948]) ).
tcf(c_2170,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( in(X0_iProver_pigeon_1,X0_iProver_hole_1)
| ~ in(X0_iProver_pigeon_1,hole_of(X0_iProver_pigeon_1))
| ( X0_iProver_hole_1 != hole_of(X0_iProver_pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_2174,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_3) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_3 )
| ( hole_of(pigeon_3) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_1951]) ).
tcf(c_2175,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_of(pigeon_3))
| ~ in(X0_iProver_pigeon_1,hole_3)
| ( hole_of(pigeon_3) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_1937]) ).
tcf(c_2176,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( X0_iProver_hole_1 = hole_of(pigeon_3) )
| ( X0_iProver_hole_1 != hole_3 )
| ( hole_of(pigeon_3) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_1936]) ).
tcf(c_2191,plain,
( in(pigeon_5,hole_2)
| ~ in(pigeon_5,hole_of(pigeon_5))
| ( hole_2 != hole_of(pigeon_5) ) ),
inference(instantiation,[status(thm)],[c_1878]) ).
tcf(c_2197,plain,
( in(pigeon_4,hole_2)
| ~ in(pigeon_4,hole_of(pigeon_4))
| ( hole_2 != hole_of(pigeon_4) ) ),
inference(instantiation,[status(thm)],[c_1885]) ).
tcf(c_2223,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1,X1_iProver_hole_1: iProver_hole_1] :
( ( X1_iProver_hole_1 = hole_of(X0_iProver_pigeon_1) )
| ( X1_iProver_hole_1 != X0_iProver_hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_2228,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_3) = X0_iProver_hole_1 )
| ( X0_iProver_hole_1 != hole_4 )
| ( hole_of(pigeon_3) != hole_4 ) ),
inference(instantiation,[status(thm)],[c_1951]) ).
tcf(c_2246,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_3) = hole_of(pigeon_2) )
| ( hole_of(pigeon_3) != X0_iProver_hole_1 )
| ( hole_of(pigeon_2) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_1940]) ).
tcf(c_2247,plain,
( ( hole_of(pigeon_3) = hole_of(pigeon_2) )
| ( hole_of(pigeon_3) != hole_1 )
| ( hole_of(pigeon_2) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_2246]) ).
tcf(c_2248,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_4) = hole_of(pigeon_2) )
| ( hole_of(pigeon_4) != X0_iProver_hole_1 )
| ( hole_of(pigeon_2) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_1940]) ).
tcf(c_2249,plain,
( ( hole_of(pigeon_4) = hole_of(pigeon_2) )
| ( hole_of(pigeon_4) != hole_1 )
| ( hole_of(pigeon_2) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_2248]) ).
tcf(c_2250,plain,
! [X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_5) = hole_of(pigeon_2) )
| ( hole_of(pigeon_5) != X0_iProver_hole_1 )
| ( hole_of(pigeon_2) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_1940]) ).
tcf(c_2251,plain,
( ( hole_of(pigeon_5) = hole_of(pigeon_2) )
| ( hole_of(pigeon_5) != hole_1 )
| ( hole_of(pigeon_2) != hole_1 ) ),
inference(instantiation,[status(thm)],[c_2250]) ).
tcf(c_2253,plain,
( in(pigeon_2,hole_2)
| ~ in(pigeon_2,hole_of(pigeon_2))
| ( hole_2 != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_1899]) ).
tcf(c_2255,plain,
( in(pigeon_2,hole_of(pigeon_5))
| ~ in(pigeon_2,hole_of(pigeon_2))
| ( hole_of(pigeon_5) != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_1899]) ).
tcf(c_2256,plain,
( in(pigeon_2,hole_of(pigeon_4))
| ~ in(pigeon_2,hole_of(pigeon_2))
| ( hole_of(pigeon_4) != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_1899]) ).
tcf(c_2257,plain,
( in(pigeon_2,hole_of(pigeon_3))
| ~ in(pigeon_2,hole_of(pigeon_2))
| ( hole_of(pigeon_3) != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_1899]) ).
tcf(c_2288,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_2) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_2) != hole_of(pigeon_2) )
| ( hole_of(X0_iProver_pigeon_1) != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_2025]) ).
tcf(c_2289,plain,
( ( hole_of(pigeon_2) = hole_of(pigeon_1) )
| ( hole_of(pigeon_2) != hole_of(pigeon_2) )
| ( hole_of(pigeon_1) != hole_of(pigeon_2) ) ),
inference(instantiation,[status(thm)],[c_2288]) ).
tcf(c_2320,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_2) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_2) != X0_iProver_hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_1954]) ).
tcf(c_2356,plain,
( ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1215,c_82,c_369,c_1074]) ).
tcf(c_2357,plain,
( ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2356]) ).
tcf(c_2359,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2357,c_351]) ).
tcf(c_2364,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_2)
| ~ in(X0_iProver_pigeon_1,hole_of(X0_iProver_pigeon_1))
| ( hole_2 != hole_of(X0_iProver_pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_2161]) ).
tcf(c_2365,plain,
( in(pigeon_1,hole_2)
| ~ in(pigeon_1,hole_of(pigeon_1))
| ( hole_2 != hole_of(pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_2364]) ).
tcf(c_2388,plain,
( in(pigeon_5,hole_of(pigeon_3))
| ~ in(pigeon_5,hole_2)
| ( hole_of(pigeon_3) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2147]) ).
tcf(c_2389,plain,
( in(pigeon_5,hole_of(pigeon_4))
| ~ in(pigeon_5,hole_2)
| ( hole_of(pigeon_4) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2142]) ).
tcf(c_2399,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2359,c_83,c_2359]) ).
tcf(c_2401,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ hole(hole_3)
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2399,c_350]) ).
tcf(c_2409,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1435,c_81,c_371,c_991]) ).
tcf(c_2410,plain,
( ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2409]) ).
tcf(c_2412,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2410,c_351]) ).
tcf(c_2414,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_4))
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2410,c_1153]) ).
tcf(c_2430,plain,
( ( hole_of(pigeon_4) = hole_of(pigeon_2) )
| ( hole_of(pigeon_4) != hole_2 )
| ( hole_of(pigeon_2) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2141]) ).
tcf(c_2447,plain,
( ( hole_of(pigeon_5) = hole_of(pigeon_2) )
| ( hole_of(pigeon_5) != hole_3 )
| ( hole_of(pigeon_2) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2157]) ).
tcf(c_2449,plain,
( ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1436,c_82,c_368,c_1073]) ).
tcf(c_2450,plain,
( ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2449]) ).
tcf(c_2452,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2450,c_351]) ).
tcf(c_2454,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_4))
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2450,c_1153]) ).
tcf(c_2481,plain,
( in(pigeon_4,hole_of(pigeon_3))
| ~ in(pigeon_4,hole_2)
| ( hole_of(pigeon_3) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2147]) ).
tcf(c_2483,plain,
( in(pigeon_4,hole_of(pigeon_5))
| ~ in(pigeon_4,hole_2)
| ( hole_of(pigeon_5) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2137]) ).
tcf(c_2491,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(global_subsumption_just,[status(thm)],[c_2401,c_98,c_83,c_2401]) ).
tcf(c_2499,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1288,c_81,c_370,c_1580]) ).
tcf(c_2500,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2499]) ).
tcf(c_2502,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2500,c_351]) ).
tcf(c_2507,plain,
( ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1311,c_84,c_366,c_1311]) ).
tcf(c_2508,plain,
( ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2507]) ).
tcf(c_2510,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2508,c_351]) ).
tcf(c_2512,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(pigeon_4))
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2508,c_1153]) ).
tcf(c_2532,plain,
( ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1312,c_85,c_365,c_1312]) ).
tcf(c_2533,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2532]) ).
tcf(c_2535,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2533,c_351]) ).
tcf(c_2567,plain,
( ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1439,c_85,c_364,c_1439]) ).
tcf(c_2568,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2567]) ).
tcf(c_2570,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2568,c_351]) ).
tcf(c_2583,plain,
( ( hole_of(pigeon_3) = hole_of(pigeon_2) )
| ( hole_of(pigeon_3) != hole_4 )
| ( hole_of(pigeon_2) != hole_4 ) ),
inference(instantiation,[status(thm)],[c_2228]) ).
tcf(c_2697,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ hole(hole_of(X1_iProver_pigeon_1))
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(superposition,[status(thm)],[c_351,c_350]) ).
tcf(c_2702,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(X0_iProver_pigeon_1) = hole_4 )
| ( hole_of(X0_iProver_pigeon_1) = hole_3 )
| ( hole_of(X0_iProver_pigeon_1) = hole_2 )
| ( hole_of(X0_iProver_pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(superposition,[status(thm)],[c_352,c_353]) ).
tcf(c_2703,plain,
( ( hole_of(pigeon_1) = hole_4 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(superposition,[status(thm)],[c_378,c_2702]) ).
tcf(c_2704,plain,
( ( hole_of(pigeon_2) = hole_4 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(superposition,[status(thm)],[c_377,c_2702]) ).
tcf(c_2705,plain,
( ( hole_of(pigeon_3) = hole_4 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(superposition,[status(thm)],[c_376,c_2702]) ).
tcf(c_2706,plain,
( ( hole_of(pigeon_4) = hole_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(superposition,[status(thm)],[c_375,c_2702]) ).
tcf(c_2707,plain,
( ( hole_of(pigeon_5) = hole_4 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 ) ),
inference(superposition,[status(thm)],[c_374,c_2702]) ).
tcf(c_2708,plain,
( in(pigeon_1,hole_4)
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_2703,c_351]) ).
tcf(c_2710,plain,
( in(pigeon_1,hole_4)
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2708,c_988]) ).
tcf(c_2712,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_2710,c_350]) ).
tcf(c_2713,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X1_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = X1_iProver_pigeon_1 )
| ~ pigeon(X1_iProver_pigeon_1)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_of(X1_iProver_pigeon_1)) ),
inference(global_subsumption_just,[status(thm)],[c_2697,c_1698]) ).
tcf(c_2717,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_2712,c_81,c_391,c_833]) ).
tcf(c_2724,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_2)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_2704,c_2713]) ).
tcf(c_2726,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_4)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_2724,c_82,c_836,c_844]) ).
tcf(c_2727,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(renaming,[status(thm)],[c_2726]) ).
tcf(c_2728,plain,
( ( pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_1) ),
inference(superposition,[status(thm)],[c_2710,c_2727]) ).
tcf(c_2729,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2728,c_1183]) ).
tcf(c_2730,plain,
( ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2729]) ).
tcf(c_2734,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_2)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2730,c_2713]) ).
tcf(c_2737,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ in(X0_iProver_pigeon_1,hole_3)
| ~ pigeon(X0_iProver_pigeon_1) ),
inference(global_subsumption_just,[status(thm)],[c_2734,c_82,c_836,c_1187]) ).
tcf(c_2738,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(renaming,[status(thm)],[c_2737]) ).
tcf(c_2743,plain,
( in(pigeon_3,hole_4)
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2705,c_351]) ).
tcf(c_2747,plain,
( in(pigeon_4,hole_4)
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2706,c_351]) ).
tcf(c_2751,plain,
( in(pigeon_5,hole_4)
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2707,c_351]) ).
tcf(c_2760,plain,
( in(pigeon_3,hole_4)
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2743,c_1212]) ).
tcf(c_2762,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_2760,c_350]) ).
tcf(c_2763,plain,
( ( pigeon_2 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2760,c_2727]) ).
tcf(c_2764,plain,
( ( pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2760,c_2717]) ).
tcf(c_2765,plain,
( in(pigeon_4,hole_4)
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2747,c_1247]) ).
tcf(c_2767,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ hole(hole_4)
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(superposition,[status(thm)],[c_2765,c_350]) ).
tcf(c_2768,plain,
( ( pigeon_2 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2765,c_2727]) ).
tcf(c_2769,plain,
( ( pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2765,c_2717]) ).
tcf(c_2770,plain,
( in(pigeon_5,hole_4)
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2751,c_1284]) ).
tcf(c_2773,plain,
( ( pigeon_2 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2770,c_2727]) ).
tcf(c_2774,plain,
( ( pigeon_1 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2770,c_2717]) ).
tcf(c_2777,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_2762,c_83,c_841,c_871]) ).
tcf(c_2782,plain,
( ( pigeon_3 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2765,c_2777]) ).
tcf(c_2783,plain,
( ( pigeon_3 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2770,c_2777]) ).
tcf(c_2784,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_4) ),
inference(global_subsumption_just,[status(thm)],[c_2767,c_84,c_850,c_896]) ).
tcf(c_2790,plain,
( ( pigeon_4 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2770,c_2784]) ).
tcf(c_2806,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2764,c_1638]) ).
tcf(c_2807,plain,
( ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2806]) ).
tcf(c_2809,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2807,c_351]) ).
tcf(c_2814,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2809,c_1675]) ).
tcf(c_2816,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ hole(hole_3)
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2814,c_350]) ).
tcf(c_2817,plain,
( ( pigeon_2 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2814,c_2738]) ).
tcf(c_2818,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(global_subsumption_just,[status(thm)],[c_2816,c_83,c_841,c_1642]) ).
tcf(c_2822,plain,
( ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2763,c_83,c_82,c_369,c_719,c_786,c_785,c_789,c_791,c_841,c_2257,c_2583]) ).
tcf(c_2823,plain,
( ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2822]) ).
tcf(c_2825,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_3) ),
inference(superposition,[status(thm)],[c_2823,c_351]) ).
tcf(c_2830,plain,
( in(pigeon_3,hole_3)
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2825,c_83,c_2359]) ).
tcf(c_2832,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ hole(hole_3)
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2830,c_350]) ).
tcf(c_2835,plain,
( ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2768,c_2450]) ).
tcf(c_2836,plain,
( ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2835]) ).
tcf(c_2838,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2836,c_351]) ).
tcf(c_2840,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2836,c_2713]) ).
tcf(c_2842,plain,
( ( pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_1)
| ~ in(pigeon_1,hole_3) ),
inference(instantiation,[status(thm)],[c_2840]) ).
tcf(c_2843,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2838,c_84,c_2452]) ).
tcf(c_2845,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ hole(hole_3)
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2843,c_350]) ).
tcf(c_2849,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2769,c_2410]) ).
tcf(c_2850,plain,
( ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2849]) ).
tcf(c_2852,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2850,c_351]) ).
tcf(c_2857,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2852,c_84,c_2412]) ).
tcf(c_2859,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ hole(hole_3)
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_2857,c_350]) ).
tcf(c_2860,plain,
( ( pigeon_3 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2857,c_2818]) ).
tcf(c_2861,plain,
( ( pigeon_2 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2857,c_2738]) ).
tcf(c_2863,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(global_subsumption_just,[status(thm)],[c_2832,c_2491]) ).
tcf(c_2869,plain,
( ( pigeon_3 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2843,c_2863]) ).
tcf(c_2870,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(global_subsumption_just,[status(thm)],[c_2845,c_84,c_850,c_2454]) ).
tcf(c_2878,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(global_subsumption_just,[status(thm)],[c_2859,c_84,c_850,c_2414]) ).
tcf(c_2886,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2774,c_81,c_370,c_1580]) ).
tcf(c_2887,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2886]) ).
tcf(c_2889,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_2887,c_351]) ).
tcf(c_2938,plain,
( ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2782,c_2508]) ).
tcf(c_2939,plain,
( ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(renaming,[status(thm)],[c_2938]) ).
tcf(c_2941,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_4) ),
inference(superposition,[status(thm)],[c_2939,c_351]) ).
tcf(c_3059,plain,
( ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_4)
| ~ in(pigeon_5,hole_of(pigeon_4)) ),
inference(resolution,[status(thm)],[c_1722,c_364]) ).
tcf(c_3060,plain,
( ~ pigeon(pigeon_5)
| ~ pigeon(pigeon_3)
| ~ in(pigeon_5,hole_of(pigeon_3)) ),
inference(resolution,[status(thm)],[c_1722,c_365]) ).
tcf(c_3061,plain,
( ~ pigeon(pigeon_4)
| ~ pigeon(pigeon_3)
| ~ in(pigeon_4,hole_of(pigeon_3)) ),
inference(resolution,[status(thm)],[c_1722,c_366]) ).
tcf(c_3108,plain,
( ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2783,c_2533]) ).
tcf(c_3109,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(renaming,[status(thm)],[c_3108]) ).
tcf(c_3111,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3109,c_351]) ).
tcf(c_3127,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2889,c_85,c_2502]) ).
tcf(c_3130,plain,
( ( pigeon_4 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3127,c_2878]) ).
tcf(c_3133,plain,
( ( pigeon_3 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3127,c_2818]) ).
tcf(c_3134,plain,
( ( pigeon_2 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_3 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3127,c_2738]) ).
tcf(c_3274,plain,
( in(pigeon_5,hole_of(pigeon_3))
| ~ in(pigeon_5,hole_3)
| ( hole_of(pigeon_3) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2175]) ).
tcf(c_3285,plain,
( in(pigeon_4,hole_3)
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_2941,c_84,c_2510]) ).
tcf(c_3287,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ hole(hole_3)
| ~ pigeon(pigeon_4)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(superposition,[status(thm)],[c_3285,c_350]) ).
tcf(c_3412,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_3111,c_85,c_2535]) ).
tcf(c_3422,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_5) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_5) != hole_3 )
| ( hole_of(X0_iProver_pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2157]) ).
tcf(c_3424,plain,
( ( hole_of(pigeon_5) = hole_of(pigeon_1) )
| ( hole_of(pigeon_5) != hole_3 )
| ( hole_of(pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_3422]) ).
tcf(c_3429,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_2) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_2) != hole_3 )
| ( hole_of(X0_iProver_pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2320]) ).
tcf(c_3431,plain,
( ( hole_of(pigeon_2) = hole_of(pigeon_1) )
| ( hole_of(pigeon_2) != hole_3 )
| ( hole_of(pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_3429]) ).
tcf(c_3475,plain,
( ( hole_of(pigeon_3) = hole_of(pigeon_2) )
| ( hole_of(pigeon_3) != hole_3 )
| ( hole_of(pigeon_2) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2246]) ).
tcf(c_3483,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_3) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_3) != hole_3 )
| ( hole_of(X0_iProver_pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2174]) ).
tcf(c_3484,plain,
( ( hole_of(pigeon_3) = hole_of(pigeon_1) )
| ( hole_of(pigeon_3) != hole_3 )
| ( hole_of(pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_3483]) ).
tcf(c_3504,plain,
( ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2773,c_85,c_367,c_1287]) ).
tcf(c_3505,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(renaming,[status(thm)],[c_3504]) ).
tcf(c_3507,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3505,c_351]) ).
tcf(c_3563,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_4 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_3) ),
inference(global_subsumption_just,[status(thm)],[c_3287,c_84,c_850,c_2512]) ).
tcf(c_3572,plain,
( ( pigeon_4 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3412,c_3563]) ).
tcf(c_3697,plain,
( ( hole_of(pigeon_4) = hole_of(pigeon_2) )
| ( hole_of(pigeon_4) != hole_3 )
| ( hole_of(pigeon_2) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2248]) ).
tcf(c_3716,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_4) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_4) != hole_3 )
| ( hole_of(X0_iProver_pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2166]) ).
tcf(c_3717,plain,
( ( hole_of(pigeon_4) = hole_of(pigeon_1) )
| ( hole_of(pigeon_4) != hole_3 )
| ( hole_of(pigeon_1) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_3716]) ).
tcf(c_3749,plain,
( ( hole_of(pigeon_4) = hole_of(pigeon_3) )
| ( hole_of(pigeon_4) != hole_3 )
| ( hole_of(pigeon_3) != hole_3 ) ),
inference(instantiation,[status(thm)],[c_2176]) ).
tcf(c_3764,plain,
( ( hole_of(pigeon_5) = hole_of(pigeon_2) )
| ( hole_of(pigeon_5) != hole_2 )
| ( hole_of(pigeon_2) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2136]) ).
tcf(c_3811,plain,
( in(pigeon_2,hole_of(pigeon_3))
| ~ in(pigeon_2,hole_2)
| ( hole_of(pigeon_3) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2147]) ).
tcf(c_3820,plain,
( ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_2790,c_2568]) ).
tcf(c_3821,plain,
( ( hole_of(pigeon_5) = hole_3 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(renaming,[status(thm)],[c_3820]) ).
tcf(c_3823,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3821,c_351]) ).
tcf(c_3906,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_3507,c_85,c_3507]) ).
tcf(c_3913,plain,
( ( pigeon_4 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3906,c_2870]) ).
tcf(c_3914,plain,
( ( pigeon_3 = pigeon_5 )
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ~ pigeon(pigeon_5) ),
inference(superposition,[status(thm)],[c_3906,c_2863]) ).
tcf(c_3935,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( in(X0_iProver_pigeon_1,hole_3)
| ~ in(X0_iProver_pigeon_1,hole_of(X0_iProver_pigeon_1))
| ( hole_3 != hole_of(X0_iProver_pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_2170]) ).
tcf(c_3936,plain,
( in(pigeon_1,hole_3)
| ~ in(pigeon_1,hole_of(pigeon_1))
| ( hole_3 != hole_of(pigeon_1) ) ),
inference(instantiation,[status(thm)],[c_3935]) ).
tcf(c_3998,plain,
( in(pigeon_5,hole_3)
| ( hole_of(pigeon_5) = hole_2 )
| ( hole_of(pigeon_5) = hole_1 )
| ( hole_of(pigeon_4) = hole_3 )
| ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_3823,c_85,c_2570]) ).
tcf(c_4049,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1,X0_iProver_hole_1: iProver_hole_1] :
( ( hole_of(pigeon_3) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_3) != X0_iProver_hole_1 )
| ( hole_of(X0_iProver_pigeon_1) != X0_iProver_hole_1 ) ),
inference(instantiation,[status(thm)],[c_2223]) ).
tcf(c_4087,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_2) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_2) != hole_2 )
| ( hole_of(X0_iProver_pigeon_1) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_2320]) ).
tcf(c_4088,plain,
( ( hole_of(pigeon_2) = hole_of(pigeon_1) )
| ( hole_of(pigeon_2) != hole_2 )
| ( hole_of(pigeon_1) != hole_2 ) ),
inference(instantiation,[status(thm)],[c_4087]) ).
tcf(c_4258,plain,
( ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2817,c_83,c_82,c_81,c_390,c_369,c_372,c_373,c_732,c_736,c_789,c_791,c_836,c_841,c_1138,c_1139,c_1215,c_1678,c_3431,c_3484]) ).
tcf(c_4259,plain,
( ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_4258]) ).
tcf(c_4266,plain,
( ( hole_2 = hole_3 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(superposition,[status(thm)],[c_4259,c_2823]) ).
tcf(c_4726,plain,
( ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_4) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2860,c_84,c_83,c_81,c_390,c_366,c_371,c_372,c_728,c_732,c_782,c_789,c_830,c_841,c_850,c_1138,c_1311,c_2860,c_3484,c_3717]) ).
tcf(c_4727,plain,
( ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_4726]) ).
tcf(c_4728,plain,
( ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_4727,c_97,c_96,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_364,c_365,c_367,c_368,c_370,c_372,c_635,c_637,c_697,c_711,c_715,c_724,c_732,c_780,c_782,c_789,c_791,c_802,c_820,c_822,c_829,c_841,c_850,c_853,c_1117,c_1119,c_1138,c_2140,c_2197,c_2249,c_2251,c_2255,c_2256,c_2430,c_2483,c_2533,c_3133,c_3424,c_3484,c_3764,c_4259,c_4727]) ).
tcf(c_4729,plain,
( ( hole_of(pigeon_4) = hole_2 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_4728]) ).
tcf(c_4730,plain,
( ( hole_of(pigeon_1) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_4729,c_97,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_364,c_365,c_367,c_368,c_370,c_372,c_635,c_697,c_711,c_715,c_724,c_732,c_780,c_782,c_789,c_791,c_802,c_829,c_841,c_850,c_853,c_1138,c_2140,c_2197,c_2251,c_2255,c_2256,c_2430,c_2483,c_2533,c_3133,c_3424,c_3484,c_4259,c_4729]) ).
tcf(c_4731,plain,
( ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_1) = hole_1 ) ),
inference(renaming,[status(thm)],[c_4730]) ).
tcf(c_4743,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( hole_of(pigeon_3) = hole_of(X0_iProver_pigeon_1) )
| ( hole_of(pigeon_3) != hole_of(pigeon_3) )
| ( hole_of(X0_iProver_pigeon_1) != hole_of(pigeon_3) ) ),
inference(instantiation,[status(thm)],[c_4049]) ).
tcf(c_4744,plain,
( ( hole_of(pigeon_3) = hole_of(pigeon_1) )
| ( hole_of(pigeon_3) != hole_of(pigeon_3) )
| ( hole_of(pigeon_1) != hole_of(pigeon_3) ) ),
inference(instantiation,[status(thm)],[c_4743]) ).
tcf(c_4951,plain,
( ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_4266,c_97,c_85,c_84,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_365,c_366,c_370,c_371,c_373,c_635,c_724,c_728,c_736,c_780,c_782,c_791,c_802,c_829,c_830,c_836,c_850,c_853,c_1124,c_1125,c_1139,c_1279,c_1620,c_2135,c_2191,c_2289,c_2389,c_2869,c_3059,c_3914,c_4731]) ).
tcf(c_4952,plain,
( ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_1) = hole_2 ) ),
inference(renaming,[status(thm)],[c_4951]) ).
tcf(c_4953,plain,
( ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_1) = hole_2 )
| ( hole_of(pigeon_2) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_4952,c_97,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_367,c_368,c_369,c_370,c_371,c_635,c_711,c_715,c_719,c_724,c_728,c_780,c_782,c_789,c_791,c_802,c_829,c_830,c_841,c_850,c_853,c_1124,c_1125,c_2135,c_2191,c_2255,c_2256,c_2257,c_2389,c_2447,c_2508,c_2533,c_3059,c_3475,c_3697,c_4731,c_4952]) ).
tcf(c_4954,plain,
( ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_2 )
| ( hole_of(pigeon_1) = hole_2 ) ),
inference(renaming,[status(thm)],[c_4953]) ).
tcf(c_5104,plain,
( in(pigeon_3,hole_of(pigeon_4))
| ~ in(pigeon_3,hole_of(pigeon_3))
| ( hole_of(pigeon_4) != hole_of(pigeon_3) ) ),
inference(instantiation,[status(thm)],[c_1892]) ).
tcf(c_5123,plain,
( ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 )
| ( hole_of(pigeon_2) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2869,c_97,c_96,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_364,c_365,c_366,c_367,c_368,c_370,c_371,c_635,c_637,c_706,c_711,c_715,c_724,c_728,c_780,c_782,c_789,c_791,c_802,c_820,c_822,c_850,c_853,c_1002,c_1117,c_1119,c_2139,c_2144,c_2249,c_2251,c_2255,c_2256,c_2365,c_2430,c_2869,c_3060,c_3274,c_3572,c_3749,c_3914,c_3998,c_4952,c_4954,c_5104]) ).
tcf(c_5125,plain,
( ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_2) = hole_3 ) ),
inference(global_subsumption_just,[status(thm)],[c_5123,c_97,c_96,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_364,c_365,c_366,c_367,c_368,c_370,c_371,c_373,c_635,c_637,c_706,c_711,c_715,c_724,c_728,c_736,c_780,c_782,c_789,c_791,c_802,c_820,c_822,c_829,c_830,c_836,c_850,c_853,c_1002,c_1117,c_1119,c_1124,c_1125,c_1139,c_2139,c_2144,c_2249,c_2255,c_2256,c_2365,c_2430,c_3060,c_3274,c_3572,c_3749,c_3764,c_3914,c_3998,c_4088,c_4727,c_4731,c_4954,c_5104,c_5123]) ).
tcf(c_5127,plain,
( ( hole_of(pigeon_4) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(global_subsumption_just,[status(thm)],[c_5125,c_97,c_96,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_364,c_365,c_367,c_368,c_369,c_370,c_371,c_373,c_635,c_637,c_711,c_715,c_719,c_724,c_728,c_736,c_780,c_782,c_789,c_791,c_802,c_820,c_822,c_830,c_836,c_841,c_850,c_853,c_1002,c_1117,c_1119,c_1125,c_1139,c_2139,c_2144,c_2249,c_2255,c_2256,c_2257,c_2365,c_2430,c_2447,c_2508,c_2533,c_3475,c_3697,c_3914,c_4088,c_4731,c_4954,c_5125]) ).
tcf(c_5129,plain,
( ( hole_of(pigeon_3) = hole_1 )
| ( hole_of(pigeon_3) = hole_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_5127,c_97,c_96,c_85,c_84,c_83,c_82,c_81,c_389,c_390,c_355,c_356,c_359,c_364,c_365,c_367,c_368,c_369,c_370,c_371,c_373,c_635,c_637,c_711,c_715,c_719,c_724,c_728,c_736,c_780,c_782,c_789,c_791,c_802,c_820,c_822,c_830,c_836,c_841,c_850,c_853,c_1002,c_1117,c_1119,c_1125,c_1139,c_2139,c_2249,c_2255,c_2256,c_2257,c_2365,c_2447,c_2533,c_3475,c_3914,c_4088,c_4731,c_5127]) ).
tcf(c_5130,plain,
( ( hole_of(pigeon_3) = hole_2 )
| ( hole_of(pigeon_3) = hole_1 ) ),
inference(renaming,[status(thm)],[c_5129]) ).
tcf(c_5135,plain,
! [X0_iProver_pigeon_1: iProver_pigeon_1] :
( ( X0_iProver_pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_3)
| ~ pigeon(X0_iProver_pigeon_1)
| ~ in(X0_iProver_pigeon_1,hole_2) ),
inference(superposition,[status(thm)],[c_5130,c_2713]) ).
tcf(c_5138,plain,
( ( pigeon_1 = pigeon_3 )
| ( hole_of(pigeon_3) = hole_1 )
| ~ pigeon(pigeon_3)
| ~ pigeon(pigeon_1)
| ~ in(pigeon_1,hole_2) ),
inference(instantiation,[status(thm)],[c_5135]) ).
tcf(c_5159,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_5138,c_5130,c_5127,c_4744,c_4088,c_3936,c_3913,c_3811,c_3764,c_3717,c_3697,c_3505,c_3431,c_3424,c_3130,c_3134,c_3061,c_3060,c_2861,c_2842,c_2568,c_2481,c_2483,c_2447,c_2430,c_2388,c_2365,c_2289,c_2257,c_2256,c_2255,c_2253,c_2251,c_2249,c_2247,c_2197,c_2191,c_2150,c_2144,c_2140,c_2139,c_2135,c_1749,c_1620,c_1619,c_1279,c_1277,c_1139,c_1138,c_1125,c_1124,c_1121,c_1119,c_1117,c_1063,c_1002,c_853,c_850,c_841,c_836,c_830,c_829,c_824,c_822,c_820,c_802,c_791,c_789,c_782,c_780,c_736,c_732,c_728,c_724,c_719,c_715,c_711,c_697,c_645,c_641,c_637,c_635,c_373,c_372,c_371,c_370,c_369,c_368,c_367,c_366,c_365,c_364,c_359,c_356,c_355,c_390,c_389,c_81,c_82,c_83,c_84,c_85,c_96,c_97]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MSC007-2.005 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.38 % Computer : n019.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Thu Sep 24 01:26:58 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.42 Running first-order theorem proving
% 0.16/5.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.43
% 0.16/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.43
% 0.16/5.43 % Detected problem language: tptp
% 0.16/5.44 % Proving...
% 2.80/6.29 % SZS status Started for theBenchmark.p
% 2.80/6.29 % SZS status Unsatisfiable for theBenchmark.p
% 2.80/6.29
% 2.80/6.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.80/6.29
% 2.80/6.29 % ------ iProver source info
% 2.80/6.29
% 2.80/6.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.80/6.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.80/6.29 % git: non_committed_changes: false
% 2.80/6.29
% 2.80/6.29 % ------ Parsing...% successful
% 2.80/6.29
% 2.80/6.29
% 2.80/6.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.80/6.29
% 2.80/6.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 2.80/6.29
% 2.80/6.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.80/6.29
% 2.80/6.29 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.80/6.29 % ------ Proving...
% 2.80/6.29 % ------ Problem Properties
% 2.80/6.29
% 2.80/6.29 %
% 2.80/6.29 % clauses 29
% 2.80/6.29 % conjectures 1
% 2.80/6.29 % EPR 27
% 2.80/6.29 % Horn 28
% 2.80/6.29 % unary 25
% 2.80/6.29 % binary 2
% 2.80/6.29 % lits 40
% 2.80/6.29 % lits eq 21
% 2.80/6.29 % fd_pure 0
% 2.80/6.29 % fd_pseudo 0
% 2.80/6.29 % fd_cond 1
% 2.80/6.29 % fd_pseudo_cond 1
% 2.80/6.29 % AC symbols 0
% 2.80/6.29
% 2.80/6.29 % ------ Input Options Time Limit: Unbounded
% 2.80/6.29
% 2.80/6.29
% 2.80/6.29 % ------
% 2.80/6.29 % Current options:
% 2.80/6.29 % ------
% 2.80/6.29
% 2.80/6.29
% 2.80/6.29 %
% 2.80/6.29
% 2.80/6.29 % ------ Proving...
% 2.80/6.29 %
% 2.80/6.29
% 2.80/6.29 % SZS status Unsatisfiable for theBenchmark.p
% 2.80/6.29
% 2.80/6.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.80/6.31
% 3.80/6.31
%------------------------------------------------------------------------------