%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP053^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 01:46:49 PM UTC 2025
% Result : Theorem 4.15s 4.35s
% Output : Proof 4.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 48
% Syntax : Number of formulae : 143 ( 86 unt; 0 typ; 0 def)
% Number of atoms : 808 ( 98 equ; 0 cnn)
% Maximal formula atoms : 3 ( 5 avg)
% Number of connectives : 786 ( 61 ~; 44 |; 0 &; 656 @)
% ( 1 <=>; 21 =>; 3 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Number of types : 4 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 31 ( 29 usr; 26 con; 0-3 aty)
% Number of variables : 85 ( 0 ^; 85 !; 0 ?; 85 :)
% Comments :
%------------------------------------------------------------------------------
thf(ty_list_P559422087at_nat,type,
list_P559422087at_nat: $tType ).
thf(ty_product_prod_nat_nat,type,
product_prod_nat_nat: $tType ).
thf(ty_capacity,type,
capacity: $tType ).
thf(ty_nat,type,
nat: $tType ).
thf(ty_plus_plus_nat,type,
plus_plus_nat: nat > nat > nat ).
thf(ty_s,type,
s: nat ).
thf(ty_u,type,
u: nat ).
thf(ty_p2,type,
p2: list_P559422087at_nat ).
thf(ty_t,type,
t: nat ).
thf(ty_size_s1990949619at_nat,type,
size_s1990949619at_nat: list_P559422087at_nat > nat ).
thf(ty_c,type,
c: product_prod_nat_nat > capacity ).
thf(ty_one_one_nat,type,
one_one_nat: nat ).
thf(ty_min_dist_capacity,type,
min_dist_capacity: ( product_prod_nat_nat > capacity ) > nat > nat > nat ).
thf(ty_p1,type,
p1: list_P559422087at_nat ).
thf(sP1,plain,
( sP1
<=> ( ( min_dist_capacity @ c @ u @ t )
= ( plus_plus_nat @ one_one_nat @ ( size_s1990949619at_nat @ p2 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])]) ).
thf(conj_0,conjecture,
sP1 ).
thf(h0,negated_conjecture,
~ sP1,
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(h1,assumption,
( ( min_dist_capacity @ c @ s @ t )
!= ( plus_plus_nat @ ( size_s1990949619at_nat @ p1 ) @ ( plus_plus_nat @ one_one_nat @ ( size_s1990949619at_nat @ p2 ) ) ) ),
introduced(assumption,[]) ).
thf(h2,assumption,
sP1,
introduced(assumption,[]) ).
thf(h3,assumption,
( ( min_dist_capacity @ c @ s @ u )
= ( size_s1990949619at_nat @ p1 ) ),
introduced(assumption,[]) ).
thf(pax4,axiom,
( p4
=> ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) ) ),
file('<stdin>',pax4) ).
thf(nax2,axiom,
( p2
<= ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ) ),
file('<stdin>',nax2) ).
thf(ax32,axiom,
p4,
file('<stdin>',ax32) ).
thf(ax34,axiom,
~ p2,
file('<stdin>',ax34) ).
thf(pax25,axiom,
( p25
=> ! [X12: nat,X4: nat,X13: nat,X6: nat] :
( ( X12
= ( fplus_plus_nat @ X4 @ X13 ) )
=> ( ( fplus_plus_nat @ X6 @ X12 )
= ( fplus_plus_nat @ X4 @ ( fplus_plus_nat @ X6 @ X13 ) ) ) ) ),
file('<stdin>',pax25) ).
thf(pax24,axiom,
( p24
=> ! [X12: nat,X4: nat,X13: nat] :
( ( fplus_plus_nat @ ( fplus_plus_nat @ X12 @ X4 ) @ X13 )
= ( fplus_plus_nat @ X12 @ ( fplus_plus_nat @ X4 @ X13 ) ) ) ),
file('<stdin>',pax24) ).
thf(pax6,axiom,
( p6
=> ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) ) ),
file('<stdin>',pax6) ).
thf(ax11,axiom,
p25,
file('<stdin>',ax11) ).
thf(ax12,axiom,
p24,
file('<stdin>',ax12) ).
thf(ax30,axiom,
p6,
file('<stdin>',ax30) ).
thf(pax1,axiom,
( p1
=> ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
file('<stdin>',pax1) ).
thf(ax35,axiom,
p1,
file('<stdin>',ax35) ).
thf(c_0_12,plain,
( ~ p4
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) ) ),
inference(fof_nnf,[status(thm)],[pax4]) ).
thf(c_0_13,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
!= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) )
| p2 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])]) ).
thf(c_0_14,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) )
| ~ p4 ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_15,plain,
p4,
inference(split_conjunct,[status(thm)],[ax32]) ).
thf(c_0_16,plain,
~ p2,
inference(fof_simplification,[status(thm)],[ax34]) ).
thf(c_0_17,plain,
! [X88: nat,X89: nat,X90: nat,X91: nat] :
( ~ p25
| ( X88
!= ( fplus_plus_nat @ X89 @ X90 ) )
| ( ( fplus_plus_nat @ X91 @ X88 )
= ( fplus_plus_nat @ X89 @ ( fplus_plus_nat @ X91 @ X90 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax25])])]) ).
thf(c_0_18,plain,
! [X96: nat,X97: nat,X98: nat] :
( ~ p24
| ( ( fplus_plus_nat @ ( fplus_plus_nat @ X96 @ X97 ) @ X98 )
= ( fplus_plus_nat @ X96 @ ( fplus_plus_nat @ X97 @ X98 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax24])])]) ).
thf(c_0_19,plain,
( ~ p6
| ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) ) ),
inference(fof_nnf,[status(thm)],[pax6]) ).
thf(c_0_20,plain,
( p2
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
!= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
thf(c_0_21,plain,
( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14,c_0_15])]) ).
thf(c_0_22,plain,
~ p2,
inference(split_conjunct,[status(thm)],[c_0_16]) ).
thf(c_0_23,plain,
! [X1: nat,X3: nat,X6: nat,X4: nat] :
( ( ( fplus_plus_nat @ X6 @ X1 )
= ( fplus_plus_nat @ X3 @ ( fplus_plus_nat @ X6 @ X4 ) ) )
| ~ p25
| ( X1
!= ( fplus_plus_nat @ X3 @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_24,plain,
p25,
inference(split_conjunct,[status(thm)],[ax11]) ).
thf(c_0_25,plain,
! [X1: nat,X3: nat,X4: nat] :
( ( ( fplus_plus_nat @ ( fplus_plus_nat @ X1 @ X3 ) @ X4 )
= ( fplus_plus_nat @ X1 @ ( fplus_plus_nat @ X3 @ X4 ) ) )
| ~ p24 ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_26,plain,
p24,
inference(split_conjunct,[status(thm)],[ax12]) ).
thf(c_0_27,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) )
| ~ p6 ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
thf(c_0_28,plain,
p6,
inference(split_conjunct,[status(thm)],[ax30]) ).
thf(c_0_29,plain,
( ~ p1
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
inference(fof_nnf,[status(thm)],[pax1]) ).
thf(c_0_30,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) )
!= ( fsize_s1990949619at_nat @ fp ) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_21]),c_0_22]) ).
thf(c_0_31,plain,
! [X1: nat,X3: nat,X4: nat] :
( ( fplus_plus_nat @ X1 @ ( fplus_plus_nat @ X3 @ X4 ) )
= ( fplus_plus_nat @ X3 @ ( fplus_plus_nat @ X1 @ X4 ) ) ),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_24])])]) ).
thf(c_0_32,plain,
! [X1: nat,X3: nat,X4: nat] :
( ( fplus_plus_nat @ ( fplus_plus_nat @ X1 @ X3 ) @ X4 )
= ( fplus_plus_nat @ X1 @ ( fplus_plus_nat @ X3 @ X4 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25,c_0_26])]) ).
thf(c_0_33,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat )
= ( fmin_dist_capacity @ fc @ fs @ fv ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28])]) ).
thf(c_0_34,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) )
| ~ p1 ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_35,plain,
p1,
inference(split_conjunct,[status(thm)],[ax35]) ).
thf(c_0_36,plain,
( ( fplus_plus_nat @ fone_one_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fsize_s1990949619at_nat @ fp2 ) ) )
!= ( fsize_s1990949619at_nat @ fp ) ),
inference(rw,[status(thm)],[c_0_30,c_0_31]) ).
thf(c_0_37,plain,
! [X1: nat] :
( ( fplus_plus_nat @ fone_one_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ X1 ) )
= ( fplus_plus_nat @ ( fmin_dist_capacity @ fc @ fs @ fv ) @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_31]) ).
thf(c_0_38,plain,
( ( fplus_plus_nat @ ( fmin_dist_capacity @ fc @ fs @ fv ) @ ( fsize_s1990949619at_nat @ fp2 ) )
= ( fsize_s1990949619at_nat @ fp ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_33]),c_0_21]),c_0_35])]) ).
thf(c_0_39,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_37]),c_0_38])]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h1,h1,h0])],[]) ).
thf(pax4_001,axiom,
( p4
=> ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) ) ),
file('<stdin>',pax4) ).
thf(nax2_002,axiom,
( p2
<= ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ) ),
file('<stdin>',nax2) ).
thf(ax45,axiom,
p4,
file('<stdin>',ax45) ).
thf(ax47,axiom,
~ p2,
file('<stdin>',ax47) ).
thf(pax25_003,axiom,
( p25
=> ! [X18: nat,X13: nat,X19: nat,X4: nat] :
( ( X18
= ( fplus_plus_nat @ X13 @ X19 ) )
=> ( ( fplus_plus_nat @ X4 @ X18 )
= ( fplus_plus_nat @ X13 @ ( fplus_plus_nat @ X4 @ X19 ) ) ) ) ),
file('<stdin>',pax25) ).
thf(pax24_004,axiom,
( p24
=> ! [X18: nat,X13: nat,X19: nat] :
( ( fplus_plus_nat @ ( fplus_plus_nat @ X18 @ X13 ) @ X19 )
= ( fplus_plus_nat @ X18 @ ( fplus_plus_nat @ X13 @ X19 ) ) ) ),
file('<stdin>',pax24) ).
thf(pax6_005,axiom,
( p6
=> ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) ) ),
file('<stdin>',pax6) ).
thf(ax24,axiom,
p25,
file('<stdin>',ax24) ).
thf(ax25,axiom,
p24,
file('<stdin>',ax25) ).
thf(ax43,axiom,
p6,
file('<stdin>',ax43) ).
thf(pax1_006,axiom,
( p1
=> ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
file('<stdin>',pax1) ).
thf(ax49,axiom,
p1,
file('<stdin>',ax49) ).
thf(c_0_12_007,plain,
( ~ p4
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) ) ),
inference(fof_nnf,[status(thm)],[pax4]) ).
thf(c_0_13_008,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
!= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) )
| p2 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])]) ).
thf(c_0_14_009,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) )
| ~ p4 ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_15_010,plain,
p4,
inference(split_conjunct,[status(thm)],[ax45]) ).
thf(c_0_16_011,plain,
~ p2,
inference(fof_simplification,[status(thm)],[ax47]) ).
thf(c_0_17_012,plain,
! [X162: nat,X163: nat,X164: nat,X165: nat] :
( ~ p25
| ( X162
!= ( fplus_plus_nat @ X163 @ X164 ) )
| ( ( fplus_plus_nat @ X165 @ X162 )
= ( fplus_plus_nat @ X163 @ ( fplus_plus_nat @ X165 @ X164 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax25])])]) ).
thf(c_0_18_013,plain,
! [X170: nat,X171: nat,X172: nat] :
( ~ p24
| ( ( fplus_plus_nat @ ( fplus_plus_nat @ X170 @ X171 ) @ X172 )
= ( fplus_plus_nat @ X170 @ ( fplus_plus_nat @ X171 @ X172 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax24])])]) ).
thf(c_0_19_014,plain,
( ~ p6
| ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) ) ),
inference(fof_nnf,[status(thm)],[pax6]) ).
thf(c_0_20_015,plain,
( p2
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
!= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
thf(c_0_21_016,plain,
( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fsize_s1990949619at_nat @ fp ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14,c_0_15])]) ).
thf(c_0_22_017,plain,
~ p2,
inference(split_conjunct,[status(thm)],[c_0_16]) ).
thf(c_0_23_018,plain,
! [X1: nat,X3: nat,X5: nat,X4: nat] :
( ( ( fplus_plus_nat @ X5 @ X1 )
= ( fplus_plus_nat @ X3 @ ( fplus_plus_nat @ X5 @ X4 ) ) )
| ~ p25
| ( X1
!= ( fplus_plus_nat @ X3 @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_24_019,plain,
p25,
inference(split_conjunct,[status(thm)],[ax24]) ).
thf(c_0_25_020,plain,
! [X1: nat,X3: nat,X4: nat] :
( ( ( fplus_plus_nat @ ( fplus_plus_nat @ X1 @ X3 ) @ X4 )
= ( fplus_plus_nat @ X1 @ ( fplus_plus_nat @ X3 @ X4 ) ) )
| ~ p24 ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_26_021,plain,
p24,
inference(split_conjunct,[status(thm)],[ax25]) ).
thf(c_0_27_022,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) )
| ~ p6 ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
thf(c_0_28_023,plain,
p6,
inference(split_conjunct,[status(thm)],[ax43]) ).
thf(c_0_29_024,plain,
( ~ p1
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
inference(fof_nnf,[status(thm)],[pax1]) ).
thf(c_0_30_025,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) )
!= ( fsize_s1990949619at_nat @ fp ) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_21]),c_0_22]) ).
thf(c_0_31_026,plain,
! [X1: nat,X3: nat,X4: nat] :
( ( fplus_plus_nat @ X1 @ ( fplus_plus_nat @ X3 @ X4 ) )
= ( fplus_plus_nat @ X3 @ ( fplus_plus_nat @ X1 @ X4 ) ) ),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_24])])]) ).
thf(c_0_32_027,plain,
! [X1: nat,X3: nat,X4: nat] :
( ( fplus_plus_nat @ ( fplus_plus_nat @ X1 @ X3 ) @ X4 )
= ( fplus_plus_nat @ X1 @ ( fplus_plus_nat @ X3 @ X4 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25,c_0_26])]) ).
thf(c_0_33_028,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat )
= ( fmin_dist_capacity @ fc @ fs @ fv ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28])]) ).
thf(c_0_34_029,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) )
| ~ p1 ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_35_030,plain,
p1,
inference(split_conjunct,[status(thm)],[ax49]) ).
thf(c_0_36_031,plain,
( ( fplus_plus_nat @ fone_one_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fsize_s1990949619at_nat @ fp2 ) ) )
!= ( fsize_s1990949619at_nat @ fp ) ),
inference(rw,[status(thm)],[c_0_30,c_0_31]) ).
thf(c_0_37_032,plain,
! [X1: nat] :
( ( fplus_plus_nat @ fone_one_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ X1 ) )
= ( fplus_plus_nat @ ( fmin_dist_capacity @ fc @ fs @ fv ) @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_31]) ).
thf(c_0_38_033,plain,
( ( fplus_plus_nat @ ( fmin_dist_capacity @ fc @ fs @ fv ) @ ( fsize_s1990949619at_nat @ fp2 ) )
= ( fsize_s1990949619at_nat @ fp ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_33]),c_0_21]),c_0_35])]) ).
thf(c_0_39_034,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_37]),c_0_38])]),
[proof] ).
thf(2,plain,
$false,
inference(eprover,[status(thm),assumptions([h3,h1,h0])],[]) ).
thf(fact_1__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_As_Au_A_061_Alength_Ap1_092_060close_062,axiom,
( ( ( min_dist_capacity @ c @ s @ t )
= ( plus_plus_nat @ ( size_s1990949619at_nat @ p1 ) @ ( plus_plus_nat @ one_one_nat @ ( size_s1990949619at_nat @ p2 ) ) ) )
=> ( ( min_dist_capacity @ c @ s @ u )
= ( size_s1990949619at_nat @ p1 ) ) ) ).
thf(3,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h1,h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h3])],[fact_1__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_As_Au_A_061_Alength_Ap1_092_060close_062,1,2,h1,h3]) ).
thf(pax3,axiom,
( p3
=> ( ( fmin_dist_capacity @ fc @ fv @ ft )
= ( fsize_s1990949619at_nat @ fp2 ) ) ),
file('<stdin>',pax3) ).
thf(pax24_035,axiom,
( p24
=> ! [X21: nat,X16: nat,X22: nat] :
( ( fplus_plus_nat @ ( fplus_plus_nat @ X21 @ X16 ) @ X22 )
= ( fplus_plus_nat @ X21 @ ( fplus_plus_nat @ X16 @ X22 ) ) ) ),
file('<stdin>',pax24) ).
thf(pax6_036,axiom,
( p6
=> ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) ) ),
file('<stdin>',pax6) ).
thf(pax25_037,axiom,
( p25
=> ! [X21: nat,X16: nat,X22: nat,X4: nat] :
( ( X21
= ( fplus_plus_nat @ X16 @ X22 ) )
=> ( ( fplus_plus_nat @ X4 @ X21 )
= ( fplus_plus_nat @ X16 @ ( fplus_plus_nat @ X4 @ X22 ) ) ) ) ),
file('<stdin>',pax25) ).
thf(pax52,axiom,
( p52
=> ( ( fmin_dist_capacity @ fc @ fu @ ft )
= ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
file('<stdin>',pax52) ).
thf(ax57,axiom,
p3,
file('<stdin>',ax57) ).
thf(nax2_038,axiom,
( p2
<= ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ) ),
file('<stdin>',nax2) ).
thf(ax59,axiom,
~ p2,
file('<stdin>',ax59) ).
thf(ax36,axiom,
p24,
file('<stdin>',ax36) ).
thf(ax54,axiom,
p6,
file('<stdin>',ax54) ).
thf(ax35_039,axiom,
p25,
file('<stdin>',ax35) ).
thf(ax58,axiom,
p52,
file('<stdin>',ax58) ).
thf(pax1_040,axiom,
( p1
=> ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
file('<stdin>',pax1) ).
thf(ax60,axiom,
p1,
file('<stdin>',ax60) ).
thf(c_0_14_041,plain,
( ~ p3
| ( ( fmin_dist_capacity @ fc @ fv @ ft )
= ( fsize_s1990949619at_nat @ fp2 ) ) ),
inference(fof_nnf,[status(thm)],[pax3]) ).
thf(c_0_15_042,plain,
! [X257: nat,X258: nat,X259: nat] :
( ~ p24
| ( ( fplus_plus_nat @ ( fplus_plus_nat @ X257 @ X258 ) @ X259 )
= ( fplus_plus_nat @ X257 @ ( fplus_plus_nat @ X258 @ X259 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax24])])]) ).
thf(c_0_16_043,plain,
( ~ p6
| ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) ) ),
inference(fof_nnf,[status(thm)],[pax6]) ).
thf(c_0_17_044,plain,
! [X249: nat,X250: nat,X251: nat,X252: nat] :
( ~ p25
| ( X249
!= ( fplus_plus_nat @ X250 @ X251 ) )
| ( ( fplus_plus_nat @ X252 @ X249 )
= ( fplus_plus_nat @ X250 @ ( fplus_plus_nat @ X252 @ X251 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax25])])]) ).
thf(c_0_18_045,plain,
( ~ p52
| ( ( fmin_dist_capacity @ fc @ fu @ ft )
= ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
inference(fof_nnf,[status(thm)],[pax52]) ).
thf(c_0_19_046,plain,
( ( ( fmin_dist_capacity @ fc @ fv @ ft )
= ( fsize_s1990949619at_nat @ fp2 ) )
| ~ p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_20_047,plain,
p3,
inference(split_conjunct,[status(thm)],[ax57]) ).
thf(c_0_21_048,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
!= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) )
| p2 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])]) ).
thf(c_0_22_049,plain,
~ p2,
inference(fof_simplification,[status(thm)],[ax59]) ).
thf(c_0_23_050,plain,
! [X2: nat,X4: nat,X5: nat] :
( ( ( fplus_plus_nat @ ( fplus_plus_nat @ X2 @ X4 ) @ X5 )
= ( fplus_plus_nat @ X2 @ ( fplus_plus_nat @ X4 @ X5 ) ) )
| ~ p24 ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
thf(c_0_24_051,plain,
p24,
inference(split_conjunct,[status(thm)],[ax36]) ).
thf(c_0_25_052,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ fv )
= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) )
| ~ p6 ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
thf(c_0_26_053,plain,
p6,
inference(split_conjunct,[status(thm)],[ax54]) ).
thf(c_0_27_054,plain,
! [X2: nat,X4: nat,X6: nat,X5: nat] :
( ( ( fplus_plus_nat @ X6 @ X2 )
= ( fplus_plus_nat @ X4 @ ( fplus_plus_nat @ X6 @ X5 ) ) )
| ~ p25
| ( X2
!= ( fplus_plus_nat @ X4 @ X5 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_28_055,plain,
p25,
inference(split_conjunct,[status(thm)],[ax35]) ).
thf(c_0_29_056,plain,
( ( ( fmin_dist_capacity @ fc @ fu @ ft )
= ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) )
| ~ p52 ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_30_057,plain,
( ( fsize_s1990949619at_nat @ fp2 )
= ( fmin_dist_capacity @ fc @ fv @ ft ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19,c_0_20])]) ).
thf(c_0_31_058,plain,
p52,
inference(split_conjunct,[status(thm)],[ax58]) ).
thf(c_0_32_059,plain,
( ~ p1
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ),
inference(fof_nnf,[status(thm)],[pax1]) ).
thf(c_0_33_060,plain,
( p2
| ( ( fmin_dist_capacity @ fc @ fs @ ft )
!= ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fsize_s1990949619at_nat @ fp2 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
thf(c_0_34_061,plain,
~ p2,
inference(split_conjunct,[status(thm)],[c_0_22]) ).
thf(c_0_35_062,plain,
! [X2: nat,X4: nat,X5: nat] :
( ( fplus_plus_nat @ ( fplus_plus_nat @ X2 @ X4 ) @ X5 )
= ( fplus_plus_nat @ X2 @ ( fplus_plus_nat @ X4 @ X5 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_24])]) ).
thf(c_0_36_063,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat )
= ( fmin_dist_capacity @ fc @ fs @ fv ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25,c_0_26])]) ).
thf(c_0_37_064,plain,
! [X2: nat,X4: nat,X5: nat] :
( ( fplus_plus_nat @ X2 @ ( fplus_plus_nat @ X4 @ X5 ) )
= ( fplus_plus_nat @ X4 @ ( fplus_plus_nat @ X2 @ X5 ) ) ),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28])])]) ).
thf(c_0_38_065,plain,
( ( fplus_plus_nat @ fone_one_nat @ ( fmin_dist_capacity @ fc @ fv @ ft ) )
= ( fmin_dist_capacity @ fc @ fu @ ft ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_29,c_0_30]),c_0_31])]) ).
thf(c_0_39_066,plain,
( ( ( fmin_dist_capacity @ fc @ fs @ ft )
= ( fplus_plus_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ fone_one_nat ) @ ( fsize_s1990949619at_nat @ fp2 ) ) )
| ~ p1 ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_40,plain,
p1,
inference(split_conjunct,[status(thm)],[ax60]) ).
thf(c_0_41,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fplus_plus_nat @ fone_one_nat @ ( fmin_dist_capacity @ fc @ fv @ ft ) ) )
!= ( fmin_dist_capacity @ fc @ fs @ ft ) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_33,c_0_30]),c_0_34]) ).
thf(c_0_42,plain,
! [X2: nat] :
( ( fplus_plus_nat @ fone_one_nat @ ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ X2 ) )
= ( fplus_plus_nat @ ( fmin_dist_capacity @ fc @ fs @ fv ) @ X2 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_37]) ).
thf(c_0_43,plain,
! [X2: nat] :
( ( fplus_plus_nat @ fone_one_nat @ ( fplus_plus_nat @ X2 @ ( fmin_dist_capacity @ fc @ fv @ ft ) ) )
= ( fplus_plus_nat @ X2 @ ( fmin_dist_capacity @ fc @ fu @ ft ) ) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
thf(c_0_44,plain,
( ( fplus_plus_nat @ ( fmin_dist_capacity @ fc @ fs @ fv ) @ ( fmin_dist_capacity @ fc @ fv @ ft ) )
= ( fmin_dist_capacity @ fc @ fs @ ft ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_39,c_0_36]),c_0_30]),c_0_40])]) ).
thf(c_0_45,plain,
( ( fplus_plus_nat @ ( fsize_s1990949619at_nat @ fp1 ) @ ( fmin_dist_capacity @ fc @ fu @ ft ) )
!= ( fmin_dist_capacity @ fc @ fs @ ft ) ),
inference(rw,[status(thm)],[c_0_41,c_0_38]) ).
thf(c_0_46,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_44]),c_0_45]),
[proof] ).
thf(4,plain,
$false,
inference(eprover,[status(thm),assumptions([h1,h2,h0])],[]) ).
thf(5,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h3,h2,h0])],[h2,h0]) ).
thf(6,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h2,h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h3])],[fact_1__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_As_Au_A_061_Alength_Ap1_092_060close_062,4,5,h1,h3]) ).
thf(fact_2__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_Au_At_A_061_A1_A_L_Alength_Ap2_092_060close_062,axiom,
( ( ( min_dist_capacity @ c @ s @ t )
= ( plus_plus_nat @ ( size_s1990949619at_nat @ p1 ) @ ( plus_plus_nat @ one_one_nat @ ( size_s1990949619at_nat @ p2 ) ) ) )
=> sP1 ) ).
thf(7,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[fact_2__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_Au_At_A_061_A1_A_L_Alength_Ap2_092_060close_062,3,6,h1,h2]) ).
thf(0,theorem,
sP1,
inference(contra,[status(thm),contra(discharge,[h0])],[7,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : ITP053^1 : TPTP v9.2.0. Released v7.5.0.
% 0.09/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n031.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 17:58:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 4.15/4.35 % SZS status Theorem
% 4.15/4.35 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 4.15/4.35 % Inferences: 0
% 4.15/4.35 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------