%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG271^5 : TPTP v9.2.0. Bugfixed v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n022.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:17 PM UTC 2025
% Result : Theorem 76.44s 76.22s
% Output : Proof 76.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 40
% Syntax : Number of formulae : 152 ( 44 unt; 0 typ; 7 def)
% Number of atoms : 690 ( 132 equ; 0 cnn)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 857 ( 214 ~; 142 |; 9 &; 445 @)
% ( 0 <=>; 42 =>; 5 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 20 ( 20 >; 0 *; 0 +; 0 <<)
% Number of symbols : 39 ( 37 usr; 38 con; 0-2 aty)
% Number of variables : 158 ( 13 ^; 145 !; 0 ?; 158 :)
% Comments :
%------------------------------------------------------------------------------
thf(def_cGRP_ASSOC,definition,
( cGRP_ASSOC
= ( ^ [X1: g > g > g] :
! [X2: g,X3: g,X4: g] :
( ( X1 @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ X2 @ ( X1 @ X3 @ X4 ) ) ) ) ) ).
thf(def_cGRP_INVERSE,definition,
( cGRP_INVERSE
= ( ^ [X1: g > g > g,X2: g] :
! [X3: g] :
~ ! [X4: g] :
( ( ( X1 @ X3 @ X4 )
= X2 )
=> ( ( X1 @ X4 @ X3 )
!= X2 ) ) ) ) ).
thf(def_cGRP_RIGHT_INVERSE,definition,
( cGRP_RIGHT_INVERSE
= ( ^ [X1: g > g > g,X2: g] :
! [X3: g] :
~ ! [X4: g] :
( ( X1 @ X3 @ X4 )
!= X2 ) ) ) ).
thf(def_cGRP_RIGHT_UNIT,definition,
( cGRP_RIGHT_UNIT
= ( ^ [X1: g > g > g,X2: g] :
! [X3: g] :
( ( X1 @ X3 @ X2 )
= X3 ) ) ) ).
thf(def_cGRP_UNIT,definition,
( cGRP_UNIT
= ( ^ [X1: g > g > g,X2: g] :
! [X3: g] :
~ ( ( ( X1 @ X2 @ X3 )
= X3 )
=> ( ( X1 @ X3 @ X2 )
!= X3 ) ) ) ) ).
thf(def_cGROUP1,definition,
( cGROUP1
= ( ^ [X1: g > g > g,X2: g] :
~ ( ~ ( ( cGRP_ASSOC @ X1 )
=> ~ ( cGRP_UNIT @ X1 @ X2 ) )
=> ~ ( cGRP_INVERSE @ X1 @ X2 ) ) ) ) ).
thf(def_cGROUP3,definition,
( cGROUP3
= ( ^ [X1: g > g > g,X2: g] :
~ ( ~ ( ( cGRP_ASSOC @ X1 )
=> ~ ( cGRP_RIGHT_UNIT @ X1 @ X2 ) )
=> ~ ( cGRP_RIGHT_INVERSE @ X1 @ X2 ) ) ) ) ).
thf(cEQUIV_01_03,conjecture,
! [X1: g > g > g,X2: g] :
( ( ~ ( ~ ( ! [X3: g,X4: g,X5: g] :
( ( X1 @ ( X1 @ X3 @ X4 ) @ X5 )
= ( X1 @ X3 @ ( X1 @ X4 @ X5 ) ) )
=> ~ ! [X3: g] :
~ ( ( ( X1 @ X2 @ X3 )
= X3 )
=> ( ( X1 @ X3 @ X2 )
!= X3 ) ) )
=> ~ ! [X3: g] :
~ ! [X4: g] :
( ( ( X1 @ X3 @ X4 )
= X2 )
=> ( ( X1 @ X4 @ X3 )
!= X2 ) ) ) )
= ( ~ ( ~ ( ! [X3: g,X4: g,X5: g] :
( ( X1 @ ( X1 @ X3 @ X4 ) @ X5 )
= ( X1 @ X3 @ ( X1 @ X4 @ X5 ) ) )
=> ~ ! [X3: g] :
( ( X1 @ X3 @ X2 )
= X3 ) )
=> ~ ! [X3: g] :
~ ! [X4: g] :
( ( X1 @ X3 @ X4 )
!= X2 ) ) ) ) ).
thf(h0,negated_conjecture,
~ ! [X1: g > g > g,X2: g] :
( ( ~ ( ~ ( ! [X3: g,X4: g,X5: g] :
( ( X1 @ ( X1 @ X3 @ X4 ) @ X5 )
= ( X1 @ X3 @ ( X1 @ X4 @ X5 ) ) )
=> ~ ! [X3: g] :
~ ( ( ( X1 @ X2 @ X3 )
= X3 )
=> ( ( X1 @ X3 @ X2 )
!= X3 ) ) )
=> ~ ! [X3: g] :
~ ! [X4: g] :
( ( ( X1 @ X3 @ X4 )
= X2 )
=> ( ( X1 @ X4 @ X3 )
!= X2 ) ) ) )
= ( ~ ( ~ ( ! [X3: g,X4: g,X5: g] :
( ( X1 @ ( X1 @ X3 @ X4 ) @ X5 )
= ( X1 @ X3 @ ( X1 @ X4 @ X5 ) ) )
=> ~ ! [X3: g] :
( ( X1 @ X3 @ X2 )
= X3 ) )
=> ~ ! [X3: g] :
~ ! [X4: g] :
( ( X1 @ X3 @ X4 )
!= X2 ) ) ) ),
inference(assume_negation,[status(cth)],[cEQUIV_01_03]) ).
thf(ax1726,axiom,
( p1
| ~ p2 ),
file('<stdin>',ax1726) ).
thf(ax1727,axiom,
~ p1,
file('<stdin>',ax1727) ).
thf(ax1725,axiom,
( p2
| ~ p3 ),
file('<stdin>',ax1725) ).
thf(ax1717,axiom,
( p3
| ~ p10
| ~ p11 ),
file('<stdin>',ax1717) ).
thf(ax1712,axiom,
( p11
| ~ p17 ),
file('<stdin>',ax1712) ).
thf(ax1709,axiom,
( p17
| p19 ),
file('<stdin>',ax1709) ).
thf(ax1706,axiom,
( p10
| ~ p12 ),
file('<stdin>',ax1706) ).
thf(ax1703,axiom,
( p12
| p15 ),
file('<stdin>',ax1703) ).
thf(ax1685,axiom,
( ~ p15
| ~ p37 ),
file('<stdin>',ax1685) ).
thf(pax82,axiom,
( p82
=> ! [X1: g] :
( ( f__0 @ f__7 @ X1 )
!= f__1 ) ),
file('<stdin>',pax82) ).
thf(ax1701,axiom,
( ~ p17
| ~ p14
| ~ p19 ),
file('<stdin>',ax1701) ).
thf(ax1702,axiom,
( ~ p11
| p17
| ~ p18 ),
file('<stdin>',ax1702) ).
thf(ax1710,axiom,
( p17
| p14 ),
file('<stdin>',ax1710) ).
thf(ax1704,axiom,
( p12
| p14 ),
file('<stdin>',ax1704) ).
thf(ax1682,axiom,
( ~ p19
| p23 ),
file('<stdin>',ax1682) ).
thf(ax1617,axiom,
( p37
| p23 ),
file('<stdin>',ax1617) ).
thf(ax1637,axiom,
( p18
| p82 ),
file('<stdin>',ax1637) ).
thf(nax10,axiom,
( p10
<= ( ~ ( ! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
=> ~ ! [X1: g] :
~ ( ( ( f__0 @ f__1 @ X1 )
= X1 )
=> ( ( f__0 @ X1 @ f__1 )
!= X1 ) ) )
=> ~ ! [X1: g] :
~ ! [X2: g] :
( ( ( f__0 @ X1 @ X2 )
= f__1 )
=> ( ( f__0 @ X2 @ X1 )
!= f__1 ) ) ) ),
file('<stdin>',nax10) ).
thf(ax1711,axiom,
( p11
| p18 ),
file('<stdin>',ax1711) ).
thf(ax1700,axiom,
( p19
| ~ p23 ),
file('<stdin>',ax1700) ).
thf(ax1716,axiom,
( p3
| p10
| p11 ),
file('<stdin>',ax1716) ).
thf(ax1659,axiom,
( ~ p18
| ~ p62 ),
file('<stdin>',ax1659) ).
thf(pax14,axiom,
( p14
=> ! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) ) ),
file('<stdin>',pax14) ).
thf(nax62,axiom,
( p62
<= ! [X1: g] :
( ( f__0 @ f__6 @ X1 )
!= f__1 ) ),
file('<stdin>',nax62) ).
thf(nax17,axiom,
( p17
<= ( ! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
=> ~ ! [X1: g] :
( ( f__0 @ X1 @ f__1 )
= X1 ) ) ),
file('<stdin>',nax17) ).
thf(nax11,axiom,
( p11
<= ( ~ ( ! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
=> ~ ! [X1: g] :
( ( f__0 @ X1 @ f__1 )
= X1 ) )
=> ~ ! [X1: g] :
~ ! [X2: g] :
( ( f__0 @ X1 @ X2 )
!= f__1 ) ) ),
file('<stdin>',nax11) ).
thf(pax10,axiom,
( p10
=> ( ~ ( ! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
=> ~ ! [X1: g] :
~ ( ( ( f__0 @ f__1 @ X1 )
= X1 )
=> ( ( f__0 @ X1 @ f__1 )
!= X1 ) ) )
=> ~ ! [X1: g] :
~ ! [X2: g] :
( ( ( f__0 @ X1 @ X2 )
= f__1 )
=> ( ( f__0 @ X2 @ X1 )
!= f__1 ) ) ) ),
file('<stdin>',pax10) ).
thf(nax12,axiom,
( p12
<= ( ! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
=> ~ ! [X1: g] :
~ ( ( ( f__0 @ f__1 @ X1 )
= X1 )
=> ( ( f__0 @ X1 @ f__1 )
!= X1 ) ) ) ),
file('<stdin>',nax12) ).
thf(ax1714,axiom,
( ~ p12
| ~ p14
| ~ p15 ),
file('<stdin>',ax1714) ).
thf(pax20,axiom,
( p20
=> ( ( ( f__0 @ f__1 @ f__3 )
= f__3 )
=> ( ( f__0 @ f__3 @ f__1 )
!= f__3 ) ) ),
file('<stdin>',pax20) ).
thf(ax1708,axiom,
( p15
| p20 ),
file('<stdin>',ax1708) ).
thf(c_0_31,plain,
( p1
| ~ p2 ),
inference(fof_simplification,[status(thm)],[ax1726]) ).
thf(c_0_32,plain,
~ p1,
inference(fof_simplification,[status(thm)],[ax1727]) ).
thf(c_0_33,plain,
( p2
| ~ p3 ),
inference(fof_simplification,[status(thm)],[ax1725]) ).
thf(c_0_34,plain,
( p1
| ~ p2 ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_35,plain,
~ p1,
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_36,plain,
( p3
| ~ p10
| ~ p11 ),
inference(fof_simplification,[status(thm)],[ax1717]) ).
thf(c_0_37,plain,
( p2
| ~ p3 ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_38,plain,
~ p2,
inference(sr,[status(thm)],[c_0_34,c_0_35]) ).
thf(c_0_39,plain,
( p11
| ~ p17 ),
inference(fof_simplification,[status(thm)],[ax1712]) ).
thf(c_0_40,plain,
( p3
| ~ p10
| ~ p11 ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
thf(c_0_41,plain,
~ p3,
inference(sr,[status(thm)],[c_0_37,c_0_38]) ).
thf(c_0_42,plain,
( p11
| ~ p17 ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
thf(c_0_43,plain,
( p17
| p19 ),
inference(split_conjunct,[status(thm)],[ax1709]) ).
thf(c_0_44,plain,
( p10
| ~ p12 ),
inference(fof_simplification,[status(thm)],[ax1706]) ).
thf(c_0_45,plain,
( ~ p10
| ~ p11 ),
inference(sr,[status(thm)],[c_0_40,c_0_41]) ).
thf(c_0_46,plain,
( p19
| p11 ),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
thf(c_0_47,plain,
( p10
| ~ p12 ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
thf(c_0_48,plain,
( p12
| p15 ),
inference(split_conjunct,[status(thm)],[ax1703]) ).
thf(c_0_49,plain,
( ~ p15
| ~ p37 ),
inference(fof_simplification,[status(thm)],[ax1685]) ).
thf(c_0_50,plain,
! [X368: g] :
( ~ p82
| ( ( f__0 @ f__7 @ X368 )
!= f__1 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax82])])])]) ).
thf(c_0_51,plain,
( ~ p17
| ~ p14
| ~ p19 ),
inference(fof_simplification,[status(thm)],[ax1701]) ).
thf(c_0_52,plain,
( ~ p11
| p17
| ~ p18 ),
inference(fof_simplification,[status(thm)],[ax1702]) ).
thf(c_0_53,plain,
( p17
| p14 ),
inference(split_conjunct,[status(thm)],[ax1710]) ).
thf(c_0_54,plain,
( p12
| p14 ),
inference(split_conjunct,[status(thm)],[ax1704]) ).
thf(c_0_55,plain,
( ~ p19
| p23 ),
inference(fof_simplification,[status(thm)],[ax1682]) ).
thf(c_0_56,plain,
( p19
| ~ p10 ),
inference(spm,[status(thm)],[c_0_45,c_0_46]) ).
thf(c_0_57,plain,
( p15
| p10 ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
thf(c_0_58,plain,
( ~ p15
| ~ p37 ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
thf(c_0_59,plain,
( p37
| p23 ),
inference(split_conjunct,[status(thm)],[ax1617]) ).
thf(c_0_60,plain,
! [X1: g] :
( ~ p82
| ( ( f__0 @ f__7 @ X1 )
!= f__1 ) ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
thf(c_0_61,plain,
( p18
| p82 ),
inference(split_conjunct,[status(thm)],[ax1637]) ).
thf(c_0_62,plain,
! [X504: g,X505: g,X506: g,X507: g,X508: g] :
( ( ( ( f__0 @ ( f__0 @ X504 @ X505 ) @ X506 )
= ( f__0 @ X504 @ ( f__0 @ X505 @ X506 ) ) )
| p10 )
& ( ( ( f__0 @ f__1 @ X507 )
= X507 )
| p10 )
& ( ( ( f__0 @ X507 @ f__1 )
= X507 )
| p10 )
& ( ( ( f__0 @ X508 @ ( esk253_1 @ X508 ) )
= f__1 )
| p10 )
& ( ( ( f__0 @ ( esk253_1 @ X508 ) @ X508 )
= f__1 )
| p10 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax10])])])])])]) ).
thf(c_0_63,plain,
( p11
| p18 ),
inference(split_conjunct,[status(thm)],[ax1711]) ).
thf(c_0_64,plain,
( ~ p17
| ~ p14
| ~ p19 ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
thf(c_0_65,plain,
( p17
| ~ p11
| ~ p18 ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
thf(c_0_66,plain,
( p14
| p11 ),
inference(spm,[status(thm)],[c_0_42,c_0_53]) ).
thf(c_0_67,plain,
( p14
| p10 ),
inference(spm,[status(thm)],[c_0_47,c_0_54]) ).
thf(c_0_68,plain,
( p19
| ~ p23 ),
inference(fof_simplification,[status(thm)],[ax1700]) ).
thf(c_0_69,plain,
( p23
| ~ p19 ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
thf(c_0_70,plain,
( p15
| p19 ),
inference(spm,[status(thm)],[c_0_56,c_0_57]) ).
thf(c_0_71,plain,
( p23
| ~ p15 ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
thf(c_0_72,plain,
( p3
| p10
| p11 ),
inference(split_conjunct,[status(thm)],[ax1716]) ).
thf(c_0_73,plain,
( ~ p18
| ~ p62 ),
inference(fof_simplification,[status(thm)],[ax1659]) ).
thf(c_0_74,plain,
! [X1: g] :
( p18
| ( ( f__0 @ f__7 @ X1 )
!= f__1 ) ),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
thf(c_0_75,plain,
! [X1: g] :
( ( ( f__0 @ X1 @ ( esk253_1 @ X1 ) )
= f__1 )
| p10 ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
thf(c_0_76,plain,
( p18
| ~ p10 ),
inference(spm,[status(thm)],[c_0_45,c_0_63]) ).
thf(c_0_77,plain,
( ~ p14
| ~ p19
| ~ p11
| ~ p18 ),
inference(spm,[status(thm)],[c_0_64,c_0_65]) ).
thf(c_0_78,plain,
p14,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_66]),c_0_67]) ).
thf(c_0_79,plain,
( p19
| ~ p23 ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
thf(c_0_80,plain,
p23,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_71]) ).
thf(c_0_81,plain,
( p11
| p10 ),
inference(sr,[status(thm)],[c_0_72,c_0_41]) ).
thf(c_0_82,plain,
! [X468: g,X469: g,X470: g] :
( ~ p14
| ( ( f__0 @ ( f__0 @ X468 @ X469 ) @ X470 )
= ( f__0 @ X468 @ ( f__0 @ X469 @ X470 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax14])])]) ).
thf(c_0_83,plain,
( ( ( f__0 @ f__6 @ esk196_0 )
= f__1 )
| p62 ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax62])])])]) ).
thf(c_0_84,plain,
( ~ p18
| ~ p62 ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
thf(c_0_85,plain,
p18,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_75]),c_0_76]) ).
thf(c_0_86,plain,
( ~ p19
| ~ p11
| ~ p18 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_77,c_0_78])]) ).
thf(c_0_87,plain,
p19,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_79,c_0_80])]) ).
thf(c_0_88,plain,
( p10
| ~ p14
| ~ p19
| ~ p18 ),
inference(spm,[status(thm)],[c_0_77,c_0_81]) ).
thf(c_0_89,plain,
! [X458: g,X459: g,X460: g,X461: g] :
( ( ( ( f__0 @ ( f__0 @ X458 @ X459 ) @ X460 )
= ( f__0 @ X458 @ ( f__0 @ X459 @ X460 ) ) )
| p17 )
& ( ( ( f__0 @ X461 @ f__1 )
= X461 )
| p17 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax17])])])])]) ).
thf(c_0_90,plain,
( ~ p17
| ~ p19 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64,c_0_78])]) ).
thf(c_0_91,plain,
! [X1: g,X2: g,X3: g] :
( ( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
| ~ p14 ),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
thf(c_0_92,plain,
( ( ( f__0 @ f__6 @ esk196_0 )
= f__1 )
| p62 ),
inference(split_conjunct,[status(thm)],[c_0_83]) ).
thf(c_0_93,plain,
~ p62,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_84,c_0_85])]) ).
thf(c_0_94,plain,
! [X492: g,X493: g,X494: g,X495: g,X496: g] :
( ( ( ( f__0 @ ( f__0 @ X492 @ X493 ) @ X494 )
= ( f__0 @ X492 @ ( f__0 @ X493 @ X494 ) ) )
| p11 )
& ( ( ( f__0 @ X495 @ f__1 )
= X495 )
| p11 )
& ( ( ( f__0 @ X496 @ ( esk247_1 @ X496 ) )
= f__1 )
| p11 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax11])])])])])]) ).
thf(c_0_95,plain,
( ~ p11
| ~ p18 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_86,c_0_87])]) ).
thf(c_0_96,plain,
( p10
| ~ p19
| ~ p18 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88,c_0_78])]) ).
thf(c_0_97,plain,
! [X1: g] :
( ( ( f__0 @ X1 @ f__1 )
= X1 )
| p17 ),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
thf(c_0_98,plain,
~ p17,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90,c_0_87])]) ).
thf(c_0_99,plain,
! [X1: g,X2: g,X3: g] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_91,c_0_78])]) ).
thf(c_0_100,plain,
( ( f__0 @ f__6 @ esk196_0 )
= f__1 ),
inference(sr,[status(thm)],[c_0_92,c_0_93]) ).
thf(c_0_101,plain,
! [X1: g] :
( ( ( f__0 @ X1 @ ( esk247_1 @ X1 ) )
= f__1 )
| p11 ),
inference(split_conjunct,[status(thm)],[c_0_94]) ).
thf(c_0_102,plain,
~ p11,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95,c_0_85])]) ).
thf(c_0_103,plain,
! [X503: g] :
( ~ p10
| ( ( f__0 @ ( f__0 @ esk248_0 @ esk249_0 ) @ esk250_0 )
!= ( f__0 @ esk248_0 @ ( f__0 @ esk249_0 @ esk250_0 ) ) )
| ( ( f__0 @ f__1 @ esk251_0 )
!= esk251_0 )
| ( ( f__0 @ esk251_0 @ f__1 )
!= esk251_0 )
| ( ( f__0 @ esk252_0 @ X503 )
!= f__1 )
| ( ( f__0 @ X503 @ esk252_0 )
!= f__1 ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax10])])])])]) ).
thf(c_0_104,plain,
( p10
| ~ p18 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96,c_0_87])]) ).
thf(c_0_105,plain,
! [X1: g] :
( ( f__0 @ X1 @ f__1 )
= X1 ),
inference(sr,[status(thm)],[c_0_97,c_0_98]) ).
thf(c_0_106,plain,
! [X1: g] :
( ( f__0 @ f__6 @ ( f__0 @ esk196_0 @ X1 ) )
= ( f__0 @ f__1 @ X1 ) ),
inference(spm,[status(thm)],[c_0_99,c_0_100]) ).
thf(c_0_107,plain,
! [X1: g] :
( ( f__0 @ X1 @ ( esk247_1 @ X1 ) )
= f__1 ),
inference(sr,[status(thm)],[c_0_101,c_0_102]) ).
thf(c_0_108,plain,
! [X1: g] :
( ~ p10
| ( ( f__0 @ ( f__0 @ esk248_0 @ esk249_0 ) @ esk250_0 )
!= ( f__0 @ esk248_0 @ ( f__0 @ esk249_0 @ esk250_0 ) ) )
| ( ( f__0 @ f__1 @ esk251_0 )
!= esk251_0 )
| ( ( f__0 @ esk251_0 @ f__1 )
!= esk251_0 )
| ( ( f__0 @ esk252_0 @ X1 )
!= f__1 )
| ( ( f__0 @ X1 @ esk252_0 )
!= f__1 ) ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
thf(c_0_109,plain,
p10,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104,c_0_85])]) ).
thf(c_0_110,plain,
! [X1: g,X2: g] :
( ( f__0 @ X1 @ ( f__0 @ f__1 @ X2 ) )
= ( f__0 @ X1 @ X2 ) ),
inference(spm,[status(thm)],[c_0_99,c_0_105]) ).
thf(c_0_111,plain,
( ( f__0 @ f__1 @ ( esk247_1 @ esk196_0 ) )
= f__6 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_107]),c_0_105]) ).
thf(c_0_112,plain,
! [X1: g] :
( ( ( f__0 @ f__1 @ esk251_0 )
!= esk251_0 )
| ( ( f__0 @ X1 @ esk252_0 )
!= f__1 )
| ( ( f__0 @ esk252_0 @ X1 )
!= f__1 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_108,c_0_99]),c_0_105]),c_0_109])]) ).
thf(c_0_113,plain,
! [X482: g,X483: g,X484: g,X485: g] :
( ( ( ( f__0 @ ( f__0 @ X482 @ X483 ) @ X484 )
= ( f__0 @ X482 @ ( f__0 @ X483 @ X484 ) ) )
| p12 )
& ( ( ( f__0 @ f__1 @ X485 )
= X485 )
| p12 )
& ( ( ( f__0 @ X485 @ f__1 )
= X485 )
| p12 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax12])])])])]) ).
thf(c_0_114,plain,
! [X1: g] :
( ( f__0 @ X1 @ ( esk247_1 @ esk196_0 ) )
= ( f__0 @ X1 @ f__6 ) ),
inference(spm,[status(thm)],[c_0_110,c_0_111]) ).
thf(c_0_115,plain,
! [X1: g,X2: g] :
( ( f__0 @ X1 @ ( f__0 @ ( esk247_1 @ X1 ) @ X2 ) )
= ( f__0 @ f__1 @ X2 ) ),
inference(spm,[status(thm)],[c_0_99,c_0_107]) ).
thf(c_0_116,plain,
! [X1: g,X2: g] :
( ( ( f__0 @ X1 @ ( f__0 @ X2 @ esk252_0 ) )
!= f__1 )
| ( ( f__0 @ esk252_0 @ ( f__0 @ X1 @ X2 ) )
!= f__1 )
| ( ( f__0 @ f__1 @ esk251_0 )
!= esk251_0 ) ),
inference(spm,[status(thm)],[c_0_112,c_0_99]) ).
thf(c_0_117,plain,
! [X1: g,X2: g,X3: g] :
( ( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
| p12 ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_118,plain,
! [X1: g] :
( ( ( f__0 @ f__1 @ X1 )
= X1 )
| p12 ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_119,plain,
( ( f__0 @ esk196_0 @ f__6 )
= f__1 ),
inference(spm,[status(thm)],[c_0_107,c_0_114]) ).
thf(c_0_120,plain,
! [X1: g] :
( ( f__0 @ f__1 @ ( esk247_1 @ ( esk247_1 @ X1 ) ) )
= X1 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115,c_0_107]),c_0_105]) ).
thf(c_0_121,plain,
( ~ p12
| ~ p14
| ~ p15 ),
inference(fof_simplification,[status(thm)],[ax1714]) ).
thf(c_0_122,plain,
! [X1: g,X2: g,X3: g] :
( p12
| ( ( f__0 @ X1 @ ( f__0 @ X2 @ ( f__0 @ X3 @ esk252_0 ) ) )
!= f__1 )
| ( ( f__0 @ esk252_0 @ ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) )
!= f__1 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_117]),c_0_118]) ).
thf(c_0_123,plain,
! [X1: g] :
( ( f__0 @ esk196_0 @ ( f__0 @ f__6 @ X1 ) )
= ( f__0 @ f__1 @ X1 ) ),
inference(spm,[status(thm)],[c_0_99,c_0_119]) ).
thf(c_0_124,plain,
! [X1: g] :
( ( ( esk247_1 @ ( esk247_1 @ X1 ) )
= X1 )
| p12 ),
inference(spm,[status(thm)],[c_0_118,c_0_120]) ).
thf(c_0_125,plain,
( ~ p12
| ~ p14
| ~ p15 ),
inference(split_conjunct,[status(thm)],[c_0_121]) ).
thf(c_0_126,plain,
! [X1: g] :
( p12
| ( ( f__0 @ X1 @ esk252_0 )
!= f__1 )
| ( ( f__0 @ esk252_0 @ X1 )
!= f__1 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_122,c_0_123]),c_0_110]),c_0_119]),c_0_105]) ).
thf(c_0_127,plain,
! [X1: g] :
( ( ( f__0 @ ( esk247_1 @ X1 ) @ X1 )
= f__1 )
| p12 ),
inference(spm,[status(thm)],[c_0_107,c_0_124]) ).
thf(c_0_128,plain,
( ~ p20
| ( ( f__0 @ f__1 @ f__3 )
!= f__3 )
| ( ( f__0 @ f__3 @ f__1 )
!= f__3 ) ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax20])]) ).
thf(c_0_129,plain,
( ~ p12
| ~ p15 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_125,c_0_78])]) ).
thf(c_0_130,plain,
p12,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126,c_0_127]),c_0_107])]) ).
thf(c_0_131,plain,
( ~ p20
| ( ( f__0 @ f__1 @ f__3 )
!= f__3 )
| ( ( f__0 @ f__3 @ f__1 )
!= f__3 ) ),
inference(split_conjunct,[status(thm)],[c_0_128]) ).
thf(c_0_132,plain,
( p15
| p20 ),
inference(split_conjunct,[status(thm)],[ax1708]) ).
thf(c_0_133,plain,
~ p15,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_129,c_0_130])]) ).
thf(c_0_134,plain,
! [X1: g,X2: g] :
( ( f__0 @ X1 @ ( f__0 @ X2 @ ( esk247_1 @ ( f__0 @ X1 @ X2 ) ) ) )
= f__1 ),
inference(spm,[status(thm)],[c_0_107,c_0_99]) ).
thf(c_0_135,plain,
( ( ( f__0 @ f__1 @ f__3 )
!= f__3 )
| ~ p20 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131,c_0_105])]) ).
thf(c_0_136,plain,
p20,
inference(sr,[status(thm)],[c_0_132,c_0_133]) ).
thf(c_0_137,plain,
! [X1: g,X2: g] :
( ( f__0 @ f__1 @ ( f__0 @ X1 @ ( esk247_1 @ ( f__0 @ ( esk247_1 @ X2 ) @ X1 ) ) ) )
= X2 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115,c_0_134]),c_0_105]) ).
thf(c_0_138,plain,
( ( f__0 @ f__1 @ f__3 )
!= f__3 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_135,c_0_136])]) ).
thf(c_0_139,plain,
! [X1: g] :
( ( f__0 @ f__1 @ X1 )
= X1 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_110]),c_0_99]),c_0_137]) ).
thf(c_0_140,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_138,c_0_139])]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
! [X1: g > g > g,X2: g] :
( ( ~ ( ~ ( ! [X3: g,X4: g,X5: g] :
( ( X1 @ ( X1 @ X3 @ X4 ) @ X5 )
= ( X1 @ X3 @ ( X1 @ X4 @ X5 ) ) )
=> ~ ! [X3: g] :
~ ( ( ( X1 @ X2 @ X3 )
= X3 )
=> ( ( X1 @ X3 @ X2 )
!= X3 ) ) )
=> ~ ! [X3: g] :
~ ! [X4: g] :
( ( ( X1 @ X3 @ X4 )
= X2 )
=> ( ( X1 @ X4 @ X3 )
!= X2 ) ) ) )
= ( ~ ( ~ ( ! [X3: g,X4: g,X5: g] :
( ( X1 @ ( X1 @ X3 @ X4 ) @ X5 )
= ( X1 @ X3 @ ( X1 @ X4 @ X5 ) ) )
=> ~ ! [X3: g] :
( ( X1 @ X3 @ X2 )
= X3 ) )
=> ~ ! [X3: g] :
~ ! [X4: g] :
( ( X1 @ X3 @ X4 )
!= X2 ) ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : ALG271^5 : TPTP v9.2.0. Bugfixed v5.3.0.
% 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n022.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 23:27:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 76.44/76.22 % SZS status Theorem
% 76.44/76.22 % Mode: mode446
% 76.44/76.22 % Inferences: 19499
% 76.44/76.22 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------