%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG298^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 : n026.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:20 PM UTC 2025
% Result : Theorem 23.77s 23.92s
% Output : Proof 23.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 55 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 367 ( 66 equ; 0 cnn)
% Maximal formula atoms : 10 ( 6 avg)
% Number of connectives : 493 ( 78 ~; 37 |; 12 &; 338 @)
% ( 0 <=>; 24 =>; 4 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 12 ( 12 >; 0 *; 0 +; 0 <<)
% Number of symbols : 34 ( 32 usr; 33 con; 0-2 aty)
% Number of variables : 110 ( 0 ^; 110 !; 0 ?; 110 :)
% Comments :
%------------------------------------------------------------------------------
thf(cTHM270_pme,conjecture,
! [X1: a > b,X2: a > c,X3: b > c] :
( ~ ( ~ ( ~ ( ! [X4: a] :
( ( X3 @ ( X1 @ X4 ) )
= ( X2 @ X4 ) )
=> ~ ! [X4: b] :
~ ! [X5: a] :
( ( X1 @ X5 )
!= X4 ) )
=> ~ ! [X4: a,X5: a] :
( ( X1 @ ( c_stara @ X4 @ X5 ) )
= ( c_starb @ ( X1 @ X4 ) @ ( X1 @ X5 ) ) ) )
=> ~ ! [X4: a,X5: a] :
( ( X2 @ ( c_stara @ X4 @ X5 ) )
= ( c_starc @ ( X2 @ X4 ) @ ( X2 @ X5 ) ) ) )
=> ! [X4: b,X5: b] :
( ( X3 @ ( c_starb @ X4 @ X5 ) )
= ( c_starc @ ( X3 @ X4 ) @ ( X3 @ X5 ) ) ) ) ).
thf(h0,negated_conjecture,
~ ! [X1: a > b,X2: a > c,X3: b > c] :
( ~ ( ~ ( ~ ( ! [X4: a] :
( ( X3 @ ( X1 @ X4 ) )
= ( X2 @ X4 ) )
=> ~ ! [X4: b] :
~ ! [X5: a] :
( ( X1 @ X5 )
!= X4 ) )
=> ~ ! [X4: a,X5: a] :
( ( X1 @ ( c_stara @ X4 @ X5 ) )
= ( c_starb @ ( X1 @ X4 ) @ ( X1 @ X5 ) ) ) )
=> ~ ! [X4: a,X5: a] :
( ( X2 @ ( c_stara @ X4 @ X5 ) )
= ( c_starc @ ( X2 @ X4 ) @ ( X2 @ X5 ) ) ) )
=> ! [X4: b,X5: b] :
( ( X3 @ ( c_starb @ X4 @ X5 ) )
= ( c_starc @ ( X3 @ X4 ) @ ( X3 @ X5 ) ) ) ),
inference(assume_negation,[status(cth)],[cTHM270_pme]) ).
thf(ax7,axiom,
( p1
| ~ p2 ),
file('<stdin>',ax7) ).
thf(ax8,axiom,
~ p1,
file('<stdin>',ax8) ).
thf(ax6,axiom,
( p2
| ~ p3 ),
file('<stdin>',ax6) ).
thf(ax5,axiom,
( p3
| ~ p4 ),
file('<stdin>',ax5) ).
thf(nax4,axiom,
( p4
<= ( ~ ( ~ ( ~ ( ! [X23: a] :
( ( f__2 @ ( f__0 @ X23 ) )
= ( f__1 @ X23 ) )
=> ~ ! [X24: b] :
~ ! [X25: a] :
( ( f__0 @ X25 )
!= X24 ) )
=> ~ ! [X26: a,X25: a] :
( ( f__0 @ ( fc_stara @ X26 @ X25 ) )
= ( fc_starb @ ( f__0 @ X26 ) @ ( f__0 @ X25 ) ) ) )
=> ~ ! [X26: a,X25: a] :
( ( f__1 @ ( fc_stara @ X26 @ X25 ) )
= ( fc_starc @ ( f__1 @ X26 ) @ ( f__1 @ X25 ) ) ) )
=> ! [X27: b,X28: b] :
( ( f__2 @ ( fc_starb @ X27 @ X28 ) )
= ( fc_starc @ ( f__2 @ X27 ) @ ( f__2 @ X28 ) ) ) ) ),
file('<stdin>',nax4) ).
thf(nax2,axiom,
( p2
<= ! [X42: a > c,X43: b > c] :
( ~ ( ~ ( ~ ( ! [X50: a] :
( ( X43 @ ( f__0 @ X50 ) )
= ( X42 @ X50 ) )
=> ~ ! [X51: b] :
~ ! [X52: a] :
( ( f__0 @ X52 )
!= X51 ) )
=> ~ ! [X53: a,X52: a] :
( ( f__0 @ ( fc_stara @ X53 @ X52 ) )
= ( fc_starb @ ( f__0 @ X53 ) @ ( f__0 @ X52 ) ) ) )
=> ~ ! [X53: a,X52: a] :
( ( X42 @ ( fc_stara @ X53 @ X52 ) )
= ( fc_starc @ ( X42 @ X53 ) @ ( X42 @ X52 ) ) ) )
=> ! [X54: b,X55: b] :
( ( X43 @ ( fc_starb @ X54 @ X55 ) )
= ( fc_starc @ ( X43 @ X54 ) @ ( X43 @ X55 ) ) ) ) ),
file('<stdin>',nax2) ).
thf(nax3,axiom,
( p3
<= ! [X29: b > c] :
( ~ ( ~ ( ~ ( ! [X36: a] :
( ( X29 @ ( f__0 @ X36 ) )
= ( f__1 @ X36 ) )
=> ~ ! [X37: b] :
~ ! [X38: a] :
( ( f__0 @ X38 )
!= X37 ) )
=> ~ ! [X39: a,X38: a] :
( ( f__0 @ ( fc_stara @ X39 @ X38 ) )
= ( fc_starb @ ( f__0 @ X39 ) @ ( f__0 @ X38 ) ) ) )
=> ~ ! [X39: a,X38: a] :
( ( f__1 @ ( fc_stara @ X39 @ X38 ) )
= ( fc_starc @ ( f__1 @ X39 ) @ ( f__1 @ X38 ) ) ) )
=> ! [X40: b,X41: b] :
( ( X29 @ ( fc_starb @ X40 @ X41 ) )
= ( fc_starc @ ( X29 @ X40 ) @ ( X29 @ X41 ) ) ) ) ),
file('<stdin>',nax3) ).
thf(ax3,axiom,
( p4
| ~ p6 ),
file('<stdin>',ax3) ).
thf(ax0,axiom,
( p6
| ~ p9 ),
file('<stdin>',ax0) ).
thf(nax9,axiom,
( p9
<= ! [X5: b] :
( ( f__2 @ ( fc_starb @ f__3 @ X5 ) )
= ( fc_starc @ ( f__2 @ f__3 ) @ ( f__2 @ X5 ) ) ) ),
file('<stdin>',nax9) ).
thf(c_0_10,plain,
( p1
| ~ p2 ),
inference(fof_simplification,[status(thm)],[ax7]) ).
thf(c_0_11,plain,
~ p1,
inference(fof_simplification,[status(thm)],[ax8]) ).
thf(c_0_12,plain,
( p2
| ~ p3 ),
inference(fof_simplification,[status(thm)],[ax6]) ).
thf(c_0_13,plain,
( p1
| ~ p2 ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_14,plain,
~ p1,
inference(split_conjunct,[status(thm)],[c_0_11]) ).
thf(c_0_15,plain,
( p3
| ~ p4 ),
inference(fof_simplification,[status(thm)],[ax5]) ).
thf(c_0_16,plain,
( p2
| ~ p3 ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_17,plain,
~ p2,
inference(sr,[status(thm)],[c_0_13,c_0_14]) ).
thf(c_0_18,plain,
! [X120: a,X121: b,X123: a,X124: a,X125: a,X126: a] :
( ( ( ( f__2 @ ( f__0 @ X120 ) )
= ( f__1 @ X120 ) )
| p4 )
& ( ( ( f__0 @ ( esk27_1 @ X121 ) )
= X121 )
| p4 )
& ( ( ( f__0 @ ( fc_stara @ X123 @ X124 ) )
= ( fc_starb @ ( f__0 @ X123 ) @ ( f__0 @ X124 ) ) )
| p4 )
& ( ( ( f__1 @ ( fc_stara @ X125 @ X126 ) )
= ( fc_starc @ ( f__1 @ X125 ) @ ( f__1 @ X126 ) ) )
| p4 )
& ( ( ( f__2 @ ( fc_starb @ esk28_0 @ esk29_0 ) )
!= ( fc_starc @ ( f__2 @ esk28_0 ) @ ( f__2 @ esk29_0 ) ) )
| p4 ) ),
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)],[nax4])])])])])]) ).
thf(c_0_19,plain,
( p3
| ~ p4 ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
thf(c_0_20,plain,
~ p3,
inference(sr,[status(thm)],[c_0_16,c_0_17]) ).
thf(c_0_21,plain,
! [X162: a,X163: b,X165: a,X166: a,X167: a,X168: a] :
( ( ( ( esk47_0 @ ( f__0 @ X162 ) )
= ( esk46_0 @ X162 ) )
| p2 )
& ( ( ( f__0 @ ( esk48_1 @ X163 ) )
= X163 )
| p2 )
& ( ( ( f__0 @ ( fc_stara @ X165 @ X166 ) )
= ( fc_starb @ ( f__0 @ X165 ) @ ( f__0 @ X166 ) ) )
| p2 )
& ( ( ( esk46_0 @ ( fc_stara @ X167 @ X168 ) )
= ( fc_starc @ ( esk46_0 @ X167 ) @ ( esk46_0 @ X168 ) ) )
| p2 )
& ( ( ( esk47_0 @ ( fc_starb @ esk49_0 @ esk50_0 ) )
!= ( fc_starc @ ( esk47_0 @ esk49_0 ) @ ( esk47_0 @ esk50_0 ) ) )
| p2 ) ),
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)],[nax2])])])])])]) ).
thf(c_0_22,plain,
! [X140: a,X141: b,X143: a,X144: a,X145: a,X146: a] :
( ( ( ( esk36_0 @ ( f__0 @ X140 ) )
= ( f__1 @ X140 ) )
| p3 )
& ( ( ( f__0 @ ( esk37_1 @ X141 ) )
= X141 )
| p3 )
& ( ( ( f__0 @ ( fc_stara @ X143 @ X144 ) )
= ( fc_starb @ ( f__0 @ X143 ) @ ( f__0 @ X144 ) ) )
| p3 )
& ( ( ( f__1 @ ( fc_stara @ X145 @ X146 ) )
= ( fc_starc @ ( f__1 @ X145 ) @ ( f__1 @ X146 ) ) )
| p3 )
& ( ( ( esk36_0 @ ( fc_starb @ esk38_0 @ esk39_0 ) )
!= ( fc_starc @ ( esk36_0 @ esk38_0 ) @ ( esk36_0 @ esk39_0 ) ) )
| p3 ) ),
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)],[nax3])])])])])]) ).
thf(c_0_23,plain,
! [X1: a] :
( ( ( f__2 @ ( f__0 @ X1 ) )
= ( f__1 @ X1 ) )
| p4 ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_24,plain,
~ p4,
inference(sr,[status(thm)],[c_0_19,c_0_20]) ).
thf(c_0_25,plain,
! [X2: b] :
( ( ( f__0 @ ( esk48_1 @ X2 ) )
= X2 )
| p2 ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
thf(c_0_26,plain,
! [X1: a] :
( ( ( esk36_0 @ ( f__0 @ X1 ) )
= ( f__1 @ X1 ) )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
thf(c_0_27,plain,
! [X1: a] :
( ( f__2 @ ( f__0 @ X1 ) )
= ( f__1 @ X1 ) ),
inference(sr,[status(thm)],[c_0_23,c_0_24]) ).
thf(c_0_28,plain,
! [X2: b] :
( ( f__0 @ ( esk48_1 @ X2 ) )
= X2 ),
inference(sr,[status(thm)],[c_0_25,c_0_17]) ).
thf(c_0_29,plain,
! [X1: a] :
( ( esk36_0 @ ( f__0 @ X1 ) )
= ( f__1 @ X1 ) ),
inference(sr,[status(thm)],[c_0_26,c_0_20]) ).
thf(c_0_30,plain,
! [X2: b] :
( ( f__1 @ ( esk48_1 @ X2 ) )
= ( f__2 @ X2 ) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
thf(c_0_31,plain,
( p4
| ~ p6 ),
inference(fof_simplification,[status(thm)],[ax3]) ).
thf(c_0_32,plain,
! [X1: a,X3: a] :
( ( ( f__0 @ ( fc_stara @ X1 @ X3 ) )
= ( fc_starb @ ( f__0 @ X1 ) @ ( f__0 @ X3 ) ) )
| p2 ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
thf(c_0_33,plain,
! [X1: a,X3: a] :
( ( ( f__1 @ ( fc_stara @ X1 @ X3 ) )
= ( fc_starc @ ( f__1 @ X1 ) @ ( f__1 @ X3 ) ) )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
thf(c_0_34,plain,
! [X2: b] :
( ( f__2 @ X2 )
= ( esk36_0 @ X2 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_28]),c_0_30]) ).
thf(c_0_35,plain,
( p6
| ~ p9 ),
inference(fof_simplification,[status(thm)],[ax0]) ).
thf(c_0_36,plain,
( p4
| ~ p6 ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_37,plain,
! [X1: a,X3: a] :
( ( fc_starb @ ( f__0 @ X1 ) @ ( f__0 @ X3 ) )
= ( f__0 @ ( fc_stara @ X1 @ X3 ) ) ),
inference(sr,[status(thm)],[c_0_32,c_0_17]) ).
thf(c_0_38,plain,
! [X1: a,X3: a] :
( ( fc_starc @ ( f__1 @ X1 ) @ ( f__1 @ X3 ) )
= ( f__1 @ ( fc_stara @ X1 @ X3 ) ) ),
inference(sr,[status(thm)],[c_0_33,c_0_20]) ).
thf(c_0_39,plain,
! [X2: b] :
( ( f__1 @ ( esk48_1 @ X2 ) )
= ( esk36_0 @ X2 ) ),
inference(rw,[status(thm)],[c_0_30,c_0_34]) ).
thf(c_0_40,plain,
( ( ( f__2 @ ( fc_starb @ f__3 @ esk4_0 ) )
!= ( fc_starc @ ( f__2 @ f__3 ) @ ( f__2 @ esk4_0 ) ) )
| p9 ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])])]) ).
thf(c_0_41,plain,
( p6
| ~ p9 ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
thf(c_0_42,plain,
~ p6,
inference(sr,[status(thm)],[c_0_36,c_0_24]) ).
thf(c_0_43,plain,
! [X1: a,X2: b] :
( ( f__0 @ ( fc_stara @ X1 @ ( esk48_1 @ X2 ) ) )
= ( fc_starb @ ( f__0 @ X1 ) @ X2 ) ),
inference(spm,[status(thm)],[c_0_37,c_0_28]) ).
thf(c_0_44,plain,
! [X1: a,X2: b] :
( ( f__1 @ ( fc_stara @ X1 @ ( esk48_1 @ X2 ) ) )
= ( fc_starc @ ( f__1 @ X1 ) @ ( esk36_0 @ X2 ) ) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
thf(c_0_45,plain,
( p9
| ( ( f__2 @ ( fc_starb @ f__3 @ esk4_0 ) )
!= ( fc_starc @ ( f__2 @ f__3 ) @ ( f__2 @ esk4_0 ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
thf(c_0_46,plain,
~ p9,
inference(sr,[status(thm)],[c_0_41,c_0_42]) ).
thf(c_0_47,plain,
! [X1: a,X2: b] :
( ( fc_starc @ ( f__1 @ X1 ) @ ( esk36_0 @ X2 ) )
= ( esk36_0 @ ( fc_starb @ ( f__0 @ X1 ) @ X2 ) ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_43]),c_0_44]) ).
thf(c_0_48,plain,
( ( fc_starc @ ( esk36_0 @ f__3 ) @ ( esk36_0 @ esk4_0 ) )
!= ( esk36_0 @ ( fc_starb @ f__3 @ esk4_0 ) ) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45,c_0_34]),c_0_34]),c_0_34]),c_0_46]) ).
thf(c_0_49,plain,
! [X2: b,X5: b] :
( ( fc_starc @ ( esk36_0 @ X2 ) @ ( esk36_0 @ X5 ) )
= ( esk36_0 @ ( fc_starb @ X2 @ X5 ) ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47,c_0_39]),c_0_28]) ).
thf(c_0_50,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48,c_0_49])]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
! [X1: a > b,X2: a > c,X3: b > c] :
( ~ ( ~ ( ~ ( ! [X4: a] :
( ( X3 @ ( X1 @ X4 ) )
= ( X2 @ X4 ) )
=> ~ ! [X4: b] :
~ ! [X5: a] :
( ( X1 @ X5 )
!= X4 ) )
=> ~ ! [X4: a,X5: a] :
( ( X1 @ ( c_stara @ X4 @ X5 ) )
= ( c_starb @ ( X1 @ X4 ) @ ( X1 @ X5 ) ) ) )
=> ~ ! [X4: a,X5: a] :
( ( X2 @ ( c_stara @ X4 @ X5 ) )
= ( c_starc @ ( X2 @ X4 ) @ ( X2 @ X5 ) ) ) )
=> ! [X4: b,X5: b] :
( ( X3 @ ( c_starb @ X4 @ X5 ) )
= ( c_starc @ ( X3 @ X4 ) @ ( X3 @ X5 ) ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : ALG298^5 : TPTP v9.2.0. Released v4.0.0.
% 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n026.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 23:33:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 23.77/23.92 % SZS status Theorem
% 23.77/23.92 % Mode: mode371
% 23.77/23.92 % Inferences: 7
% 23.77/23.92 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------