%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP043^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 : n004.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:48 PM UTC 2025
% Result : Theorem 37.58s 37.74s
% Output : Proof 37.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 29
% Syntax : Number of formulae : 96 ( 45 unt; 0 typ; 0 def)
% Number of atoms : 547 ( 61 equ; 0 cnn)
% Maximal formula atoms : 4 ( 5 avg)
% Number of connectives : 465 ( 60 ~; 48 |; 0 &; 342 @)
% ( 0 <=>; 14 =>; 1 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 44 ( 42 usr; 43 con; 0-2 aty)
% Number of variables : 46 ( 0 ^; 46 !; 0 ?; 46 :)
% Comments :
%------------------------------------------------------------------------------
thf(conj_0,conjecture,
( ( descar1375166517sums_a @ xsa )
= ( append_a @ ( replicate_a @ p @ zero_zero_a ) @ ( descar1375166517sums_a @ ( cons_a @ ( nth_a @ xsa @ p ) @ xs2 ) ) ) ) ).
thf(h0,negated_conjecture,
( ( descar1375166517sums_a @ xsa )
!= ( append_a @ ( replicate_a @ p @ zero_zero_a ) @ ( descar1375166517sums_a @ ( cons_a @ ( nth_a @ xsa @ p ) @ xs2 ) ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(ax1213,axiom,
( ~ p49
| p542 ),
file('<stdin>',ax1213) ).
thf(pax69,axiom,
( p69
=> ! [X679: a,X676: list_a] :
( ( fcons_a @ X679 @ X676 )
!= X676 ) ),
file('<stdin>',pax69) ).
thf(ax1558,axiom,
( ~ p16
| p197 ),
file('<stdin>',ax1558) ).
thf(ax1210,axiom,
( ~ p49
| p545 ),
file('<stdin>',ax1210) ).
thf(pax57,axiom,
( p57
=> ! [X685: a,X683: list_a] :
( fnil_a
!= ( fcons_a @ X685 @ X683 ) ) ),
file('<stdin>',pax57) ).
thf(pax58,axiom,
( p58
=> ! [X682: list_a] :
( ( fappend_a @ fnil_a @ X682 )
= X682 ) ),
file('<stdin>',pax58) ).
thf(pax542,axiom,
( p542
=> ( ! [X311: a,X312: list_a] :
( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
!= ( fcons_a @ X311 @ X312 ) )
=> ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= fnil_a ) ) ),
file('<stdin>',pax542) ).
thf(ax1712,axiom,
p49,
file('<stdin>',ax1712) ).
thf(ax1692,axiom,
p69,
file('<stdin>',ax1692) ).
thf(ax11,axiom,
( ~ p197
| p1728 ),
file('<stdin>',ax11) ).
thf(ax1745,axiom,
p16,
file('<stdin>',ax1745) ).
thf(pax72,axiom,
( p72
=> ! [X675: a,X676: list_a,X671: list_a] :
( ( fappend_a @ ( fcons_a @ X675 @ X676 ) @ X671 )
= ( fcons_a @ X675 @ ( fappend_a @ X676 @ X671 ) ) ) ),
file('<stdin>',pax72) ).
thf(pax5,axiom,
( p5
=> ( fxs1
= ( freplicate_a @ fp @ fzero_zero_a ) ) ),
file('<stdin>',pax5) ).
thf(pax545,axiom,
( p545
=> ( ! [X311: a,X312: list_a] :
( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
!= ( fcons_a @ X311 @ X312 ) )
=> ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
= fnil_a ) ) ),
file('<stdin>',pax545) ).
thf(ax1704,axiom,
p57,
file('<stdin>',ax1704) ).
thf(pax1728,axiom,
( p1728
=> ! [X1: list_a,X2: list_a,X3: list_a] :
( ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= X1 )
=> ( ( X2
= ( fappend_a @ fnil_a @ X3 ) )
=> ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ X2 )
= ( fappend_a @ X1 @ X3 ) ) ) ) ),
file('<stdin>',pax1728) ).
thf(ax1703,axiom,
p58,
file('<stdin>',ax1703) ).
thf(ax1689,axiom,
p72,
file('<stdin>',ax1689) ).
thf(pax6,axiom,
( p6
=> ( fxsa
= ( fappend_a @ fxs1 @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) ),
file('<stdin>',pax6) ).
thf(ax1618,axiom,
( ~ p7
| p138 ),
file('<stdin>',ax1618) ).
thf(nax98,axiom,
( p98
<= ( ( fdescar1375166517sums_a @ fxsa )
= ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) ) ),
file('<stdin>',nax98) ).
thf(ax1756,axiom,
p5,
file('<stdin>',ax1756) ).
thf(ax1663,axiom,
~ p98,
file('<stdin>',ax1663) ).
thf(ax1755,axiom,
p6,
file('<stdin>',ax1755) ).
thf(ax620,axiom,
( ~ p138
| p1117 ),
file('<stdin>',ax620) ).
thf(ax1754,axiom,
p7,
file('<stdin>',ax1754) ).
thf(pax1117,axiom,
( p1117
=> ( ( fdescar1375166517sums_a @ ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) )
= ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) ) ),
file('<stdin>',pax1117) ).
thf(c_0_27,plain,
( ~ p49
| p542 ),
inference(fof_simplification,[status(thm)],[ax1213]) ).
thf(c_0_28,plain,
! [X5022: a,X5023: list_a] :
( ~ p69
| ( ( fcons_a @ X5022 @ X5023 )
!= X5023 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax69])])])]) ).
thf(c_0_29,plain,
( ~ p16
| p197 ),
inference(fof_simplification,[status(thm)],[ax1558]) ).
thf(c_0_30,plain,
( ~ p49
| p545 ),
inference(fof_simplification,[status(thm)],[ax1210]) ).
thf(c_0_31,plain,
! [X5044: a,X5045: list_a] :
( ~ p57
| ( fnil_a
!= ( fcons_a @ X5044 @ X5045 ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax57])])])]) ).
thf(c_0_32,plain,
! [X5042: list_a] :
( ~ p58
| ( ( fappend_a @ fnil_a @ X5042 )
= X5042 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax58])])]) ).
thf(c_0_33,plain,
( ~ p542
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= ( fcons_a @ esk1117_0 @ esk1118_0 ) )
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= fnil_a ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax542])])])]) ).
thf(c_0_34,plain,
( p542
| ~ p49 ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
thf(c_0_35,plain,
p49,
inference(split_conjunct,[status(thm)],[ax1712]) ).
thf(c_0_36,plain,
! [X6: a,X1: list_a] :
( ~ p69
| ( ( fcons_a @ X6 @ X1 )
!= X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
thf(c_0_37,plain,
p69,
inference(split_conjunct,[status(thm)],[ax1692]) ).
thf(c_0_38,plain,
( ~ p197
| p1728 ),
inference(fof_simplification,[status(thm)],[ax11]) ).
thf(c_0_39,plain,
( p197
| ~ p16 ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_40,plain,
p16,
inference(split_conjunct,[status(thm)],[ax1745]) ).
thf(c_0_41,plain,
! [X5006: a,X5007: list_a,X5008: list_a] :
( ~ p72
| ( ( fappend_a @ ( fcons_a @ X5006 @ X5007 ) @ X5008 )
= ( fcons_a @ X5006 @ ( fappend_a @ X5007 @ X5008 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax72])])]) ).
thf(c_0_42,plain,
( ~ p5
| ( fxs1
= ( freplicate_a @ fp @ fzero_zero_a ) ) ),
inference(fof_nnf,[status(thm)],[pax5]) ).
thf(c_0_43,plain,
( ~ p545
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
= ( fcons_a @ esk1111_0 @ esk1112_0 ) )
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
= fnil_a ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax545])])])]) ).
thf(c_0_44,plain,
( p545
| ~ p49 ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
thf(c_0_45,plain,
! [X6: a,X1: list_a] :
( ~ p57
| ( fnil_a
!= ( fcons_a @ X6 @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_46,plain,
p57,
inference(split_conjunct,[status(thm)],[ax1704]) ).
thf(c_0_47,plain,
! [X789: list_a,X790: list_a,X791: list_a] :
( ~ p1728
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
!= X789 )
| ( X790
!= ( fappend_a @ fnil_a @ X791 ) )
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ X790 )
= ( fappend_a @ X789 @ X791 ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1728])])]) ).
thf(c_0_48,plain,
! [X1: list_a] :
( ( ( fappend_a @ fnil_a @ X1 )
= X1 )
| ~ p58 ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_49,plain,
p58,
inference(split_conjunct,[status(thm)],[ax1703]) ).
thf(c_0_50,plain,
( ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= ( fcons_a @ esk1117_0 @ esk1118_0 ) )
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= fnil_a )
| ~ p542 ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_51,plain,
p542,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_35])]) ).
thf(c_0_52,plain,
! [X6: a,X1: list_a] :
( ( fcons_a @ X6 @ X1 )
!= X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_37])]) ).
thf(c_0_53,plain,
( p1728
| ~ p197 ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
thf(c_0_54,plain,
p197,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39,c_0_40])]) ).
thf(c_0_55,plain,
! [X1: list_a,X6: a,X2: list_a] :
( ( ( fappend_a @ ( fcons_a @ X6 @ X1 ) @ X2 )
= ( fcons_a @ X6 @ ( fappend_a @ X1 @ X2 ) ) )
| ~ p72 ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
thf(c_0_56,plain,
p72,
inference(split_conjunct,[status(thm)],[ax1689]) ).
thf(c_0_57,plain,
( ~ p6
| ( fxsa
= ( fappend_a @ fxs1 @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) ),
inference(fof_nnf,[status(thm)],[pax6]) ).
thf(c_0_58,plain,
( ~ p7
| p138 ),
inference(fof_simplification,[status(thm)],[ax1618]) ).
thf(c_0_59,plain,
( ( ( fdescar1375166517sums_a @ fxsa )
!= ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) )
| p98 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax98])]) ).
thf(c_0_60,plain,
( ( fxs1
= ( freplicate_a @ fp @ fzero_zero_a ) )
| ~ p5 ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
thf(c_0_61,plain,
p5,
inference(split_conjunct,[status(thm)],[ax1756]) ).
thf(c_0_62,plain,
~ p98,
inference(fof_simplification,[status(thm)],[ax1663]) ).
thf(c_0_63,plain,
( ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
= ( fcons_a @ esk1111_0 @ esk1112_0 ) )
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
= fnil_a )
| ~ p545 ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
thf(c_0_64,plain,
p545,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44,c_0_35])]) ).
thf(c_0_65,plain,
! [X6: a,X1: list_a] :
( ( fcons_a @ X6 @ X1 )
!= fnil_a ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45,c_0_46])]) ).
thf(c_0_66,plain,
! [X1: list_a,X2: list_a,X3: list_a] :
( ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ X2 )
= ( fappend_a @ X1 @ X3 ) )
| ~ p1728
| ( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
!= X1 )
| ( X2
!= ( fappend_a @ fnil_a @ X3 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
thf(c_0_67,plain,
! [X1: list_a] :
( ( fappend_a @ fnil_a @ X1 )
= X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48,c_0_49])]) ).
thf(c_0_68,plain,
( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fnil_a )
= ( fcons_a @ esk1117_0 @ esk1118_0 ) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50,c_0_51])]),c_0_52]) ).
thf(c_0_69,plain,
p1728,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53,c_0_54])]) ).
thf(c_0_70,plain,
! [X1: list_a,X6: a,X2: list_a] :
( ( fappend_a @ ( fcons_a @ X6 @ X1 ) @ X2 )
= ( fcons_a @ X6 @ ( fappend_a @ X1 @ X2 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55,c_0_56])]) ).
thf(c_0_71,plain,
( ( fxsa
= ( fappend_a @ fxs1 @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) )
| ~ p6 ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
thf(c_0_72,plain,
p6,
inference(split_conjunct,[status(thm)],[ax1755]) ).
thf(c_0_73,plain,
( ~ p138
| p1117 ),
inference(fof_simplification,[status(thm)],[ax620]) ).
thf(c_0_74,plain,
( p138
| ~ p7 ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
thf(c_0_75,plain,
p7,
inference(split_conjunct,[status(thm)],[ax1754]) ).
thf(c_0_76,plain,
( p98
| ( ( fdescar1375166517sums_a @ fxsa )
!= ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
thf(c_0_77,plain,
( ( freplicate_a @ fp @ fzero_zero_a )
= fxs1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60,c_0_61])]) ).
thf(c_0_78,plain,
~ p98,
inference(split_conjunct,[status(thm)],[c_0_62]) ).
thf(c_0_79,plain,
( ~ p1117
| ( ( fdescar1375166517sums_a @ ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) )
= ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) ) ),
inference(fof_nnf,[status(thm)],[pax1117]) ).
thf(c_0_80,plain,
( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 )
= ( fcons_a @ esk1111_0 @ esk1112_0 ) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63,c_0_64])]),c_0_65]) ).
thf(c_0_81,plain,
! [X1: list_a] :
( ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ X1 )
= ( fcons_a @ esk1117_0 @ ( fappend_a @ esk1118_0 @ X1 ) ) ),
inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_66,c_0_67]),c_0_68]),c_0_69])])])]),c_0_70]) ).
thf(c_0_82,plain,
( ( fappend_a @ fxs1 @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) )
= fxsa ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71,c_0_72])]) ).
thf(c_0_83,plain,
( p1117
| ~ p138 ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
thf(c_0_84,plain,
p138,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74,c_0_75])]) ).
thf(c_0_85,plain,
( ( fappend_a @ fxs1 @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) )
!= ( fdescar1375166517sums_a @ fxsa ) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_76,c_0_77]),c_0_78]) ).
thf(c_0_86,plain,
( ( ( fdescar1375166517sums_a @ ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) )
= ( fappend_a @ ( freplicate_a @ fp @ fzero_zero_a ) @ ( fdescar1375166517sums_a @ ( fcons_a @ ( fnth_a @ fxsa @ fp ) @ fxs2 ) ) ) )
| ~ p1117 ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
thf(c_0_87,plain,
( ( fcons_a @ esk1117_0 @ ( fappend_a @ esk1118_0 @ fxs2 ) )
= ( fcons_a @ esk1111_0 @ esk1112_0 ) ),
inference(rw,[status(thm)],[c_0_80,c_0_81]) ).
thf(c_0_88,plain,
( ( fappend_a @ fxs1 @ ( fcons_a @ esk1111_0 @ esk1112_0 ) )
= fxsa ),
inference(rw,[status(thm)],[c_0_82,c_0_80]) ).
thf(c_0_89,plain,
p1117,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83,c_0_84])]) ).
thf(c_0_90,plain,
( ( fappend_a @ fxs1 @ ( fdescar1375166517sums_a @ ( fcons_a @ esk1111_0 @ esk1112_0 ) ) )
!= ( fdescar1375166517sums_a @ fxsa ) ),
inference(rw,[status(thm)],[c_0_85,c_0_80]) ).
thf(c_0_91,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_86,c_0_77]),c_0_81]),c_0_87]),c_0_88]),c_0_77]),c_0_81]),c_0_87]),c_0_89])]),c_0_90]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
( ( descar1375166517sums_a @ xsa )
= ( append_a @ ( replicate_a @ p @ zero_zero_a ) @ ( descar1375166517sums_a @ ( cons_a @ ( nth_a @ xsa @ p ) @ xs2 ) ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP043^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n004.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 18:40:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 37.58/37.74 % SZS status Theorem
% 37.58/37.74 % Mode: mode478:USE_SINE=true:SINE_TOLERANCE=2.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=1.:SINE_DEPTH=0
% 37.58/37.74 % Inferences: 188
% 37.58/37.74 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------