TPTP Problem File: SWX208+1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX208+1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find the inverse of a printing function
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Parse_prop3.p [CST26]
% Status : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 156 ( 152 unt; 0 def)
% Number of atoms : 161 ( 161 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 120 ( 115 ~; 0 |; 0 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 46 ( 46 usr; 18 con; 0-2 aty)
% Number of variables : 70 ( 69 !; 1 ?)
% SPC : FOF_THM_RFO_PEQ
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2] : proj1pair(pair2(X,X2)) = X ).
fof(axiom_002,axiom,
! [X,X2] : proj2pair(pair2(X,X2)) = X2 ).
fof(axiom_003,axiom,
! [X,X2] : head(cons(X,X2)) = X ).
fof(axiom_004,axiom,
! [X,X2] : tail(cons(X,X2)) = X2 ).
fof(axiom_005,axiom,
! [X,X2] : nil != cons(X,X2) ).
fof(axiom_006,axiom,
! [X] : proj1S(s(X)) = X ).
fof(axiom_007,axiom,
! [X] : z != s(X) ).
fof(axiom_008,axiom,
! [X,X2] : proj1Add(add(X,X2)) = X ).
fof(axiom_009,axiom,
! [X,X2] : proj2Add(add(X,X2)) = X2 ).
fof(axiom_010,axiom,
! [X,X2] : proj1Mul(mul(X,X2)) = X ).
fof(axiom_011,axiom,
! [X,X2] : proj2Mul(mul(X,X2)) = X2 ).
fof(axiom_012,axiom,
! [X] : proj1Num(num(X)) = X ).
fof(axiom_013,axiom,
! [X,X2] : x != add(X,X2) ).
fof(axiom_014,axiom,
! [X,X2] : x != mul(X,X2) ).
fof(axiom_015,axiom,
! [X] : x != num(X) ).
fof(axiom_016,axiom,
! [X,X2,X3,X4] : add(X,X2) != mul(X3,X4) ).
fof(axiom_017,axiom,
! [X,X2,X3] : add(X,X2) != num(X3) ).
fof(axiom_018,axiom,
! [X,X2,X3] : mul(X,X2) != num(X3) ).
fof(axiom_019,axiom,
! [X] : proj1Left(left(X)) = X ).
fof(axiom_020,axiom,
! [X] : proj1Right(right(X)) = X ).
fof(axiom_021,axiom,
! [X,X2] : left(X) != right(X2) ).
fof(axiom_022,axiom,
pAR1 != pAR2 ).
fof(axiom_023,axiom,
pAR1 != pLUS ).
fof(axiom_024,axiom,
pAR1 != mULT ).
fof(axiom_025,axiom,
pAR1 != cHARX ).
fof(axiom_026,axiom,
pAR1 != dIG0 ).
fof(axiom_027,axiom,
pAR1 != dIG1 ).
fof(axiom_028,axiom,
pAR1 != dIG2 ).
fof(axiom_029,axiom,
pAR1 != dIG3 ).
fof(axiom_030,axiom,
pAR1 != dIG4 ).
fof(axiom_031,axiom,
pAR1 != dIG5 ).
fof(axiom_032,axiom,
pAR1 != dIG6 ).
fof(axiom_033,axiom,
pAR1 != dIG7 ).
fof(axiom_034,axiom,
pAR1 != dIG8 ).
fof(axiom_035,axiom,
pAR1 != dIG9 ).
fof(axiom_036,axiom,
pAR2 != pLUS ).
fof(axiom_037,axiom,
pAR2 != mULT ).
fof(axiom_038,axiom,
pAR2 != cHARX ).
fof(axiom_039,axiom,
pAR2 != dIG0 ).
fof(axiom_040,axiom,
pAR2 != dIG1 ).
fof(axiom_041,axiom,
pAR2 != dIG2 ).
fof(axiom_042,axiom,
pAR2 != dIG3 ).
fof(axiom_043,axiom,
pAR2 != dIG4 ).
fof(axiom_044,axiom,
pAR2 != dIG5 ).
fof(axiom_045,axiom,
pAR2 != dIG6 ).
fof(axiom_046,axiom,
pAR2 != dIG7 ).
fof(axiom_047,axiom,
pAR2 != dIG8 ).
fof(axiom_048,axiom,
pAR2 != dIG9 ).
fof(axiom_049,axiom,
pLUS != mULT ).
fof(axiom_050,axiom,
pLUS != cHARX ).
fof(axiom_051,axiom,
pLUS != dIG0 ).
fof(axiom_052,axiom,
pLUS != dIG1 ).
fof(axiom_053,axiom,
pLUS != dIG2 ).
fof(axiom_054,axiom,
pLUS != dIG3 ).
fof(axiom_055,axiom,
pLUS != dIG4 ).
fof(axiom_056,axiom,
pLUS != dIG5 ).
fof(axiom_057,axiom,
pLUS != dIG6 ).
fof(axiom_058,axiom,
pLUS != dIG7 ).
fof(axiom_059,axiom,
pLUS != dIG8 ).
fof(axiom_060,axiom,
pLUS != dIG9 ).
fof(axiom_061,axiom,
mULT != cHARX ).
fof(axiom_062,axiom,
mULT != dIG0 ).
fof(axiom_063,axiom,
mULT != dIG1 ).
fof(axiom_064,axiom,
mULT != dIG2 ).
fof(axiom_065,axiom,
mULT != dIG3 ).
fof(axiom_066,axiom,
mULT != dIG4 ).
fof(axiom_067,axiom,
mULT != dIG5 ).
fof(axiom_068,axiom,
mULT != dIG6 ).
fof(axiom_069,axiom,
mULT != dIG7 ).
fof(axiom_070,axiom,
mULT != dIG8 ).
fof(axiom_071,axiom,
mULT != dIG9 ).
fof(axiom_072,axiom,
cHARX != dIG0 ).
fof(axiom_073,axiom,
cHARX != dIG1 ).
fof(axiom_074,axiom,
cHARX != dIG2 ).
fof(axiom_075,axiom,
cHARX != dIG3 ).
fof(axiom_076,axiom,
cHARX != dIG4 ).
fof(axiom_077,axiom,
cHARX != dIG5 ).
fof(axiom_078,axiom,
cHARX != dIG6 ).
fof(axiom_079,axiom,
cHARX != dIG7 ).
fof(axiom_080,axiom,
cHARX != dIG8 ).
fof(axiom_081,axiom,
cHARX != dIG9 ).
fof(axiom_082,axiom,
dIG0 != dIG1 ).
fof(axiom_083,axiom,
dIG0 != dIG2 ).
fof(axiom_084,axiom,
dIG0 != dIG3 ).
fof(axiom_085,axiom,
dIG0 != dIG4 ).
fof(axiom_086,axiom,
dIG0 != dIG5 ).
fof(axiom_087,axiom,
dIG0 != dIG6 ).
fof(axiom_088,axiom,
dIG0 != dIG7 ).
fof(axiom_089,axiom,
dIG0 != dIG8 ).
fof(axiom_090,axiom,
dIG0 != dIG9 ).
fof(axiom_091,axiom,
dIG1 != dIG2 ).
fof(axiom_092,axiom,
dIG1 != dIG3 ).
fof(axiom_093,axiom,
dIG1 != dIG4 ).
fof(axiom_094,axiom,
dIG1 != dIG5 ).
fof(axiom_095,axiom,
dIG1 != dIG6 ).
fof(axiom_096,axiom,
dIG1 != dIG7 ).
fof(axiom_097,axiom,
dIG1 != dIG8 ).
fof(axiom_098,axiom,
dIG1 != dIG9 ).
fof(axiom_099,axiom,
dIG2 != dIG3 ).
fof(axiom_100,axiom,
dIG2 != dIG4 ).
fof(axiom_101,axiom,
dIG2 != dIG5 ).
fof(axiom_102,axiom,
dIG2 != dIG6 ).
fof(axiom_103,axiom,
dIG2 != dIG7 ).
fof(axiom_104,axiom,
dIG2 != dIG8 ).
fof(axiom_105,axiom,
dIG2 != dIG9 ).
fof(axiom_106,axiom,
dIG3 != dIG4 ).
fof(axiom_107,axiom,
dIG3 != dIG5 ).
fof(axiom_108,axiom,
dIG3 != dIG6 ).
fof(axiom_109,axiom,
dIG3 != dIG7 ).
fof(axiom_110,axiom,
dIG3 != dIG8 ).
fof(axiom_111,axiom,
dIG3 != dIG9 ).
fof(axiom_112,axiom,
dIG4 != dIG5 ).
fof(axiom_113,axiom,
dIG4 != dIG6 ).
fof(axiom_114,axiom,
dIG4 != dIG7 ).
fof(axiom_115,axiom,
dIG4 != dIG8 ).
fof(axiom_116,axiom,
dIG4 != dIG9 ).
fof(axiom_117,axiom,
dIG5 != dIG6 ).
fof(axiom_118,axiom,
dIG5 != dIG7 ).
fof(axiom_119,axiom,
dIG5 != dIG8 ).
fof(axiom_120,axiom,
dIG5 != dIG9 ).
fof(axiom_121,axiom,
dIG6 != dIG7 ).
fof(axiom_122,axiom,
dIG6 != dIG8 ).
fof(axiom_123,axiom,
dIG6 != dIG9 ).
fof(axiom_124,axiom,
dIG7 != dIG8 ).
fof(axiom_125,axiom,
dIG7 != dIG9 ).
fof(axiom_126,axiom,
dIG8 != dIG9 ).
fof(axiom_127,axiom,
! [Y] : append(nil,Y) = Y ).
fof(axiom_128,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).
fof(axiom_129,axiom,
x2(z,z) = z ).
fof(axiom_130,axiom,
! [Z] : x2(z,s(Z)) = z ).
fof(axiom_131,axiom,
! [N] : x2(s(N),z) = s(N) ).
fof(axiom_132,axiom,
! [N,M] : x2(s(N),s(M)) = x2(N,M) ).
fof(axiom_133,axiom,
min10(z) = left(dIG0) ).
fof(axiom_134,axiom,
min10(s(z)) = left(dIG1) ).
fof(axiom_135,axiom,
min10(s(s(z))) = left(dIG2) ).
fof(axiom_136,axiom,
min10(s(s(s(z)))) = left(dIG3) ).
fof(axiom_137,axiom,
min10(s(s(s(s(z))))) = left(dIG4) ).
fof(axiom_138,axiom,
min10(s(s(s(s(s(z)))))) = left(dIG5) ).
fof(axiom_139,axiom,
min10(s(s(s(s(s(s(z))))))) = left(dIG6) ).
fof(axiom_140,axiom,
min10(s(s(s(s(s(s(s(z)))))))) = left(dIG7) ).
fof(axiom_141,axiom,
min10(s(s(s(s(s(s(s(s(z))))))))) = left(dIG8) ).
fof(axiom_142,axiom,
min10(s(s(s(s(s(s(s(s(s(z)))))))))) = left(dIG9) ).
fof(axiom_143,axiom,
! [X9] : min10(s(s(s(s(s(s(s(s(s(s(X9))))))))))) = right(x2(s(s(s(s(s(s(s(s(s(s(X9)))))))))),s(s(s(s(s(s(s(s(s(s(z)))))))))))) ).
fof(axiom_144,axiom,
! [X,D] :
( min10(X) = left(D)
=> mod10(X) = pair2(D,z) ) ).
fof(axiom_145,axiom,
! [X,N,D1,N2] :
( min10(X) = right(N)
=> ( mod10(N) = pair2(D1,N2)
=> mod10(X) = pair2(D1,s(N2)) ) ) ).
fof(axiom_146,axiom,
! [X] : showNumnum(X,z) = X ).
fof(axiom_147,axiom,
! [X,Z,A1,N] :
( mod10(s(Z)) = pair2(A1,N)
=> showNumnum(X,s(Z)) = showNumnum(cons(A1,X),N) ) ).
fof(axiom_148,axiom,
showNum(z) = cons(dIG0,nil) ).
fof(axiom_149,axiom,
! [Y] : showNum(s(Y)) = showNumnum(nil,s(Y)) ).
fof(axiom_150,axiom,
show(x) = cons(cHARX,nil) ).
fof(axiom_151,axiom,
! [B,C] : show(add(B,C)) = append(show(B),append(cons(pLUS,nil),show(C))) ).
fof(axiom_152,axiom,
! [A3,B2] : show(mul(A3,B2)) = append(showF(A3),append(cons(mULT,nil),showF(B2))) ).
fof(axiom_153,axiom,
! [N] : show(num(N)) = showNum(N) ).
fof(axiom_154,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> showF(X) = show(X) ) ).
fof(axiom_155,axiom,
! [Y,Z] : showF(add(Y,Z)) = cons(pAR1,append(show(add(Y,Z)),cons(pAR2,nil))) ).
fof(goal_156,conjecture,
? [E] : show(E) = cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil))))))))))) ).
%------------------------------------------------------------------------------