%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG286^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n028.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:12:19 PM UTC 2025
% Result : Theorem 2.00s 2.17s
% Output : Proof 2.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 49
% Syntax : Number of formulae : 201 ( 59 unt; 0 typ; 0 def)
% Number of atoms : 633 ( 74 equ; 0 cnn)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 557 ( 223 ~; 190 |; 5 &; 109 @)
% ( 0 <=>; 24 =>; 6 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 61 ( 59 usr; 60 con; 0-2 aty)
% Number of variables : 28 ( 0 ^; 28 !; 0 ?; 28 :)
% Comments :
%------------------------------------------------------------------------------
thf(cPU_PAIR_NOT_ZERO_pme,conjecture,
( ~ ( ~ ( ~ ( ~ ( ( ( cL @ cZ )
= cZ )
=> ( ( cR @ cZ )
!= cZ ) )
=> ~ ! [X1: a,X2: a] :
( ( cL @ ( cP @ X1 @ X2 ) )
= X1 ) )
=> ~ ! [X1: a,X2: a] :
( ( cR @ ( cP @ X1 @ X2 ) )
= X2 ) )
=> ~ ! [X1: a] :
( ( X1 != cZ )
= ( X1
= ( cP @ ( cL @ X1 ) @ ( cR @ X1 ) ) ) ) )
=> ( ( u
= ( cP @ x @ y ) )
=> ( u != cZ ) ) ) ).
thf(h0,negated_conjecture,
~ ( ~ ( ~ ( ~ ( ~ ( ( ( cL @ cZ )
= cZ )
=> ( ( cR @ cZ )
!= cZ ) )
=> ~ ! [X1: a,X2: a] :
( ( cL @ ( cP @ X1 @ X2 ) )
= X1 ) )
=> ~ ! [X1: a,X2: a] :
( ( cR @ ( cP @ X1 @ X2 ) )
= X2 ) )
=> ~ ! [X1: a] :
( ( X1 != cZ )
= ( X1
= ( cP @ ( cL @ X1 ) @ ( cR @ X1 ) ) ) ) )
=> ( ( u
= ( cP @ x @ y ) )
=> ( u != cZ ) ) ),
inference(assume_negation,[status(cth)],[cPU_PAIR_NOT_ZERO_pme]) ).
thf(ax4529,axiom,
( p1
| ~ p3 ),
file('<stdin>',ax4529) ).
thf(ax4531,axiom,
~ p1,
file('<stdin>',ax4531) ).
thf(ax4530,axiom,
( p1
| ~ p2 ),
file('<stdin>',ax4530) ).
thf(ax2713,axiom,
( p764
| ~ p5 ),
file('<stdin>',ax2713) ).
thf(ax4527,axiom,
( p3
| p5 ),
file('<stdin>',ax4527) ).
thf(ax2758,axiom,
( p926
| ~ p5 ),
file('<stdin>',ax2758) ).
thf(ax4491,axiom,
( ~ p17
| p39 ),
file('<stdin>',ax4491) ).
thf(ax4513,axiom,
( p2
| p17 ),
file('<stdin>',ax4513) ).
thf(ax4514,axiom,
( p2
| ~ p16 ),
file('<stdin>',ax4514) ).
thf(ax4465,axiom,
( ~ p7
| p62 ),
file('<stdin>',ax4465) ).
thf(ax4462,axiom,
( ~ p17
| p64 ),
file('<stdin>',ax4462) ).
thf(ax2774,axiom,
( ~ p624
| p717
| ~ p624
| ~ p770 ),
file('<stdin>',ax2774) ).
thf(ax2766,axiom,
( p770
| ~ p926
| ~ p764 ),
file('<stdin>',ax2766) ).
thf(ax3415,axiom,
( ~ p39
| ~ p221
| ~ p717 ),
file('<stdin>',ax3415) ).
thf(nax8,axiom,
( p8
<= ! [X1: a] :
( ( fu = X1 )
=> ( X1 = fu ) ) ),
file('<stdin>',nax8) ).
thf(nax3,axiom,
( p3
<= ( ( fu
= ( fcP @ fx @ fy ) )
=> ( fu != fcZ ) ) ),
file('<stdin>',nax3) ).
thf(ax3544,axiom,
( ~ p62
| p627 ),
file('<stdin>',ax3544) ).
thf(ax4526,axiom,
p7,
file('<stdin>',ax4526) ).
thf(ax3545,axiom,
( ~ p64
| p624
| p625 ),
file('<stdin>',ax3545) ).
thf(ax3094,axiom,
p221,
file('<stdin>',ax3094) ).
thf(ax4519,axiom,
( ~ p8
| p13 ),
file('<stdin>',ax4519) ).
thf(ax4500,axiom,
( ~ p17
| p26 ),
file('<stdin>',ax4500) ).
thf(ax4037,axiom,
( ~ p332
| p339 ),
file('<stdin>',ax4037) ).
thf(ax3934,axiom,
( p16
| p332 ),
file('<stdin>',ax3934) ).
thf(ax3562,axiom,
( ~ p338
| p613 ),
file('<stdin>',ax3562) ).
thf(ax3543,axiom,
( ~ p627
| ~ p625
| p626 ),
file('<stdin>',ax3543) ).
thf(ax4518,axiom,
( ~ p13
| ~ p4
| p12 ),
file('<stdin>',ax4518) ).
thf(ax4528,axiom,
( p3
| p4 ),
file('<stdin>',ax4528) ).
thf(ax4473,axiom,
( ~ p26
| ~ p5
| ~ p56 ),
file('<stdin>',ax4473) ).
thf(ax3365,axiom,
( ~ p322
| p744
| ~ p322
| ~ p748 ),
file('<stdin>',ax3365) ).
thf(ax4038,axiom,
( ~ p339
| p322 ),
file('<stdin>',ax4038) ).
thf(nax285,axiom,
( p285
<= ( ( fcP @ fx @ fy )
= fcZ ) ),
file('<stdin>',nax285) ).
thf(ax3307,axiom,
( ~ p613
| p776 ),
file('<stdin>',ax3307) ).
thf(ax4044,axiom,
p338,
file('<stdin>',ax4044) ).
thf(ax4324,axiom,
( ~ p4
| p56
| ~ p12
| ~ p152 ),
file('<stdin>',ax4324) ).
thf(nax16,axiom,
( p16
<= ( ~ ( ~ ( ( ( fcL @ fcZ )
= fcZ )
=> ( ( fcR @ fcZ )
!= fcZ ) )
=> ~ ! [X1: a,X2: a] :
( ( fcL @ ( fcP @ X1 @ X2 ) )
= X1 ) )
=> ~ ! [X1: a,X2: a] :
( ( fcR @ ( fcP @ X1 @ X2 ) )
= X2 ) ) ),
file('<stdin>',nax16) ).
thf(ax3351,axiom,
( p748
| ~ p285 ),
file('<stdin>',ax3351) ).
thf(ax4004,axiom,
( ~ p332
| p371 ),
file('<stdin>',ax4004) ).
thf(ax3306,axiom,
( ~ p776
| p769
| p775 ),
file('<stdin>',ax3306) ).
thf(ax3090,axiom,
( ~ p625
| p152
| ~ p769
| ~ p626 ),
file('<stdin>',ax3090) ).
thf(nax166,axiom,
( p166
<= ( ( fcR @ fu )
= fy ) ),
file('<stdin>',nax166) ).
thf(pax744,axiom,
( p744
=> ( fy
= ( fcR @ fcZ ) ) ),
file('<stdin>',pax744) ).
thf(ax3557,axiom,
( ~ p371
| p609 ),
file('<stdin>',ax3557) ).
thf(ax3304,axiom,
( ~ p774
| ~ p609
| ~ p773 ),
file('<stdin>',ax3304) ).
thf(ax3305,axiom,
( ~ p775
| p774 ),
file('<stdin>',ax3305) ).
thf(ax2666,axiom,
( p773
| ~ p782
| ~ p166 ),
file('<stdin>',ax2666) ).
thf(nax782,axiom,
( p782
<= ( ( fcL @ ( fcP @ ( fcL @ fu ) @ ( fcR @ fu ) ) )
= fx ) ),
file('<stdin>',nax782) ).
thf(c_0_47,plain,
( p1
| ~ p3 ),
inference(fof_simplification,[status(thm)],[ax4529]) ).
thf(c_0_48,plain,
~ p1,
inference(fof_simplification,[status(thm)],[ax4531]) ).
thf(c_0_49,plain,
( p1
| ~ p2 ),
inference(fof_simplification,[status(thm)],[ax4530]) ).
thf(c_0_50,plain,
( p1
| ~ p3 ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
thf(c_0_51,plain,
~ p1,
inference(split_conjunct,[status(thm)],[c_0_48]) ).
thf(c_0_52,plain,
( p1
| ~ p2 ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
thf(c_0_53,plain,
( p764
| ~ p5 ),
inference(fof_simplification,[status(thm)],[ax2713]) ).
thf(c_0_54,plain,
( p3
| p5 ),
inference(split_conjunct,[status(thm)],[ax4527]) ).
thf(c_0_55,plain,
~ p3,
inference(sr,[status(thm)],[c_0_50,c_0_51]) ).
thf(c_0_56,plain,
( p926
| ~ p5 ),
inference(fof_simplification,[status(thm)],[ax2758]) ).
thf(c_0_57,plain,
( ~ p17
| p39 ),
inference(fof_simplification,[status(thm)],[ax4491]) ).
thf(c_0_58,plain,
( p2
| p17 ),
inference(split_conjunct,[status(thm)],[ax4513]) ).
thf(c_0_59,plain,
~ p2,
inference(sr,[status(thm)],[c_0_52,c_0_51]) ).
thf(c_0_60,plain,
( p2
| ~ p16 ),
inference(fof_simplification,[status(thm)],[ax4514]) ).
thf(c_0_61,plain,
( ~ p7
| p62 ),
inference(fof_simplification,[status(thm)],[ax4465]) ).
thf(c_0_62,plain,
( ~ p17
| p64 ),
inference(fof_simplification,[status(thm)],[ax4462]) ).
thf(c_0_63,plain,
( ~ p624
| p717
| ~ p624
| ~ p770 ),
inference(fof_simplification,[status(thm)],[ax2774]) ).
thf(c_0_64,plain,
( p770
| ~ p926
| ~ p764 ),
inference(fof_simplification,[status(thm)],[ax2766]) ).
thf(c_0_65,plain,
( p764
| ~ p5 ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
thf(c_0_66,plain,
p5,
inference(sr,[status(thm)],[c_0_54,c_0_55]) ).
thf(c_0_67,plain,
( p926
| ~ p5 ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
thf(c_0_68,plain,
( ~ p39
| ~ p221
| ~ p717 ),
inference(fof_simplification,[status(thm)],[ax3415]) ).
thf(c_0_69,plain,
( p39
| ~ p17 ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
thf(c_0_70,plain,
p17,
inference(sr,[status(thm)],[c_0_58,c_0_59]) ).
thf(c_0_71,plain,
( ( ( fu = esk446_0 )
| p8 )
& ( ( esk446_0 != fu )
| p8 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax8])])])])]) ).
thf(c_0_72,plain,
( p2
| ~ p16 ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
thf(c_0_73,plain,
( ( ( fu
= ( fcP @ fx @ fy ) )
| p3 )
& ( ( fu = fcZ )
| p3 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])]) ).
thf(c_0_74,plain,
( ~ p62
| p627 ),
inference(fof_simplification,[status(thm)],[ax3544]) ).
thf(c_0_75,plain,
( p62
| ~ p7 ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
thf(c_0_76,plain,
p7,
inference(split_conjunct,[status(thm)],[ax4526]) ).
thf(c_0_77,plain,
( ~ p64
| p624
| p625 ),
inference(fof_simplification,[status(thm)],[ax3545]) ).
thf(c_0_78,plain,
( p64
| ~ p17 ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
thf(c_0_79,plain,
( p717
| ~ p624
| ~ p624
| ~ p770 ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
thf(c_0_80,plain,
( p770
| ~ p926
| ~ p764 ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
thf(c_0_81,plain,
p764,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65,c_0_66])]) ).
thf(c_0_82,plain,
p926,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67,c_0_66])]) ).
thf(c_0_83,plain,
( ~ p39
| ~ p221
| ~ p717 ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
thf(c_0_84,plain,
p39,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69,c_0_70])]) ).
thf(c_0_85,plain,
p221,
inference(split_conjunct,[status(thm)],[ax3094]) ).
thf(c_0_86,plain,
( ~ p8
| p13 ),
inference(fof_simplification,[status(thm)],[ax4519]) ).
thf(c_0_87,plain,
( ( fu = esk446_0 )
| p8 ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
thf(c_0_88,plain,
( p8
| ( esk446_0 != fu ) ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
thf(c_0_89,plain,
( ~ p17
| p26 ),
inference(fof_simplification,[status(thm)],[ax4500]) ).
thf(c_0_90,plain,
( ~ p332
| p339 ),
inference(fof_simplification,[status(thm)],[ax4037]) ).
thf(c_0_91,plain,
( p16
| p332 ),
inference(split_conjunct,[status(thm)],[ax3934]) ).
thf(c_0_92,plain,
~ p16,
inference(sr,[status(thm)],[c_0_72,c_0_59]) ).
thf(c_0_93,plain,
( ( fu = fcZ )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
thf(c_0_94,plain,
( ~ p338
| p613 ),
inference(fof_simplification,[status(thm)],[ax3562]) ).
thf(c_0_95,plain,
( ~ p627
| ~ p625
| p626 ),
inference(fof_simplification,[status(thm)],[ax3543]) ).
thf(c_0_96,plain,
( p627
| ~ p62 ),
inference(split_conjunct,[status(thm)],[c_0_74]) ).
thf(c_0_97,plain,
p62,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_75,c_0_76])]) ).
thf(c_0_98,plain,
( p624
| p625
| ~ p64 ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
thf(c_0_99,plain,
p64,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78,c_0_70])]) ).
thf(c_0_100,plain,
( p717
| ~ p624
| ~ p770 ),
inference(cn,[status(thm)],[c_0_79]) ).
thf(c_0_101,plain,
p770,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_80,c_0_81]),c_0_82])]) ).
thf(c_0_102,plain,
~ p717,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_83,c_0_84]),c_0_85])]) ).
thf(c_0_103,plain,
( ~ p13
| ~ p4
| p12 ),
inference(fof_simplification,[status(thm)],[ax4518]) ).
thf(c_0_104,plain,
( p3
| p4 ),
inference(split_conjunct,[status(thm)],[ax4528]) ).
thf(c_0_105,plain,
( p13
| ~ p8 ),
inference(split_conjunct,[status(thm)],[c_0_86]) ).
thf(c_0_106,plain,
p8,
inference(csr,[status(thm)],[c_0_87,c_0_88]) ).
thf(c_0_107,plain,
( ~ p26
| ~ p5
| ~ p56 ),
inference(fof_simplification,[status(thm)],[ax4473]) ).
thf(c_0_108,plain,
( p26
| ~ p17 ),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
thf(c_0_109,plain,
( ~ p322
| p744
| ~ p322
| ~ p748 ),
inference(fof_simplification,[status(thm)],[ax3365]) ).
thf(c_0_110,plain,
( ~ p339
| p322 ),
inference(fof_simplification,[status(thm)],[ax4038]) ).
thf(c_0_111,plain,
( p339
| ~ p332 ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
thf(c_0_112,plain,
p332,
inference(sr,[status(thm)],[c_0_91,c_0_92]) ).
thf(c_0_113,plain,
( ( ( fcP @ fx @ fy )
!= fcZ )
| p285 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax285])]) ).
thf(c_0_114,plain,
( ( fu
= ( fcP @ fx @ fy ) )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
thf(c_0_115,plain,
fu = fcZ,
inference(sr,[status(thm)],[c_0_93,c_0_55]) ).
thf(c_0_116,plain,
( ~ p613
| p776 ),
inference(fof_simplification,[status(thm)],[ax3307]) ).
thf(c_0_117,plain,
( p613
| ~ p338 ),
inference(split_conjunct,[status(thm)],[c_0_94]) ).
thf(c_0_118,plain,
p338,
inference(split_conjunct,[status(thm)],[ax4044]) ).
thf(c_0_119,plain,
( p626
| ~ p627
| ~ p625 ),
inference(split_conjunct,[status(thm)],[c_0_95]) ).
thf(c_0_120,plain,
p627,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96,c_0_97])]) ).
thf(c_0_121,plain,
( p625
| p624 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98,c_0_99])]) ).
thf(c_0_122,plain,
~ p624,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_100,c_0_101])]),c_0_102]) ).
thf(c_0_123,plain,
( ~ p4
| p56
| ~ p12
| ~ p152 ),
inference(fof_simplification,[status(thm)],[ax4324]) ).
thf(c_0_124,plain,
( p12
| ~ p13
| ~ p4 ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
thf(c_0_125,plain,
p4,
inference(sr,[status(thm)],[c_0_104,c_0_55]) ).
thf(c_0_126,plain,
p13,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_105,c_0_106])]) ).
thf(c_0_127,plain,
( ~ p26
| ~ p5
| ~ p56 ),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
thf(c_0_128,plain,
p26,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_108,c_0_70])]) ).
thf(c_0_129,plain,
! [X885: a,X886: a,X887: a,X888: a] :
( ( ( ( fcL @ fcZ )
= fcZ )
| p16 )
& ( ( ( fcR @ fcZ )
= fcZ )
| p16 )
& ( ( ( fcL @ ( fcP @ X885 @ X886 ) )
= X885 )
| p16 )
& ( ( ( fcR @ ( fcP @ X887 @ X888 ) )
= X888 )
| p16 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax16])])])])]) ).
thf(c_0_130,plain,
( p744
| ~ p322
| ~ p322
| ~ p748 ),
inference(split_conjunct,[status(thm)],[c_0_109]) ).
thf(c_0_131,plain,
( p322
| ~ p339 ),
inference(split_conjunct,[status(thm)],[c_0_110]) ).
thf(c_0_132,plain,
p339,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_111,c_0_112])]) ).
thf(c_0_133,plain,
( p748
| ~ p285 ),
inference(fof_simplification,[status(thm)],[ax3351]) ).
thf(c_0_134,plain,
( p285
| ( ( fcP @ fx @ fy )
!= fcZ ) ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_135,plain,
( ( fcP @ fx @ fy )
= fcZ ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_114,c_0_115]),c_0_55]) ).
thf(c_0_136,plain,
( ~ p332
| p371 ),
inference(fof_simplification,[status(thm)],[ax4004]) ).
thf(c_0_137,plain,
( ~ p776
| p769
| p775 ),
inference(fof_simplification,[status(thm)],[ax3306]) ).
thf(c_0_138,plain,
( p776
| ~ p613 ),
inference(split_conjunct,[status(thm)],[c_0_116]) ).
thf(c_0_139,plain,
p613,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117,c_0_118])]) ).
thf(c_0_140,plain,
( ~ p625
| p152
| ~ p769
| ~ p626 ),
inference(fof_simplification,[status(thm)],[ax3090]) ).
thf(c_0_141,plain,
( p626
| ~ p625 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_119,c_0_120])]) ).
thf(c_0_142,plain,
p625,
inference(sr,[status(thm)],[c_0_121,c_0_122]) ).
thf(c_0_143,plain,
( p56
| ~ p4
| ~ p12
| ~ p152 ),
inference(split_conjunct,[status(thm)],[c_0_123]) ).
thf(c_0_144,plain,
p12,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_124,c_0_125]),c_0_126])]) ).
thf(c_0_145,plain,
~ p56,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_127,c_0_66]),c_0_128])]) ).
thf(c_0_146,plain,
( ( ( fcR @ fu )
!= fy )
| p166 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax166])]) ).
thf(c_0_147,plain,
( ~ p744
| ( fy
= ( fcR @ fcZ ) ) ),
inference(fof_nnf,[status(thm)],[pax744]) ).
thf(c_0_148,plain,
( ( ( fcR @ fcZ )
= fcZ )
| p16 ),
inference(split_conjunct,[status(thm)],[c_0_129]) ).
thf(c_0_149,plain,
( p744
| ~ p322
| ~ p748 ),
inference(cn,[status(thm)],[c_0_130]) ).
thf(c_0_150,plain,
p322,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131,c_0_132])]) ).
thf(c_0_151,plain,
( p748
| ~ p285 ),
inference(split_conjunct,[status(thm)],[c_0_133]) ).
thf(c_0_152,plain,
p285,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_134,c_0_135])]) ).
thf(c_0_153,plain,
( ~ p371
| p609 ),
inference(fof_simplification,[status(thm)],[ax3557]) ).
thf(c_0_154,plain,
( p371
| ~ p332 ),
inference(split_conjunct,[status(thm)],[c_0_136]) ).
thf(c_0_155,plain,
( p769
| p775
| ~ p776 ),
inference(split_conjunct,[status(thm)],[c_0_137]) ).
thf(c_0_156,plain,
p776,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_138,c_0_139])]) ).
thf(c_0_157,plain,
( p152
| ~ p625
| ~ p769
| ~ p626 ),
inference(split_conjunct,[status(thm)],[c_0_140]) ).
thf(c_0_158,plain,
p626,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141,c_0_142])]) ).
thf(c_0_159,plain,
~ p152,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_143,c_0_125]),c_0_144])]),c_0_145]) ).
thf(c_0_160,plain,
( p166
| ( ( fcR @ fu )
!= fy ) ),
inference(split_conjunct,[status(thm)],[c_0_146]) ).
thf(c_0_161,plain,
( ( fy
= ( fcR @ fcZ ) )
| ~ p744 ),
inference(split_conjunct,[status(thm)],[c_0_147]) ).
thf(c_0_162,plain,
( ( fcR @ fcZ )
= fcZ ),
inference(sr,[status(thm)],[c_0_148,c_0_92]) ).
thf(c_0_163,plain,
( p744
| ~ p748 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_149,c_0_150])]) ).
thf(c_0_164,plain,
p748,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_151,c_0_152])]) ).
thf(c_0_165,plain,
( ~ p774
| ~ p609
| ~ p773 ),
inference(fof_simplification,[status(thm)],[ax3304]) ).
thf(c_0_166,plain,
( p609
| ~ p371 ),
inference(split_conjunct,[status(thm)],[c_0_153]) ).
thf(c_0_167,plain,
p371,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_154,c_0_112])]) ).
thf(c_0_168,plain,
( ~ p775
| p774 ),
inference(fof_simplification,[status(thm)],[ax3305]) ).
thf(c_0_169,plain,
( p775
| p769 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_155,c_0_156])]) ).
thf(c_0_170,plain,
~ p769,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_157,c_0_142]),c_0_158])]),c_0_159]) ).
thf(c_0_171,plain,
( p166
| ( ( fcR @ fcZ )
!= fy ) ),
inference(rw,[status(thm)],[c_0_160,c_0_115]) ).
thf(c_0_172,plain,
( ( fy = fcZ )
| ~ p744 ),
inference(rw,[status(thm)],[c_0_161,c_0_162]) ).
thf(c_0_173,plain,
p744,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_163,c_0_164])]) ).
thf(c_0_174,plain,
( ~ p774
| ~ p609
| ~ p773 ),
inference(split_conjunct,[status(thm)],[c_0_165]) ).
thf(c_0_175,plain,
p609,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_166,c_0_167])]) ).
thf(c_0_176,plain,
( p774
| ~ p775 ),
inference(split_conjunct,[status(thm)],[c_0_168]) ).
thf(c_0_177,plain,
p775,
inference(sr,[status(thm)],[c_0_169,c_0_170]) ).
thf(c_0_178,plain,
( p773
| ~ p782
| ~ p166 ),
inference(fof_simplification,[status(thm)],[ax2666]) ).
thf(c_0_179,plain,
( p166
| ( fy != fcZ ) ),
inference(rw,[status(thm)],[c_0_171,c_0_162]) ).
thf(c_0_180,plain,
fy = fcZ,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_172,c_0_173])]) ).
thf(c_0_181,plain,
( ~ p773
| ~ p774 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_174,c_0_175])]) ).
thf(c_0_182,plain,
p774,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_176,c_0_177])]) ).
thf(c_0_183,plain,
( ( ( fcL @ ( fcP @ ( fcL @ fu ) @ ( fcR @ fu ) ) )
!= fx )
| p782 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax782])]) ).
thf(c_0_184,plain,
( ( ( fcL @ fcZ )
= fcZ )
| p16 ),
inference(split_conjunct,[status(thm)],[c_0_129]) ).
thf(c_0_185,plain,
( p773
| ~ p782
| ~ p166 ),
inference(split_conjunct,[status(thm)],[c_0_178]) ).
thf(c_0_186,plain,
p166,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_179,c_0_180])]) ).
thf(c_0_187,plain,
~ p773,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_181,c_0_182])]) ).
thf(c_0_188,plain,
( p782
| ( ( fcL @ ( fcP @ ( fcL @ fu ) @ ( fcR @ fu ) ) )
!= fx ) ),
inference(split_conjunct,[status(thm)],[c_0_183]) ).
thf(c_0_189,plain,
( ( fcL @ fcZ )
= fcZ ),
inference(sr,[status(thm)],[c_0_184,c_0_92]) ).
thf(c_0_190,plain,
~ p782,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_185,c_0_186])]),c_0_187]) ).
thf(c_0_191,plain,
! [X2: a,X1: a] :
( ( ( fcL @ ( fcP @ X1 @ X2 ) )
= X1 )
| p16 ),
inference(split_conjunct,[status(thm)],[c_0_129]) ).
thf(c_0_192,plain,
( ( fcL @ ( fcP @ fcZ @ fcZ ) )
!= fx ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_188,c_0_115]),c_0_189]),c_0_115]),c_0_162]),c_0_190]) ).
thf(c_0_193,plain,
! [X2: a,X1: a] :
( ( fcL @ ( fcP @ X1 @ X2 ) )
= X1 ),
inference(sr,[status(thm)],[c_0_191,c_0_92]) ).
thf(c_0_194,plain,
( ( fcP @ fx @ fcZ )
= fcZ ),
inference(rw,[status(thm)],[c_0_135,c_0_180]) ).
thf(c_0_195,plain,
fx != fcZ,
inference(rw,[status(thm)],[c_0_192,c_0_193]) ).
thf(c_0_196,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_193,c_0_194]),c_0_189]),c_0_195]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
( ~ ( ~ ( ~ ( ~ ( ( ( cL @ cZ )
= cZ )
=> ( ( cR @ cZ )
!= cZ ) )
=> ~ ! [X1: a,X2: a] :
( ( cL @ ( cP @ X1 @ X2 ) )
= X1 ) )
=> ~ ! [X1: a,X2: a] :
( ( cR @ ( cP @ X1 @ X2 ) )
= X2 ) )
=> ~ ! [X1: a] :
( ( X1 != cZ )
= ( X1
= ( cP @ ( cL @ X1 ) @ ( cR @ X1 ) ) ) ) )
=> ( ( u
= ( cP @ x @ y ) )
=> ( u != cZ ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG286^5 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 8 23:36:23 EDT 2025
% 0.14/0.35 % CPUTime :
% 2.00/2.17 % SZS status Theorem
% 2.00/2.17 % Mode: mode506
% 2.00/2.17 % Inferences: 37903
% 2.00/2.17 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------