%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP044^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 : n006.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 237.49s 237.16s
% Output : Proof 237.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 12
% Syntax : Number of formulae : 37 ( 22 unt; 0 typ; 0 def)
% Number of atoms : 169 ( 27 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 125 ( 17 ~; 12 |; 0 &; 90 @)
% ( 0 <=>; 5 =>; 1 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 22 ( 20 usr; 21 con; 0-2 aty)
% Number of variables : 15 ( 0 ^; 15 !; 0 ?; 15 :)
% Comments :
%------------------------------------------------------------------------------
thf(conj_0,conjecture,
( ( descar2095969287nges_a @ ys )
= ( descar2095969287nges_a @ ( coeffs_a @ g ) ) ) ).
thf(h0,negated_conjecture,
( ( descar2095969287nges_a @ ys )
!= ( descar2095969287nges_a @ ( coeffs_a @ g ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(pax41,axiom,
( p41
=> ! [X893: list_a] :
( ( fpoly_a2 @ ( fappend_a @ X893 @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) )
= ( fpoly_a2 @ X893 ) ) ),
file('<stdin>',pax41) ).
thf(pax7,axiom,
( p7
=> ( fys
= ( fappend_a @ ( fcoeffs_a @ fg ) @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) ) ),
file('<stdin>',pax7) ).
thf(pax10,axiom,
( p10
=> ! [X910: poly_a] :
( ( fpoly_a2 @ ( fcoeffs_a @ X910 ) )
= X910 ) ),
file('<stdin>',pax10) ).
thf(pax6,axiom,
( p6
=> ! [X914: list_a,X915: poly_a] :
( ( ( fpoly_a2 @ X914 )
= X915 )
=> ( ( fdescar2095969287nges_a @ X914 )
= ( fdescar2095969287nges_a @ ( fcoeffs_a @ X915 ) ) ) ) ),
file('<stdin>',pax6) ).
thf(ax1738,axiom,
p41,
file('<stdin>',ax1738) ).
thf(ax1772,axiom,
p7,
file('<stdin>',ax1772) ).
thf(ax1769,axiom,
p10,
file('<stdin>',ax1769) ).
thf(nax1,axiom,
( p1
<= ( ( fdescar2095969287nges_a @ fys )
= ( fdescar2095969287nges_a @ ( fcoeffs_a @ fg ) ) ) ),
file('<stdin>',nax1) ).
thf(ax1778,axiom,
~ p1,
file('<stdin>',ax1778) ).
thf(ax1773,axiom,
p6,
file('<stdin>',ax1773) ).
thf(c_0_10,plain,
! [X2918: list_a] :
( ~ p41
| ( ( fpoly_a2 @ ( fappend_a @ X2918 @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) )
= ( fpoly_a2 @ X2918 ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax41])])]) ).
thf(c_0_11,plain,
( ~ p7
| ( fys
= ( fappend_a @ ( fcoeffs_a @ fg ) @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) ) ),
inference(fof_nnf,[status(thm)],[pax7]) ).
thf(c_0_12,plain,
! [X2972: poly_a] :
( ~ p10
| ( ( fpoly_a2 @ ( fcoeffs_a @ X2972 ) )
= X2972 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax10])])]) ).
thf(c_0_13,plain,
! [X2982: list_a,X2983: poly_a] :
( ~ p6
| ( ( fpoly_a2 @ X2982 )
!= X2983 )
| ( ( fdescar2095969287nges_a @ X2982 )
= ( fdescar2095969287nges_a @ ( fcoeffs_a @ X2983 ) ) ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])]) ).
thf(c_0_14,plain,
! [X1: list_a] :
( ( ( fpoly_a2 @ ( fappend_a @ X1 @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) )
= ( fpoly_a2 @ X1 ) )
| ~ p41 ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_15,plain,
p41,
inference(split_conjunct,[status(thm)],[ax1738]) ).
thf(c_0_16,plain,
( ( fys
= ( fappend_a @ ( fcoeffs_a @ fg ) @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) )
| ~ p7 ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
thf(c_0_17,plain,
p7,
inference(split_conjunct,[status(thm)],[ax1772]) ).
thf(c_0_18,plain,
! [X106: poly_a] :
( ( ( fpoly_a2 @ ( fcoeffs_a @ X106 ) )
= X106 )
| ~ p10 ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
thf(c_0_19,plain,
p10,
inference(split_conjunct,[status(thm)],[ax1769]) ).
thf(c_0_20,plain,
( ( ( fdescar2095969287nges_a @ fys )
!= ( fdescar2095969287nges_a @ ( fcoeffs_a @ fg ) ) )
| p1 ),
inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])]) ).
thf(c_0_21,plain,
~ p1,
inference(fof_simplification,[status(thm)],[ax1778]) ).
thf(c_0_22,plain,
! [X1: list_a,X106: poly_a] :
( ( ( fdescar2095969287nges_a @ X1 )
= ( fdescar2095969287nges_a @ ( fcoeffs_a @ X106 ) ) )
| ~ p6
| ( ( fpoly_a2 @ X1 )
!= X106 ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
thf(c_0_23,plain,
p6,
inference(split_conjunct,[status(thm)],[ax1773]) ).
thf(c_0_24,plain,
! [X1: list_a] :
( ( fpoly_a2 @ ( fappend_a @ X1 @ ( fcons_a @ fzero_zero_a @ fnil_a ) ) )
= ( fpoly_a2 @ X1 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14,c_0_15])]) ).
thf(c_0_25,plain,
( ( fappend_a @ ( fcoeffs_a @ fg ) @ ( fcons_a @ fzero_zero_a @ fnil_a ) )
= fys ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16,c_0_17])]) ).
thf(c_0_26,plain,
! [X106: poly_a] :
( ( fpoly_a2 @ ( fcoeffs_a @ X106 ) )
= X106 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_19])]) ).
thf(c_0_27,plain,
( p1
| ( ( fdescar2095969287nges_a @ fys )
!= ( fdescar2095969287nges_a @ ( fcoeffs_a @ fg ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_28,plain,
~ p1,
inference(split_conjunct,[status(thm)],[c_0_21]) ).
thf(c_0_29,plain,
! [X1: list_a] :
( ( fdescar2095969287nges_a @ ( fcoeffs_a @ ( fpoly_a2 @ X1 ) ) )
= ( fdescar2095969287nges_a @ X1 ) ),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22,c_0_23])])]) ).
thf(c_0_30,plain,
( ( fpoly_a2 @ fys )
= fg ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24,c_0_25]),c_0_26]) ).
thf(c_0_31,plain,
( ( fdescar2095969287nges_a @ ( fcoeffs_a @ fg ) )
!= ( fdescar2095969287nges_a @ fys ) ),
inference(sr,[status(thm)],[c_0_27,c_0_28]) ).
thf(c_0_32,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
( ( descar2095969287nges_a @ ys )
= ( descar2095969287nges_a @ ( coeffs_a @ g ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.21 % Problem : ITP044^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.21 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.41 % Computer : n006.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8042.1875MB
% 0.12/0.41 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Wed Oct 8 17:56:38 EDT 2025
% 0.12/0.41 % CPUTime :
% 237.49/237.16 % SZS status Theorem
% 237.49/237.16 % Mode: mode328:USE_SINE=true:SINE_TOLERANCE=5.0:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 237.49/237.16 % Inferences: 241
% 237.49/237.16 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------