%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP127^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 : n001.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:47:03 PM UTC 2025
% Result : Theorem 277.13s 274.05s
% Output : Proof 277.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 18
% Syntax : Number of formulae : 58 ( 27 unt; 0 typ; 0 def)
% Number of atoms : 255 ( 29 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 241 ( 40 ~; 33 |; 0 &; 161 @)
% ( 0 <=>; 6 =>; 1 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 19 ( 19 >; 0 *; 0 +; 0 <<)
% Number of symbols : 31 ( 29 usr; 30 con; 0-2 aty)
% Number of variables : 31 ( 0 ^; 31 !; 0 ?; 31 :)
% Comments :
%------------------------------------------------------------------------------
thf(conj_0,conjecture,
( ( monomo463139869_c_m_a @ mergec @ ( counta472291938sert_c @ x @ bot_bo1320844070cset_c ) @ f )
= ( f @ x ) ) ).
thf(h0,negated_conjecture,
( ( monomo463139869_c_m_a @ mergec @ ( counta472291938sert_c @ x @ bot_bo1320844070cset_c ) @ f )
!= ( f @ x ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(ax1346,axiom,
( ~ p155
| p158 ),
file('<stdin>',ax1346) ).
thf(ax1345,axiom,
( ~ p158
| p159 ),
file('<stdin>',ax1345) ).
thf(ax1350,axiom,
p155,
file('<stdin>',ax1350) ).
thf(ax1344,axiom,
( ~ p159
| ~ p154
| p153 ),
file('<stdin>',ax1344) ).
thf(ax1351,axiom,
~ p153,
file('<stdin>',ax1351) ).
thf(pax8,axiom,
( p8
=> ! [X504: countable_Set_cset_c,X505: c > monomo197243225tT_a_m] :
( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ X504 @ X505 ) )
= ( fmergec @ X504 @ ( fcomp_M750374444_m_m_c @ fmonomo624345106et_a_m @ X505 ) ) ) ),
file('<stdin>',pax8) ).
thf(pax1,axiom,
( p1
=> ! [X506: c,X512: c > m] :
( ( fmergec @ ( fcounta472291938sert_c @ X506 @ fbot_bo1320844070cset_c ) @ X512 )
= ( X512 @ X506 ) ) ),
file('<stdin>',pax1) ).
thf(nax154,axiom,
( p154
<= ( ( ff @ fx )
= ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff ) ) ),
file('<stdin>',nax154) ).
thf(ax1154,axiom,
( ~ p9
| p339 ),
file('<stdin>',ax1154) ).
thf(pax338,axiom,
( p338
=> ( ( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff ) )
= ( fmonomo624345106et_a_m @ ( ff @ fx ) ) )
=> ( ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff )
= ( ff @ fx ) ) ) ),
file('<stdin>',pax338) ).
thf(ax1496,axiom,
p8,
file('<stdin>',ax1496) ).
thf(ax1503,axiom,
p1,
file('<stdin>',ax1503) ).
thf(ax1155,axiom,
( ~ p339
| p338 ),
file('<stdin>',ax1155) ).
thf(ax1495,axiom,
p9,
file('<stdin>',ax1495) ).
thf(pax30,axiom,
( p30
=> ! [X443: monomo197243225tT_a_m > m,X444: c > monomo197243225tT_a_m,X451: c > m,X452: c] :
( ( ( fcomp_M750374444_m_m_c @ X443 @ X444 )
= X451 )
=> ( ( X443 @ ( X444 @ X452 ) )
= ( X451 @ X452 ) ) ) ),
file('<stdin>',pax30) ).
thf(ax1474,axiom,
p30,
file('<stdin>',ax1474) ).
thf(c_0_16,plain,
( ~ p155
| p158 ),
inference(fof_simplification,[status(thm)],[ax1346]) ).
thf(c_0_17,plain,
( ~ p158
| p159 ),
inference(fof_simplification,[status(thm)],[ax1345]) ).
thf(c_0_18,plain,
( p158
| ~ p155 ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
thf(c_0_19,plain,
p155,
inference(split_conjunct,[status(thm)],[ax1350]) ).
thf(c_0_20,plain,
( ~ p159
| ~ p154
| p153 ),
inference(fof_simplification,[status(thm)],[ax1344]) ).
thf(c_0_21,plain,
( p159
| ~ p158 ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_22,plain,
p158,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_19])]) ).
thf(c_0_23,plain,
~ p153,
inference(fof_simplification,[status(thm)],[ax1351]) ).
thf(c_0_24,plain,
! [X3311: countable_Set_cset_c,X3312: c > monomo197243225tT_a_m] :
( ~ p8
| ( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ X3311 @ X3312 ) )
= ( fmergec @ X3311 @ ( fcomp_M750374444_m_m_c @ fmonomo624345106et_a_m @ X3312 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax8])])]) ).
thf(c_0_25,plain,
! [X3333: c,X3334: c > m] :
( ~ p1
| ( ( fmergec @ ( fcounta472291938sert_c @ X3333 @ fbot_bo1320844070cset_c ) @ X3334 )
= ( X3334 @ X3333 ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1])])]) ).
thf(c_0_26,plain,
( ( ( ff @ fx )
!= ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff ) )
| p154 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax154])]) ).
thf(c_0_27,plain,
( p153
| ~ p159
| ~ p154 ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_28,plain,
p159,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21,c_0_22])]) ).
thf(c_0_29,plain,
~ p153,
inference(split_conjunct,[status(thm)],[c_0_23]) ).
thf(c_0_30,plain,
( ~ p9
| p339 ),
inference(fof_simplification,[status(thm)],[ax1154]) ).
thf(c_0_31,plain,
( ~ p338
| ( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff ) )
!= ( fmonomo624345106et_a_m @ ( ff @ fx ) ) )
| ( ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff )
= ( ff @ fx ) ) ),
inference(fof_nnf,[status(thm)],[pax338]) ).
thf(c_0_32,plain,
! [X2: countable_Set_cset_c,X22: c > monomo197243225tT_a_m] :
( ( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ X2 @ X22 ) )
= ( fmergec @ X2 @ ( fcomp_M750374444_m_m_c @ fmonomo624345106et_a_m @ X22 ) ) )
| ~ p8 ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
thf(c_0_33,plain,
p8,
inference(split_conjunct,[status(thm)],[ax1496]) ).
thf(c_0_34,plain,
! [X34: c > m,X1: c] :
( ( ( fmergec @ ( fcounta472291938sert_c @ X1 @ fbot_bo1320844070cset_c ) @ X34 )
= ( X34 @ X1 ) )
| ~ p1 ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
thf(c_0_35,plain,
p1,
inference(split_conjunct,[status(thm)],[ax1503]) ).
thf(c_0_36,plain,
( p154
| ( ( ff @ fx )
!= ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff ) ) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
thf(c_0_37,plain,
~ p154,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28])]),c_0_29]) ).
thf(c_0_38,plain,
( ~ p339
| p338 ),
inference(fof_simplification,[status(thm)],[ax1155]) ).
thf(c_0_39,plain,
( p339
| ~ p9 ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
thf(c_0_40,plain,
p9,
inference(split_conjunct,[status(thm)],[ax1495]) ).
thf(c_0_41,plain,
! [X3143: monomo197243225tT_a_m > m,X3144: c > monomo197243225tT_a_m,X3145: c > m,X3146: c] :
( ~ p30
| ( ( fcomp_M750374444_m_m_c @ X3143 @ X3144 )
!= X3145 )
| ( ( X3143 @ ( X3144 @ X3146 ) )
= ( X3145 @ X3146 ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax30])])]) ).
thf(c_0_42,plain,
( ( ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff )
= ( ff @ fx ) )
| ~ p338
| ( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff ) )
!= ( fmonomo624345106et_a_m @ ( ff @ fx ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_43,plain,
! [X2: countable_Set_cset_c,X22: c > monomo197243225tT_a_m] :
( ( fmonomo624345106et_a_m @ ( fmonomo463139869_c_m_a @ fmergec @ X2 @ X22 ) )
= ( fmergec @ X2 @ ( fcomp_M750374444_m_m_c @ fmonomo624345106et_a_m @ X22 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32,c_0_33])]) ).
thf(c_0_44,plain,
! [X34: c > m,X1: c] :
( ( fmergec @ ( fcounta472291938sert_c @ X1 @ fbot_bo1320844070cset_c ) @ X34 )
= ( X34 @ X1 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_35])]) ).
thf(c_0_45,plain,
( ( fmonomo463139869_c_m_a @ fmergec @ ( fcounta472291938sert_c @ fx @ fbot_bo1320844070cset_c ) @ ff )
!= ( ff @ fx ) ),
inference(sr,[status(thm)],[c_0_36,c_0_37]) ).
thf(c_0_46,plain,
( p338
| ~ p339 ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
thf(c_0_47,plain,
p339,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39,c_0_40])]) ).
thf(c_0_48,plain,
! [X1: c,X22: c > monomo197243225tT_a_m,X420: monomo197243225tT_a_m > m,X34: c > m] :
( ( ( X420 @ ( X22 @ X1 ) )
= ( X34 @ X1 ) )
| ~ p30
| ( ( fcomp_M750374444_m_m_c @ X420 @ X22 )
!= X34 ) ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
thf(c_0_49,plain,
p30,
inference(split_conjunct,[status(thm)],[ax1474]) ).
thf(c_0_50,plain,
( ( ( fcomp_M750374444_m_m_c @ fmonomo624345106et_a_m @ ff @ fx )
!= ( fmonomo624345106et_a_m @ ( ff @ fx ) ) )
| ~ p338 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_42,c_0_43]),c_0_44]),c_0_45]) ).
thf(c_0_51,plain,
p338,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46,c_0_47])]) ).
thf(c_0_52,plain,
! [X420: monomo197243225tT_a_m > m,X22: c > monomo197243225tT_a_m,X1: c] :
( ( fcomp_M750374444_m_m_c @ X420 @ X22 @ X1 )
= ( X420 @ ( X22 @ X1 ) ) ),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48,c_0_49])])]) ).
thf(c_0_53,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50,c_0_51])]),c_0_52])]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
( ( monomo463139869_c_m_a @ mergec @ ( counta472291938sert_c @ x @ bot_bo1320844070cset_c ) @ f )
= ( f @ x ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP127^1 : TPTP v9.2.0. Released v7.5.0.
% 0.03/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.33 % Computer : n001.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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:53:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 277.13/274.05 % SZS status Theorem
% 277.13/274.05 % Mode: mode498:USE_SINE=true:SINE_TOLERANCE=1.5:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=2
% 277.13/274.05 % Inferences: 420
% 277.13/274.05 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------